摘要
本文介绍 Goedel-Architect，一个面向 Lean 4 形式化定理证明的智能体框架，核心在于蓝图的生成与细化。蓝图是由定义和引理构成的依赖图，逐步构建至主定理。系统首先生成包含形式化陈述及依赖关系的蓝图，可选由自然语言证明引导；随后利用配备工具的证明器并行闭合引理节点，失败案例驱动全局蓝图细化。该策略避免了传统递归分解的低效死循环。基于 DeepSeek-V4-Flash，该方法在 MiniF2F-test 和 PutnamBench 上取得最先进性能，显著降低计算成本。
AI 推荐理由
论文核心提出基于蓝图生成与细化的规划框架，通过依赖图分解定理证明任务，属典型规划机制研究。
研究机构
Equal contribution
Princeton University
论文信息