Beyond LLM Judge：用机械验证方法核查 Lean 数学形式化
Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
验证 LLM 写的 Lean 证明，别再只靠 LLM 打分了，这篇加了数值和空泛性机械检查，错误率最低，代码开源。
论文提出一种超越 LLM 评审的形式化验证方法，将 LLM 语义审查与机械的数值检查和空泛性检查相结合，能发现 LLM 评审漏掉的错误。作者将该方法与 Extract-Verify-Proof 自动形式化流水线应用于构建 FLMF，这是对 NIST DLMF 数学函数库的部分形式化。在三个带标注数据集上，该方法取得评估方法中最低的接受错误率。专家复核还发现了现有数据集中的翻译缺陷和源文献缺陷。代码已在 GitHub 开源。
Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization
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 results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.
