Discover and Prove：面向Lean 4硬模式自动定理证明的开源代理框架
人工智能
2026-04-20 v1 计算与语言
计算机科学中的逻辑
摘要
大多数自动定理证明基准将最终答案嵌入形式化陈述中——我们称这种设计为“易模式”，其相对于人类竞争者所面临的任务而言具有简化优势，可能导致对模型能力的乐观估计。我们称更严格、更贴近现实的设定称为“硬模式”：系统必须独立发现答案，然后再构建形式化证明。为支持硬模式研究，我们做出两项贡献：第一，发布MiniF2F-Hard和FIMO-Hard，这两个广泛使用的自动定理证明基准的硬模式变体；第二，引入Discover And Prove（DAP）——一个使用LLM自然语言推理并结合显式自省发现答案，然后将硬模式陈述重写为易模式，以适用于现有自动定理证明器的代理框架。DAP取得了最新的SOTA成绩：在CombiBench上解决的问题数从7个（前一SOTA，Pass@16）提升至10个；在PutnamBench上，DAP首次在硬模式下正式证明了36个定理——同时揭示了SOTA LLMs在相同问题上超过80%的答案准确率，而形式化证明器仅 manage不到10%，暴露了硬模式基准独特适用于衡量的巨大鸿沟。
引用
@article{arxiv.2604.15839,
title = {Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4},
author = {Chengwu Liu and Yichun Yin and Ye Yuan and Jiaxuan Xie and Botao Li and Siqi Li and Jianhao Shen and Yan Xu and Lifeng Shang and Ming Zhang},
journal= {arXiv preprint arXiv:2604.15839},
year = {2026}
}
备注
ACL 2026 Main Conference