大模型推理能力

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

发现与证明：一个开源代理框架用于Lean 4中的硬模式自动定理 proving

Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang

机构 * State Key Laboratory for Multimedia Information Processing, School of Computer Science, PKU-Anker LLM Lab, Peking University（信息处理国家重点实验室，计算机科学学院，PKU-Anker LLM实验室，北京大学） ； Huawei Technologies Co., Ltd.（华为技术有限公司） ； School of Software & Microelectronics, Peking University（软件与微电子学院，北京大学） ； School of Electronics Engineering and Computer Science, Peking University（电子工程与计算机科学学院，北京大学） 纠错

专题命中 代码与定理证明 ：reasoning(abstract)；分类 cs.CL、cs.AI

AI总结 本文提出DAP框架，通过LLM自然语言推理与自我反思发现答案，并将硬模式问题转换为易模式问题以提升自动定理证明性能，实现了CombiBench和PutnamBench上的显著提升。

Comments ACL 2026 Main Conference