Hilbert: Recursively Building Formal Proofs with Informal Reasoning

大型语言模型（LLM）展现出令人印象深刻的数学推理能力，但其解题过程常包含难以自动验证的错误。而Lean 4等形式化定理证明系统则能提供完全精确的自动化验证，这也促使近期研究致力于构建能够生成可验证形式化证明的专用证明型大模型。然而，目前仍存在显著差距：现有的证明型大模型所解决的问题数量远少于在自然语言环境下运行的通用大模型。为此，我们提出了Hilbert——一种智能体框架，通过融合非形式化推理与形式化验证的互补优势，弥合了这一鸿沟。我们的系统协调四个组件协同工作：擅长数学推理的非形式化大模型、专为Lean 4策略优化的专用证明型大模型、形式化验证器以及语义定理检索器。当面对证明器无法直接解决的问题时，Hilbert采用递归分解方法，将原问题拆分为若干子目标，并调用证明器或推理型大模型逐一求解；同时利用验证器的反馈信息，必要时对错误的证明进行修正。实验结果表明，Hilbert在关键基准测试中显著超越现有方法，在miniF2F上达到99.2%的准确率，比此前最佳公开方法高出6.6个百分点；在PutnamBench上取得了当前最优结果，成功解决了660道题目中的462道（70.0%），优于SeedProver等专有方法（50.4%），相比最佳公开基线实现了422%的性能提升。因此，Hilbert有效缩小了非形式化推理与形式化证明生成之间的差距。

如何有效结合大型语言模型（LLM）的数学推理能力与形式化证明系统的精确验证能力，以提升自动定理证明的性能。当前的专用证明器LLM在解决数学问题的数量上远不如通用LLM，存在显著性能差距。这是一个重要且尚未充分解决的问题，尤其在确保生成证明的正确性同时保持高解题覆盖率方面。

提出Hilbert，一种代理式框架，通过协同调度四个组件——擅长非正式数学推理的LLM、专精Lean 4战术的证明生成LLM、形式化验证器和语义定理检索器——实现非正式推理与形式化验证的融合。核心创新在于递归分解难题为可验证子目标，并利用验证反馈迭代修正错误证明，从而弥合非正式推理与形式化证明之间的鸿沟。

在miniF2F基准上达到99.2%准确率，超越此前最佳公开方法6.6个百分点；在PutnamBench上解决462/660题（70.0%），优于SeedProver（50.4%）并相较最优公开基线提升422%。实验设计系统性强，涵盖多个权威数学推理基准。论文展示了闭环验证与任务分解对性能提升的关键作用。目前未明确提及代码是否开源，值得后续关注。未来方向包括扩展至其他形式化系统、增强子目标分解策略及提升检索效率。

相关研究包括：'LeanDojo: An Open-Source Toolkit for Interactive Proof Generation with Large Language Models'（2023）、'Towards Formal Proof Automation with Large Language Models'（2024）、'NaturalProofs: Mathematical Theorem Proving in Natural Language'（2022）、'ProofNet: A Benchmark for Autoformalization and Formal Reasoning'（2023）以及'SeedProver: A Scalable Framework for Automated Formal Theorem Proving via Iterative Refinement'（2024）。这些工作共同推动了LLM在形式化推理中的应用，但多数仍受限于生成证明的正确性或覆盖率。