详细内容或原文请订阅后点击阅览
希尔伯特：递归通过非正式推理建立正式的证据
大型语言模型 (LLM) 展示了令人印象深刻的数学推理能力，但它们的解决方案经常包含无法自动验证的错误。 Lean 4 等形式化定理证明系统提供了完全准确的自动验证，推动了最近努力构建专门的证明者法学硕士，以形式语言生成可验证的证明。然而，仍然存在一个重大差距：当前的证明者法学硕士解决的问题比使用自然语言操作的通用法学硕士要少得多。我们介绍 Hilbert，一个代理框架，它通过以下方式弥合了这一差距
来源:Apple机器学习研究大型语言模型 (LLM) 展示了令人印象深刻的数学推理能力，但它们的解决方案经常包含无法自动验证的错误。 Lean 4 等形式化定理证明系统提供了完全准确的自动验证，推动了最近努力构建专门的证明者法学硕士，以形式语言生成可验证的证明。然而，仍然存在一个重大差距：当前的证明者法学硕士解决的问题比使用自然语言操作的通用法学硕士要少得多。我们引入了希尔伯特（Hilbert），这是一个代理框架，它通过结合非正式推理和形式验证的互补优势来弥补这一差距。我们的系统协调了四个组件：擅长数学推理的非正式 LLM、针对精益 4 策略优化的专业证明者 LLM、正式验证器和语义定理检索器。给定证明者无法解决的问题，希尔伯特采用递归分解将问题分解为使用证明者或推理者 LLM 解决的子目标。它利用验证者的反馈来根据需要完善不正确的证明。实验结果表明，Hilbert 在关键基准测试上明显优于现有方法，在 miniF2F 上达到 99.2%，比最佳公开可用方法高出 6.6%。希尔伯特在 PutnamBench 上取得了最著名的结果。它解决了 462/660 个问题 (70.0%)，优于 SeedProver (50.4%) 等专有方法，并且比最佳公开可用基线提高了 422%。因此，希尔伯特有效地缩小了非正式推理和正式证明生成之间的差距。
- † 加州大学圣地亚哥分校** 在 Apple 期间完成的工作