自然语言到一阶逻辑：基于 LLM 的自动形式化综述与任务定义

一篇 arXiv 论文针对以一阶逻辑（FOL）为目标形式化的自动形式化研究，指出现有领域缺少统一任务定义与系统综述。作者提出原则性任务定义，将本体抽取与逻辑翻译区分开，并指出二者混同会妨碍跨研究评估；随后梳理现有数据集、评测指标与基于 LLM 的方法，包括微调、提示与基于验证的改进，并列出基准测试、语义评估、本体感知方法与端到端应用方面的开放挑战。

此前 FOL 自动形式化研究分散，任务边界与评测口径不统一，不同论文结果难以横向比较。该论文首次把任务拆成本体抽取与逻辑翻译两个阶段，并系统整理数据集、指标与方法，为后续研究提供可对齐的参照框架。

论文的核心机制是任务分解：本体抽取负责从自然语言中识别实体、谓词及其关系结构，逻辑翻译负责把该结构映射为 FOL 公式。两者混同会导致评测同时测多种能力，掩盖模型究竟在哪一步失败，从而扭曲跨研究比较。按阶段拆分后，微调、提示与验证式改进可分别对应不同子任务评估。

对做形式化验证、知识库构建或合规规则转写的团队，该分解提示应把抽取与翻译拆成可分别评测的模块，而非端到端一次性交付；数据集与指标的梳理可作为选型与内部基准设计的参考，减少因评测口径不一致导致的返工。

• 在内部规则或合同转 FOL 流程中，先建本体抽取模块并单独验收，再接入逻辑翻译模块
• 按论文提出的本体抽取与逻辑翻译拆分，为自家 LLM 流水线设计两个独立评测集与指标
• 针对验证式改进方法搭建小规模对照实验，比较微调、提示与验证回路的成本与准确率

• 论文给出的 FOL 自动形式化任务定义是否已被社区广泛采用
• 所梳理的数据集与评测指标具体包含哪些，是否有公开排行榜
• 本体感知方法与端到端应用的开放挑战具体指什么
• 该论文是综述还是同时包含新的实验结果