论文页面 - h1: 自动化定理证明中的苦涩教训初探

来源：https://huggingface.co/papers/2610.35962

摘要

一个借助高效 Lean 反馈的简单智能体循环，在无需结构化工作流的情况下实现了最先进的形式化定理证明，表明执行接口比复杂的编排更为重要。

虽然非形式化数学的进展主要来自前沿语言模型在思维链和智能体推理上的规模化，但形式化定理证明（https://huggingface.co/papers?q=formal%20theorem%20proving）却日益依赖围绕这些模型的人类设计工作流，例如规划、分解以及编排专门的证明器。这引出了一个“苦涩的教训“式的问题：一个能规模化测试时计算（https://huggingface.co/papers?q=test-time%20compute）的简单智能体循环（https://huggingface.co/papers?q=agentic%20loop）能否匹敌这些工作流？这个问题至关重要，因为形式化验证必须不断扩展，才能跟上前沿模型产出研究级数学内容的步伐，而新的工作流很少能真正解决这一问题，因为它们的收益往往与更强的模型或更多的计算量混杂在一起。我们使用 h1 来研究这一问题。h1 是一个简单的工具框架，它为模型提供了一个与 Lean 4（https://huggingface.co/papers?q=Lean%204）交互的高效接口，并通过验证器反馈（https://huggingface.co/papers?q=verifier%20feedback）和自我反思（https://huggingface.co/papers?q=self-reflection）让模型持续工作，而不强加任何分解或搜索结构。h1 在 PutnamBench（https://huggingface.co/papers?q=PutnamBench）、FATE-X（https://huggingface.co/papers?q=FATE-X）和 FormalConjectures（https://huggingface.co/papers?q=FormalConjectures）100-Solved 上达到了最先进的结果，在 FormalConjectures（https://huggingface.co/papers?q=FormalConjectures）中解决了八个开放问题，并且在相同模型条件下，匹配或超越了 Goedel-Architect（https://huggingface.co/papers?q=Goedel-Architect）和 AlphaProof Nexus（https://huggingface.co/papers?q=AlphaProof%20Nexus）等专门工作流。令人惊讶的是，这表明单次尝试（pass@1）往往也能扩展到足以解决开放问题的程度。通过消融实验以及与 Claude Code（https://huggingface.co/papers?q=Claude%20Code）和 AxProverBase（https://huggingface.co/papers?q=AxProverBase）在相同模型条件下的对比，我们发现仅仅简单是不够的：一个高效的 Lean 接口在很大程度上决定了成本和求解率。因此我们建议，未来的工作在预设工作流之前，应先使用高效执行反馈来评估前沿模型，否则可能重蹈苦涩的教训。

查看 arXiv 页面（https://arxiv.org/abs/2610.35962）查看 PDF（https://arxiv.org/pdf/2610.35962）添加到收藏（https://huggingface.co/login?next=%2Fpapers%2F2610.35962）

引用此论文的模型 0

没有模型关联此论文

在模型 README.md 中引用 arxiv.org/abs/2610.35962 即可从此页面关联。

引用此论文的数据集 0

没有数据集关联此论文

在数据集 README.md 中引用 arxiv.org/abs/2610.35962 即可从此页面关联。

引用此论文的 Spaces 0

没有 Space 关联此论文

在 Space README.md 中引用 arxiv.org/abs/2610.35962 即可从此页面关联。

包含此论文的合集 0

没有合集包含此论文

将此论文添加到合集（https://huggingface.co/new-collection）即可从此页面关联。