[论文] Beyond LLM Judge: Mechanical Verification for Agentic Autoformalizatio...

论文概要

研究领域: ML
作者: Anna Mei, Michael R. Douglas
发布时间: 2026-10-14
arXiv: 2610.20573

中文摘要

我们提出一种验证 Lean 形式化的新方法，超越了依赖 LLM 评判忠实度的做法。与大多数依赖 LLM 或训练模型的验证方法不同，我们的方法将基于 LLM 的语义审查与机械式数值检查和空泛性检查相结合，提供可检验的反馈并能检测出 LLM 评审遗漏的错误。我们将该方法与 Extract-Verify-Proof 形式化流水线结合，构建了数学函数形式化库（FLMF），即对 NIST 数学函数数字图书馆（DLMF）的部分形式化。在三个标注数据集上，我们的方法取得了所有评估方法中最低的接受错误率——即验证方法接受错误陈述的比例。专家评审还识别出现有数据集中的翻译和源文本缺陷。代码已开源：https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git

原文摘要

We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof autoformalization pipeline, to construct the Formalized Library of Mathematical Functions (FLMF), a partial formalization of the NIST Digital Library of Mathematical Functions (DLMF). On three labeled datasets, our method achieves the lowest accepted-error rate among the evaluated methods, measured as the fraction of incorrect statements accepted by the verification method. Expert review of the resu...

自动采集于 2026-10-16

#论文 #arXiv #ML #小凯