我们引入了 Goedel-Architect, ，这是一个在 Lean 4 中以蓝图生成和细化为中心的形式定理证明的代理框架。蓝图是构建主定理的定义和引理的依赖图。 First, Goedel-Architect 生成正式声明的定义和引理, 以及声明的依赖项的蓝图。该蓝图可选地由自然语言证明来指导。然后, 配备工具的精益证明器组件使用相关依赖项并行关闭每个开放引理节点。失败的引理反过来又推动了全球蓝图的完善。该策略与其他使用递归引理分解, 的主流方法形成鲜明对比，并且可能会在死胡同策略上低效循环。使用开放权重 DeepSeek-V4-Flash (284B-A13B) 作为骨干, Goedel-Architect 在 MiniF2F 测试中获得 99.2% pass@1，在 PutnamBench 上获得 75.6% pass@1。通过可选的自然语言证明，为更难的问题奠定了初始蓝图,，我们另外解决了剩余的两个 MiniF2F 测试问题 (，达到 100%), 将 PutnamBench 提升到 88.8% (597/672), 并解决了 IMO 2025, 上的 4/6 和 Putnam 上的 11/12 USAMO 2026 上的 2025, 和 3/6。这代表了开源管道的最先进性能，而价格比同类开源管道低 500 倍。
We introduce Goedel-Architect, an agentic framework for formal theorem proving in Lean 4 centered on blueprint generation and refinement. A blueprint is a dependency graph of definitions and lemmas that builds up to the main theorem. First, Goedel-Architect generates a blueprint of formally stated definitions and lemmas, along with declared dependencies. This blueprint is optionally guided by a natural language proof. Then, a tool-equipped Lean prover component closes each open lemma node in parallel using relevant dependencies. Failed lemmas in turn drive refinement of the global blueprint. This strategy contrasts with other mainstream approaches which use recursive lemma decomposition, and can inefficiently loop on dead-end strategies. Using the open-weight DeepSeek-V4-Flash (284B-A13B) as the backbone, Goedel-Architect attains 99.2% pass@1 on MiniF2F-test and 75.6% pass@1 on PutnamBench. With an optional natural-language proof seeding the initial blueprint on the harder problems, we additionally close the remaining two MiniF2F-test problems (reaching 100%), lift PutnamBench to 88.8% (597/672), and solve 4/6 on IMO 2025, 11/12 on Putnam 2025, and 3/6 on USAMO 2026. This represents state-of-the-art performance for an open-source pipeline at a price point up to 500x less than comparable open-source pipelines.
科目:人工智能(cs.AI)
Subjects: Artificial Intelligence (cs.AI)