超越 LLM 评判：面向智能体自动形式化的机械化验证
Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
精选理由
提出结合语义审查与机械校验的 Lean 验证方法，能发现 LLM 评审遗漏的错误，提升数学自动形式化的可靠性。
AI 摘要
我们提出了一种验证 Lean 形式化结果的新方法，超越了由 LLM 评判忠实度的方式。与大多数依赖 LLM 或经过训练的模型的验证方法不同，我们的方法将基于 LLM 的语义审查与机械化的数值检查和空真性检查相结合，提供可核查的反馈，并检测出 LLM 评判器遗漏的错误。我们将此方法与 Extract-Verify-Proof 自动形式化流水线结合使用，构建了 Formalized Library of Mathematical Functions（FLMF），它是 NIST Digital Library of Mathematical Functions（DLMF）的部分形式化版本。在三个带标注的数据集上，我们的方法在所有参与评估的方法中实现了最低的错误接受率，该指标衡量验证方法所接受的错误陈述占全部错误陈述的比例。专家对结果的审查还发现了现有数据集中的翻译缺陷和源材料缺陷。代码地址：https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git。