Large Language Models (LLMs) have renewed interest in autoformalization.
Yet, when First-Order Logic (FOL) is considered as the target formalism, the field still lacks a unified task formulation and a systematic survey.
This Paper Addresses This Gap
we first provide a principled definition for the FOL-autoformalization task by distinguishing Ontology Extraction from Logical Translation, showing how their conflation obscures (cross-study) evaluation;
we review existing datasets, evaluation metrics, and LLM-based methods, including fine-tuning, prompting, and verification-based refinement;
we identify open challenges in benchmarking, semantic evaluation, ontology-aware methods, and end-to-end applications.