Hilbert：利用非形式化推理递归构建形式化证明
人工智能
2026-03-18 v2 形式语言与自动机理论
机器学习
摘要
大型语言模型（LLMs）展示了令人印象深刻的数学推理能力，但其解决方案经常包含无法自动检查的错误。像Lean 4这样的形式化定理证明系统提供了完全准确的自动验证，这推动了近期构建专用证明器LLM的努力，这些LLM能够生成形式化语言的可验证证明。然而，一个显著的差距仍然存在：当前的证明器LLM解决的问题远少于在自然语言中运行的通用LLM。我们引入了Hilbert，这是一个智能体框架，通过结合非形式化推理和形式化验证的互补优势来弥合这一差距。我们的系统协调四个组件：一个擅长数学推理的非形式化LLM，一个针对Lean 4策略优化的专用证明器LLM，一个形式化验证器，以及一个语义定理检索器。给定一个证明器无法解决的问题，Hilbert采用递归分解将问题拆分为子目标，并用证明器或推理器LLM来解决。它利用验证器反馈来根据需要优化不正确的证明。实验结果表明，Hilbert在关键基准上显著优于现有方法，在miniF2F上达到99.2%，比最佳公开可用方法高出6.6个百分点。Hilbert在PutnamBench上取得了来自公开可用模型的**最强已知结果**。它解决了462/660个问题（70.0%），优于SeedProver（50.4%）等专有方法，并比最佳公开可用基线提高了422%。因此，Hilbert有效地缩小了非形式化推理与形式化证明生成之间的差距。代码可在https://github.com/Rose-STL-Lab/ml-hilbert获取。
引用
@article{arxiv.2509.22819,
title = {Hilbert: Recursively Building Formal Proofs with Informal Reasoning},
author = {Sumanth Varambally and Thomas Voice and Yanchao Sun and Zhifeng Chen and Rose Yu and Ke Ye},
journal= {arXiv preprint arXiv:2509.22819},
year = {2026}
}