大模型推理能力

Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs

规划锤击：面向自动化Rocq证明的难度感知分解

Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, Xiaoxing Ma

专题命中 代码与定理证明 ：planning(title,abstract)

AI总结 提出Quarry框架，通过LLM规划证明分解并利用难度模型排序子目标，结合CoqHammer自动证明，在Rocq基准测试中成功率提升7%-13%。

Comments 26 pages, 8 figures; submitted to OOPSLA 2026

Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro

使用GPT-5.5 Pro对实数上的和积猜想进行自主反证

Yichen Huang

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

AI总结 本文借助GPT-5.5 Pro构建智能体，通过三阶段提示管道，对实数上的和积猜想进行自主反证，8次试验中7次成功生成正确证明，每次试验平均用132.4k推理令牌，还发布相关内容供重现研究。