中文内容
已翻译professional source英文原文2026-06-06
计算机科学 > 人工智能
[提交于 2026 年 6 月 4 日]
标题：Goedel-Architect：通过蓝图生成与精化简化形式化定理证明
作者：Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora
View PDF
HTML (experimental)
摘要：我们介绍 Goedel-Architect，这是一个用于 Lean 4 形式化定理证明的智能体框架，核心是蓝图生成与精化。蓝图是由定义和引理组成的依赖图，逐步构建至主定理。首先，Goedel-Architect 生成一个由形式化陈述的定义和引理以及声明的依赖关系构成的蓝图。该蓝图可选择由自然语言证明引导。随后，一个配备工具的 Lean 证明器组件利用相关依赖并行关闭每个开放的引理节点。失败的引理反过来推动全局蓝图的精化。这一策略不同于其他主流方法；后者使用递归引理分解，可能低效地陷入死胡同策略循环。以开放权重 DeepSeek-V4-Flash (284B-A13B) 作为骨干模型，Goedel-Architect 在 MiniF2F-test 上达到 99.2% pass@1，在
Subjects:
人工智能（cs.AI）
Cite as:
arXiv:2606.06468 [cs.AI]
(or
arXiv:2606.06468v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2606.06468
聚焦以了解更多
arXiv-issued DOI via DataCite (pending registration)
参考文献与引用
- 正文：NASA ADS
- 正文：Google Scholar
- 正文：Semantic Scholar
export BibTeX citation
加载中...
收藏
Bibliographic Tools
Code, Data, Media
Demos
Related Papers
About arXivLabs
书目与引用工具
书目浏览器切换
书目浏览器 (What is the Explorer?)
Connected Papers 切换
正文：Connected Papers (What is Connected Papers?)
Litmaps 切换
正文：Litmaps (What is Litmaps?)
scite.ai 切换
scite 智能引用 (What are Smart Citations?)
与本文相关的代码、数据和媒体
alphaXiv 切换
正文：alphaXiv (What is alphaXiv?)
代码链接切换
CatalyzeX 论文代码查找器 (What is CatalyzeX?)
DagsHub 切换
正文：DagsHub (What is DagsHub?)
GotitPub 切换
正文：Gotit.pub (What is GotitPub?)
Huggingface 切换
正文：Hugging Face (What is Huggingface?)
ScienceCast 切换
正文：ScienceCast (What is ScienceCast?)
演示
Replicate 切换
正文：Replicate (What is Replicate?)
Spaces 切换
正文：Hugging Face Spaces (What is Spaces?)
Spaces 切换
正文：TXYZ.AI (What is TXYZ.AI?)
推荐与搜索工具
影响力之花链接
正文：Influence Flower (What are Influence Flowers?)
CORE 推荐器 (What is CORE?)
- 作者
- 发表场所
- 机构
- 主题
arXivLabs：与社区合作者开展的实验性项目
arXivLabs 是一个框架，允许合作者直接在我们的网站上开发和分享新的 arXiv 功能。
与 arXivLabs 合作的个人和组织都认同并接受我们关于开放、社区、卓越和用户数据隐私的价值观。arXiv 致力于这些价值观，并且只与遵循这些价值观的合作伙伴合作。
有能为 arXiv 社区增加价值的项目想法吗？进一步了解 arXivLabs。