Natural Language to First-Order Logic LLM-based Autoformalization
This paper provides a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation and identifies open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.