提出新框架DAP，在硬模式下自动发现并证明定理，突破现有模型瓶颈。
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
- 用LLM自我反思生成推理路径，先发现答案再转为可证形式
- 在CombiBench上解题数从7提升至10，在PutnamBench首次证明36个定理
- 揭示大模型答对率超80%但形式证明率不足10%的显著差距
当前大多数自动定理证明（ATP）基准将答案嵌入命题中，这种设计称为'易模式'，简化了任务且可能高估模型能力。我们提出更严格、更贴近人类挑战的'硬模式'：系统需先独立发现结论，再构建形式化证明。为推动硬模式研究，我们发布了两个经专家标注的硬模式变体数据集——MiniF2F-Hard和FIMO-Hard。同时提出发现与证明（Discover And Prove, DAP）框架，利用大语言模型进行自然语言推理并结合显式自我反思，实现答案发现，并将硬模式命题转化为易模式形式供已有定理证明器处理。DAP达到新纪录：在CombiBench上解题数从7（前最优，Pass@16）增至10；在PutnamBench上首次正式证明36个定理。同时发现，顶尖大模型在相同问题上的答案准确率超过80%，而形式证明器成功率低于10%，暴露出硬模式基准的独特测量优势。
原文摘要 · Abstract (English)
Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability. We call the stricter, more realistic setting "Hard Mode": the system must independently discover the answer before constructing a formal proof. To enable Hard Mode research, we make two contributions. First, we release MiniF2F-Hard and FIMO-Hard, expert-reannotated Hard Mode variants of two widely-used ATP benchmarks. Second, we introduce Discover And Prove (DAP), an agentic framework that uses LLM natural-language reasoning with explicit self-reflection to discover answers, then rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. DAP sets the state of the art: on CombiBench it raises solved problems from 7 (previous SOTA, Pass@16) to 10; on PutnamBench it is the first system to formally prove 36 theorems in Hard Mode -- while simultaneously revealing that state-of-the-art LLMs exceed 80% answer accuracy on the same problems where formal provers manage under 10%, exposing a substantial gap that Hard Mode benchmarks are uniquely suited to measure.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。