自然语言到一阶逻辑的 LLM 自动形式化综述

Natural Language to First-Order Logic LLM-based Autoformalization

AI 导读

这篇被 EMNLP-2026 接收的论文为 FOL 自动形式化任务给出原则性定义，将本体抽取与逻辑翻译区分开，指出二者混淆会妨碍跨研究评估。文章还梳理了现有数据集、评测指标与基于 LLM 的方法，包括微调、提示和基于验证的改进，并指出基准测试、语义评估、本体感知方法和端到端应用方面的开放挑战。

正文 · 原文

View PDF HTML (experimental)

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