arXiv · cs.AI· Debargha Ganguly·· 2 天前精选AI 评分52
EasyProver：面向真实代码验证的 Lean 定理证明系统与 Aegis 基准生成管线
Scaling Lean Theorem Proving for Real-World Code Verification
来源与原文
arXiv · cs.AI
作者：Debargha Ganguly
发布时间：（北京时间）
阅读原始来源 · arxiv.org ↗完整链接与内容说明
https://arxiv.org/abs/2610.38174v1
本站目前仅有 AI 导读与摘要，未展示原文正文；技术细节、代码和完整结论请查看原始来源。
AI 导读
论文提出 EasyProver，一个由递归智能体、异步搜索、并行策略探测和弹性 elaboration 服务组成的 Lean 证明系统，用现成前沿模型、无额外训练，解出 669/672 PutnamBench、全部 6 题 IMO 2026 形式化、597/600 NTP4VC 验证条件和 189 道 VERINA 全部任务。针对基准饱和问题，团队推出 Aegis 管线，将竞赛编程题经安全 Rust 实现、Aeneas 翻译和规格生成转成更难的验证任务，产出 2,045 对差分验证的 Rust-Lean 程序对和 11,533 条候选规格；在 2,000 条分层样本上 EasyProver 以每条 30 分钟预算证明 1,054 条（52.7%）。
推荐理由
在既有定理证明基准接近饱和时，论文给出把竞赛题转成真实代码验证任务的新数据管线，并提供可复用的验证环境。
来源：arXiv · cs.AI · arxiv.org