arXiv · ML· Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata, Benjamin Mikek, Murali Krishna Ramanathan, Hao Zhou·· 6 小时前精选AI 评分76
Maestro：基于协调的代理式形式化证明开发
Maestro: Agentic Formal Proof Development by Coordination
AI 导读
Maestro 是一个 Lean 证明框架，通过让证明器报告失败原因并由协调器进行全局响应（如引导、修正假引理或重新规划），克服了现有系统盲目分解导致失败的问题。
推荐理由
原文明确给出 Maestro 在全局协调机制下对多种基准的量化提升，读者可直接对比其与普通编码智能体的表现差异。
来源：arXiv · ML · arxiv.org