自动定理证明中的“苦涩教训”初探
非形式数学的进展往往来自扩大语言模型和智能体推理的规模，而形式定理证明则常依赖人工设计的工作流。本研究探讨，增加推理时计算量的简单智能体循环能否与这些工作流媲美。h1 系统将模型接入 Lean 4，利用验证器反馈和自我反思，不强制采用特定的分解或搜索结构。它在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上取得领先成绩，并解决了八个未解问题。在模型相同的对比中，其表现达到或超过专用工作流。研究还发现，简化本身并不足够：高效的 Lean 接口对成本和解题率影响显著。
本文来源：Hugging Face，仅供学习参考，版权归原作者所有。