AITOP

5月20日

15:41

arXiv cs.AI@Gabriel Rongyang Lau

精选58

本文报告了使用Aristotle API对IMO 2009第6题（Grasshopper问题）进行Lean 4形式化证明的案例。生成的代码包含一个广义定理的Lean版本、四个已验证的辅助引理，但主定理的证明中有一个未解决的“sorry”占位符。已验证的部分建立了局部数学性质，但全局组合计数步骤未被自动化证明覆盖。该案例揭示了AI辅助形式化的核心局限：局部证明搜索可以成功，但全局推理仍需人工介入。论文提供了可复现的Lean代码，并分析了已验证与未验证的证明内容。

论文定理证明 Lean 4 Aristotle API 形式化验证 IMO问题

推荐理由：这个案例对做AI辅助形式化验证的团队很有参考价值——它清晰展示了当前AI在局部引理证明上的能力，以及全局推理的瓶颈，做Lean或定理证明器开发的值得点开看看。

5月19日

09:57

arXiv cs.AI@Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen

精选58

CAM-Bench是一个新的Lean 4定理证明基准，包含1000个计算与应用数学领域的证明目标，涵盖优化、数值线性代数和数值分析。这些题目改编自教科书习题，依赖局部定义、符号和算法。研究者开发了依赖恢复管道，将每个问题标准化为独立定理并翻译成Lean目标。该基准填补了现有形式化数学基准（如IMO风格问题）的空白，聚焦于应用数学中依赖教科书概念和初等定理的题目。评估显示，现有大模型和形式化代理在跟踪局部假设、应用初等结果、分解证明和长期控制方面存在常见失败模式。

论文定理证明 Lean 4 基准测试应用数学形式化验证

推荐理由：做形式化验证或AI数学推理的团队终于有了应用数学方向的专用基准，比纯代数题更贴近实际工程场景，建议关注其失败模式分析来改进模型。

5月18日

12:14

arXiv cs.AI@Augusto B. Corrêa, André G. Pereira, Jendrik Seipp

精选63

本文提出一种属性引导的LLM程序合成方法，用于PDDL规划领域。传统方法依赖简单分数（如测试通过数）评估程序，缺乏失败原因反馈，导致大量无效生成和评估。新方法在程序违反形式化属性时立即停止评估，并返回具体反例，引导LLM修复。在10个规划域上的实验表明，该方法平均每个域生成程序数减少7倍，无需搜索即可解决更多任务，评估计算量降低数个数量级。该方法适用于任何存在可验证属性的问题，能显著降低成本并提升程序质量。

论文程序合成 LLM 规划形式化验证 PDDL

推荐理由：做AI规划或程序合成的团队，这篇论文提供了一种减少LLM调用次数、提升生成效率的实用方法——用形式化属性替代分数反馈，直接给反例引导修复，值得点开看看具体实现。