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

Natural Language to First-Order Logic LLM-based Autoformalization

AI 导读

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

正文 · AI 翻译

查看 PDF HTML（实验性）

摘要：大语言模型（LLMs）重新激发了人们对自动形式化的兴趣。然而，当以一阶逻辑（FOL）作为目标形式化体系时，该领域仍缺乏统一的任务表述和系统性综述。本文填补了这一空白：我们首先通过区分本体抽取与逻辑翻译，为 FOL 自动形式化任务提供了有原则的定义，并说明二者的混同如何模糊了（跨研究的）评估；我们回顾了现有数据集、评估指标和基于 LLM 的方法，包括微调、提示和基于验证的改进；我们指出了在基准测试、语义评估、本体感知方法和端到端应用方面的开放挑战。

评论：	已被 EMNLP-2026 接收
主题：	计算与语言（cs.CL）
引用格式：	arXiv:2610.12030 [cs.CL]
	（或 arXiv:2610.12030v1 [cs.CL] 用于此版本）
	https://doi.org/10.48550/arXiv.2610.12030 arXiv 颁发的 DOI，经由 DataCite（待注册）

提交历史

来自：Michele Mignani [查看电子邮件]
[v1] 2026年10月8日星期四 14:24:12 UTC（59 KB）

来源：arXiv cs.CL · arxiv.org