Hilbert: Recursively Building Formal Proofs with Informal Reasoning
大型语言模型 (LLM) 展示了令人印象深刻的数学推理能力，但它们的解决方案经常包含无法自动验证的错误。 Lean 4 等形式化定理证明系统提供了完全准确的自动验证，推动了最近努力构建专门的证明者法学硕士，以形式语言生成可验证的证明。然而，仍然存在一个重大差距：当前的证明者法学硕士解决的问题比使用自然语言操作的通用法学硕士要少得多。我们介绍 Hilbert，一个代理框架，它通过以下方式弥合了这一差距
