Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
本文介绍了 KG-prover，这是一个新颖的框架，它通过从数学文本中挖掘知识图谱来增强通用大型语言模型，以提升自动定理证明能力，并在多个数据集上展示了显著的性能提升，且无需额外的微调。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
以下是论文《为自动化定理证明扩展基于自然语言的图推理测试时计算》的解释，将其拆解为简单概念并辅以富有创意的类比。
核心思想：给数学模型一张“作弊小抄”
想象你正在尝试解决一道极其困难的数学谜题。你有一位超级聪明的朋友（大型语言模型，或称 LLM），他精通数学，但有时也会陷入困境，因为他记不住某条特定规则，或者无法看清两个不同概念之间的联系。
通常，为了让这些朋友变得更聪明，你必须送他们回学校接受数年的训练（微调）。但这篇论文提出：“无需额外上学！”相反，我们可以在他们解题的同时，给他们提供一张更好的地图和一座更好的图书馆。
作者构建了一个名为KG-Prover的系统。这就像给你的聪明朋友提供一张巨大的、相互连接的数学事实网络（知识图谱），并让他们在尝试解谜时能够实时“查阅”正确的线索。
工作原理：侦探类比
将人工智能想象成一名试图侦破案件（数学定理）的侦探。
- 案发现场（问题）：侦探被赋予一个陈述，需要证明其为真。
- 图书馆（知识图谱）：作者从ProofWiki（一个充满数学证明的网站）构建了一座庞大的图书馆。他们将这座图书馆转化为一张巨大的蜘蛛网，其中每个数学概念都是一个节点，连接它们的线条展示了它们之间的关系（例如，“定理 A 使用了定义 B"）。
- 调查（搜索）：
- 侦探不再靠猜测，而是查看这张蜘蛛网。
- 他们从案发现场出发，问道：“谁与这个相关？”
- 他们沿着线条寻找相似的概念、定义和先前的证明。
- 如果陷入困境，他们不会放弃；而是深入网络，跟随更多线条以寻找隐藏的线索。这被称为“扩展测试时计算”——基本上，就是在调查过程中投入更多的时间和精力来寻找答案。
- 草稿（非形式化证明）：侦探利用找到的线索，用通俗英语（自然语言）写下解决方案的草稿。
- 翻译（形式化）：一位专门的翻译员（另一个 AI）将那份英语草稿转化为严格的、计算机可读的代码（Lean 4）。
- 法官（验证）：一位严格的裁判检查代码。如果代码有误，侦探会收到关于出错的提示，然后回到蜘蛛网，寻找新线索，再次尝试。
奏效的“作弊”手段
论文声称，通过执行这种“搜索与检索”过程，他们无需重新训练 AI 模型。他们只是使用了现有的通用模型（如 GPT-4o-mini 或 Llama 3），并让它们使用这张地图。
结果：
- 分数提升：当他们添加了这张“蜘蛛网地图”后，AI 在数学问题上的成功率显著提高（根据测试不同，提升了 2% 到 21%）。
- “深潜”效应：AI 被允许在图谱中搜索得越深（跟随更多连接），它在解决难题方面就越出色。这就像是在说：“如果你一分钟内解不出来，那就花十分钟，把图书馆里所有相关的书都看一遍。”
- 无需额外训练：最大的胜利在于，他们无需花费数百万美元去训练新模型。他们只是让旧模型在工作时拥有了更好的工具。
局限性（侦探陷入困境之处）
论文诚实地指出了该方法失效的地方：
- 翻译鸿沟：有时侦探写出了完美的英语解释，但翻译员在将其转化为严格代码时搞砸了。数学逻辑是正确的，但计算机语言的“语法”却是错误的。
- 线索缺失：如果答案需要某个极其冷门的数学事实，而该事实不在他们的图书馆（ProofWiki）中，那么无论侦探搜索得有多深，都无法找到它。
- 噪音过多：如果蜘蛛网过于杂乱，侦探可能会因不相关的信息而感到困惑。
总结
这篇论文介绍了一种无需重新训练即可让 AI 数学专家变得更聪明的方法。这就像给一位天才学生一部装有完美互联百科全书的智能手机，并告诉他：“慢慢来，查阅你需要的每一个相关事实，然后写出证明。”通过让 AI 在测试过程中“更深入地思考”并深入搜索其知识图谱，它就能更正确地解决更多问题。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。