arXiv：cs.CL· Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno·· 3 小时前
自然语言到一阶逻辑：基于 LLM 的自动形式化综述
Natural Language to First-Order Logic LLM-based Autoformalization
AI 导读
一篇被 EMNLP-2026 接收的论文系统梳理了基于 LLM 的“自然语言到一阶逻辑（FOL）”自动形式化任务，首次给出原则性定义，将任务拆分为本体抽取与逻辑翻译两个子任务，并指出二者混淆会妨碍跨研究评估。文章还综述了现有数据集、评估指标以及微调、提示词、基于验证的迭代精修等方法，并指出基准测试、语义评估、本体感知方法和端到端应用方面的开放挑战。
正文
Abstract: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.
| Comments: | Accepted to EMNLP-2026 |
| Subjects: | Computation and Language (cs.CL) |
| Cite as: | arXiv:2610.12030 [cs.CL] |
| (or arXiv:2610.12030v1 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2610.12030 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Michele Mignani [view email]
[v1]
Thu, 8 Oct 2026 14:24:12 UTC (59 KB)
来源：arXiv：cs.CL · arxiv.org