arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2610.20573cs.LOcs.AI
收藏

超越大语言模型评判:智能体自动形式化的机械验证

Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

Harvard University(哈佛大学);CMSA, Harvard University(哈佛中心数学与理论物理学院,哈佛大学);AletheAI, Inc(AletheAI公司)

Anna Mei, Michael R. Douglas

AI总结:

该研究提出结合LLM语义审查与机械检查的新方法,构建FLMF库,在三个数据集上实现最低可接受错误率,可检测LLM遗漏的错误并发现现有数据集缺陷。

摘要:

我们提出一种用于验证Lean形式化的新方法,该方法超越了大语言模型(LLM)评判的忠实度。与大多数依赖LLM或训练模型的验证方法不同,我们的方法将基于LLM的语义审查与机械数值检查及空值检查相结合,提供可核查的反馈并检测LLM评判遗漏的错误。我们将此方法与Extract-Verify-Proof自动形式化流水线结合,构建了数学函数形式化库(FLMF),这是美国国家标准与技术研究院数字数学函数库(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 results also identifies translation and source defects in existing datasets. Code available at https://github.com/annamei1/FLMF-Ch7ErrFunc-Release.git.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑