💻 computer science

Self-Supervised Theorem Discovery in a Formal Axiomatic System

本文提出了一种自我监督智能体，它仅从公理和推理规则出发，即可自主发现数以万计的有意义定理并解决人类基准问题，证明了有用的数学知识可以在没有人类先验知识的情况下涌现，并能有效增强大语言模型的推理能力。

原作者： Kazuki Ota, Takayuki Osa, Tatsuya Harada

发布于 2026-06-30

📖 1 分钟阅读☕ 轻松阅读

原作者： Kazuki Ota, Takayuki Osa, Tatsuya Harada

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一个机器人做数学，但有一个非常严格的规则：你不能给机器人任何教科书、没有已解题目的示例，也没有已知事实的“小抄”。 你只能给它最基本的底线：一些基本的逻辑规则（比如“如果 A 为真，且 A 蕴含 B，那么 B 为真”）和一个空白的起点。

这个问题是这篇论文所探讨的：这个机器人能否仅仅通过玩转这些基本规则，就学会自我发现新的、有用的数学事实？

以下是研究人员如何构建这个机器人并取得成就的过程，通过简单的类比进行解释。

1. 游戏：一叠积木

研究人员使用一个被称为“希尔伯特逻辑”（Hilbert Logic）的系统为机器人设置了一个游戏。你可以把这个系统想象成一个由一叠积木组成的系统。

规则： 机器人有三种特殊的积木（公理）可以拿起并放在堆叠中。它还有一个组合积木的规则：如果它看到一个写着“如果 X，那么 Y”的积木放在一个写着“X”的积木之上，它可以将它们替换为一个写着“Y”的积木。
目标： 机器人被给定一个目标积木（定理），并且必须找出在堆叠上构建出这个特定积木的确切动作序列。

2. 策略：“我以后再试”

机器人开始尝试随机移动。大多数情况下，它无法达到被给予的特定目标。然而，研究人员给了机器人一个聪明的技巧，叫做自监督学习（Self-Supervised Learning）。

想象机器人正在尝试建造一座塔来触及一面红旗（目标）。它失败了，没能触及红旗，但在过程中，它意外地在半空中搭建了一个非常坚固的蓝色平台。

技巧： 机器人并没有把那个蓝色平台扔掉，而是说：“嘿，我刚刚造出了一个蓝色平台！让我们把它作为下次的目标。”
循环： 机器人将这个蓝色平台保存为一个“目标”。稍后，它会再次尝试构建这个蓝色平台。每当它成功时，它就会学会实现它的确切步骤。随着时间的推移，机器人构建了一个庞大的这些“平台”（定理）的库。

3. 挑选最好的工具

机器人发现了数以千计的这些平台。但并非所有平台都是有用的。有些太过于特殊（比如一个只适合一块微小砖块的平台），有些则只是它已经知道的事物的重复。

机器人使用两个过滤器来挑选“黄金工具”：

通用性（Generality）： 它保留那些用途广泛的平台（比如一张平坦的桌子），并丢弃那些过于古怪或特殊的平台。
难度（Difficulty）： 它寻找那些从头开始构建很困难的平台。如果机器人在利用基本规则构建特定平台时感到吃力，那么这个平台就是一个“难题”。机器人决定将这个难题添加到它的工具箱中，作为一个预制工具（引理/lemma）。

4. 结果：一个不断增长的库

在运行了几个“世代”（学习轮次）之后，机器人最终拥有了一个包含数万个自我发现的数学事实的库。

研究人员通过两种方式测试了它：

机器人能解决人类的问题吗？ 他们给了机器人一组由人类编写的 30 个经典逻辑谜题（出自教科书）。机器人利用其自建的库，成功解决了其中的 30%。这令人印象深刻，因为它从未见过这些谜题，也没有人类的帮助。
它能帮助其他机器人吗？ 研究人员将机器人发现的“黄金工具”作为“提示”提供给另一个非常聪明的 AI（一个大型语言模型，如 GPT）。当这个其他 AI 被允许使用这些自我发现的工具时，它在解决逻辑谜题方面表现得更好。

大局观

这篇论文证明了，你不需要由人类向 AI 递交数学事实库。如果你只给 AI 游戏的规则，它就可以玩游戏、发现自己的捷径，并建立自己的知识库。

这就像一个孩子学习用乐高积木。如果你只给他们一些基础积木和一条指令“把它们拼在一起”，他们最终可能会自己摸索出如何建造一座复杂的城堡，然后意识到：“哦，我造出的这个特定的拱形形状对于做门非常有用”，并开始将这个拱形作为未来所有城堡的标准部件来使用。

这篇论文并没有声称：

它并未声称机器人现在就能做高等微积分或物理。
它并未声称这套方法立即适用于所有类型的数学（他们仅在命题逻辑上进行了测试）。
它并未声称这会取代数学家，而是展示了 AI 进化其自身形式化知识的一种路径。

简而言之：AI 从零开始自学了数学，建立了属于自己的有用事实字典，并证明了这些事实确实有助于解决现实问题。

技术摘要：形式化公理系统中的自监督定理发现

问题陈述

尽管最近的 AI 系统（特别是大语言模型，LLMs）在数学推理方面展现出了显著进展，但它们在很大程度上依赖于人类提供的先验知识，如数学文本、代码和现有的定理库。一个关键的开放性问题仍然存在：一个智能体能否仅从形式化公理系统的原始规则出发，在不依赖人类先验知识、现有定理库或训练问题集的情况下，自主发现有用的定理？

目前的方法通常依赖于人类构建的知识来引导推理过程。即使是在公理领域进行自我改进的智能体，也往往需要外部判别器来评估所发现定理的效用。本文研究了一个智能体是否不仅能发现定理，还能识别并利用“有用”的定理，以改进其自身的证明搜索过程以及外部推理系统的性能，且完全仅依赖于公理和推理规则。

方法论

1. 形式化设定：作为栈机（Stack Machine）的希尔伯特系统

作者在命题逻辑的希尔伯特公理系统中实例化了这一问题。该系统被刻意设计得极其精简，由以下部分组成：

三个公理：
- $Ax1: A \to (B \to A)$ （弱化）
- $Ax2: (A \to (B \to C)) \to ((A \to B) \to (A \to C))$ （分配）
- $Ax3: (\neg A \to \neg B) \to (B \to A)$ （逆否）
一个推理规则： 肯定前件式（Modus Ponens, MP），从 $X$ 和 $X \to Y$ 中导出 $Y$ 。

为了便于学习，作者将定理证明形式化为一个确定性的、目标条件的栈机决策过程 $(S, A, s_0, P)$ ：

状态 ( $S$ )： 公式的一个有限栈。
动作 ( $A$ )： 将 $Ax1, Ax2, Ax3$ 的实例压入栈中，或者应用肯定前件式（MP）。
机制： MP 动作使用 Hindley–Milner 统一化（Unification）。如果栈顶元素与 $X \to Y$ 统一，且其下方的元素与 $X$ 统一，则弹出这两个元素，并将 $Y$ 压入栈中。
成功： 如果栈中包含单个匹配目标公式的元素，则证明成功。

2. 自监督定理发现算法

核心贡献是一种在证明搜索与有用定理提取之间交替进行的算法，通过构建定理库来作为未来搜索的引理（Lemmas）。

A. 目标条件策略学习

智能体学习一个策略 $\pi_\theta(A|S, g)$ ，用于在给定当前栈 $S$ 和目标 $g$ 的情况下预测下一个动作。

后视学习（Hindsight Learning）： 在搜索回合中，任何栈内仅包含单个公式 $f_t$ 的状态都被视为“已达到的定理”，无论其是否为原始目标。
训练信号： 通向 $f_t$ 的动作前缀被视为 $f_t$ 的证明。这些前缀被加入训练集 $D_{train}$ ，通过交叉熵损失来更新策略。
目标缓冲区 ( $G$ )： 缓冲区维护已发现的定理。智能体从 $G$ 中均匀采样目标用于后续的搜索回合，从而有效地实现自我引导的课程学习（Curriculum Learning）。

B. 提取有用定理

为了防止定理库变得臃肿或充满琐碎、冗余的定理，算法根据两个标准对发现的定理进行过滤：

泛化性（Generality）： 定理经过过滤以移除那些仅仅是其他候选者特例化的定理。系统仅保留在公式替换定义的偏序关系下的“最小”元素（即保留最通用的形式）。
可重证性（Reprovability）： 系统估计当前策略重新证明某个定理的概率。利用贝叶斯后验均值（Beta(1,1) 先验），它优先考虑那些已被发现但难以可靠地重新证明的定理。这些“难重证”的定理非常有价值，因为将它们作为引理可以压缩困难的证明路径。

C. 多代定理库扩展

过程按世代（Generations）运行：

策略学习： 在当前的动作空间（最初仅为公理和 MP）上训练策略。
提取： 根据泛化性和可重证性从目标缓冲区 $G$ 中识别有用定理。
动作空间扩展： 将提取的定理作为新的库动作（例如 $Thm_1, Thm_2$ ）添加进来。当选择这些动作时，会将相应的定理压入栈中，使其作为一个预验证的引理发挥作用。
迭代： 重复此过程，允许智能体利用已发现的定理来寻找新的、更复杂的定理。

核心贡献

形式化构建： 将命题定理证明形式化为直接基于希尔伯特公理和推理规则的栈机决策过程，避免了对外部证明语料库的依赖。
算法： 提出了一种自监督定理发现算法，该算法仅从原始规则开始生长出定理库。它将提取的定理作为引理重用于后续的证明搜索。
自主发现： 智能体自主发现了数万个定理，并在未使用人类先验进行训练的情况下，找到了人类编写的基准测试问题的证明。
可迁移性： 提取的定理可以作为有效的外部知识，通过作为 Prompt 引理提供给 LLM，从而提升其在基准问题上的证明性能。

实验结果

1. 定理发现与覆盖率

增长： 发现的定理数量在六个世代中持续增加，证明了智能体能够自主扩展其知识库的能力。
基准表现： 智能体成功找到了人类编写的基准测试集（源自 Kleine 教科书）中 30% 的希尔伯特系统证明。
对比： 虽然 GPT-5-high（最强的基准模型）在没有辅助的情况下在这些基准测试中仅达到约 23% 的准确率，但该智能体能找到 30% 的证明，这表明它发现的定理从人类数学视角来看是具有实际意义的非平凡证明。

2. 对 LLM 推理的影响

Prompt 引理： 当将提取的定理作为 Prompt 引理提供给 GPT-4o 和 GPT-5 变体时，它们在基准问题上的证明成功率显著提高。
定性分析：
- 一些发现的定理对应于著名的原理（例如爆炸原理 $\neg A \to (A \to B)$ ），这些原理易于理解。
- 其他定理（例如复杂的蕴含提升）对人类来说并不直观，但在 LLM 证明中能有效地作为支撑性知识。
- 这表明该智能体可以挖掘出人类未明确提供的有用引理，并且这些引理可以在不同的推理架构之间（从智能体到 LLM）进行迁移。

重要性与主张

本文声称提供了证据，证明无需依赖人类提供的定理库，仅通过证明搜索即可发现有用的定理。

自我进化的 AI： 这项工作为数学领域的自我进化 AI 系统指明了一条路径，这类系统可以通过证明搜索自主扩展其形式化知识，同时确保每一次发现都保持形式上的可验证性。
形式可验证性： 不同于可能产生看似合理实则错误的陈述的 LLM，该智能体的发现严格基于希尔伯特系统的公理和推理规则。
谦逊立场： 作者并未声称在通用推理方面超越了最先进的 LLM。相反，他们展示了在受限的形式化设定中，一个智能体可以学习如何发现并利用自身知识，从而解决即使是高级 LLM 也难以处理的问题，并且这种自发现的知识可以增强外部系统。

该研究局限于单一公理系统（希尔伯特命题逻辑），但作者认为该框架可以推广到更丰富的系统，如一阶逻辑或集合论，这也是未来的研究方向之一。