形式化公理系统中的自监督定理发现

# 自监督定理发现：在形式化公理系统中

来源：https://arxiv.org/html/2606.28747

###### 摘要

近期的人工智能系统在数学推理方面取得了显著进展。许多现有方法，包括大语言模型，都借助人类先验知识，例如数学文本、代码或定理库。尽管这些方法在实践中非常高效，但一个开放问题是：智能体能否在没有这些人类先验知识的情况下自主发现有用的定理。我们在一个形式化公理系统中研究此问题，开发了一个智能体，它仅从公理和推理规则出发，逐步构建一个有用的定理库。具体而言，我们提出了一种自监督定理发现算法，该算法交替进行证明搜索和有用定理提取，构建一个定理库，其条目作为引理被重复用于后续的证明搜索。实验表明，该智能体发现了数万个定理，并为人工编写的基准问题找到了证明，这表明其发现包含从人类数学角度来看有意义的定理。此外，当这些发现的定理作为提示引文提供时，能够提升大语言模型的证明性能，表明它们可以作为大语言模型推理的外部知识。我们的结果证明，有用的定理可以从证明搜索中涌现，而无需依赖人类提供的定理库。更广泛地说，它们为数学领域自我进化的AI系统指明了一条道路，这类系统的发现仍然是可正式验证的。

机器学习，自动定理证明，数学推理

\icml@noticeprintedtrue††footnotetext:\\Notice@String

## 1 引言

人工智能系统正在迅速提高其数学推理能力。像GPT和Gemini这样的大语言模型在数学基准测试中表现持续提升 (OpenAI, 2024b (https://arxiv.org/html/2606.28747#bib.bib32), 2025 (https://arxiv.org/html/2606.28747#bib.bib35); Gemini Team, 2025 (https://arxiv.org/html/2606.28747#bib.bib36))。最近的一个Gemini模型被报道在国际数学奥林匹克2025中达到了金牌标准水平 (Luong and Lockhart, 2025 (https://arxiv.org/html/2606.28747#bib.bib40))，凸显了基于LLM的数学推理的进步。尽管LLM能够用自然语言进行数学推理，但其输出可能难以验证，因为它们可能包含因幻觉而产生的看似合理但错误的表述 (Farquhar et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib41); Kalai et al., 2025 (https://arxiv.org/html/2606.28747#bib.bib42))。这推动了将形式语言和证明助手用于定理证明的工作，作为通往严谨数学推理的一条路径。近期的工作包括自动形式化和证明草图方法，这些方法将自然语言数学与形式证明连接起来 (Wu et al., 2022 (https://arxiv.org/html/2606.28747#bib.bib22); Jiang et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib29))，以及在证明助手（如Lean）中生成证明的方法 (Han et al., 2022 (https://arxiv.org/html/2606.28747#bib.bib20); Polu et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib21); Yang et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib23); Xin et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib44); Zimmer et al., 2025 (https://arxiv.org/html/2606.28747#bib.bib45); Hubert et al., 2026 (https://arxiv.org/html/2606.28747#bib.bib46))，以及将语言模型生成与符号推理或学习到的库相结合的方法 (Trinh et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib47); Wang et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib43); Dong and Ma, 2025 (https://arxiv.org/html/2606.28747#bib.bib50))。这一系列工作凸显了将可正式验证的推理基底与机器学习模型的搜索能力相结合的价值。同时，许多当前方法从人类构建的数学知识出发。例如，数学语言模型可能通过预训练于数学文本和代码来使用自然语言数学知识 (Azerbayev et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib31))，而将自然语言连接到形式证明的方法通常从人类编写的问题陈述或非形式证明开始 (Wu et al., 2022 (https://arxiv.org/html/2606.28747#bib.bib22); Jiang et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib29))。此外，证明生成和检索增强定理证明的方法通常使用现有的形式库及其包含的定理和证明 (Han et al., 2022 (https://arxiv.org/html/2606.28747#bib.bib20); Polu et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib21); Yang et al., 2023 (https://arxiv.org/html/2606.28747#bib.bib23))。即使基于大规模合成数据的方法，也通常从自然语言数学问题构建训练数据 (Xin et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib44))。这类知识在实践中非常有用，但使得难以孤立地考察智能体仅从形式规则中能发现多少数学结构。一个相关的研究方向通过从公理和形式规则中学习，减少对人类提供的证明或现有数据的依赖 (Wu et al., 2021 (https://arxiv.org/html/2606.28747#bib.bib25); Laurent and Platzer, 2022 (https://arxiv.org/html/2606.28747#bib.bib30); Poesia et al., 2024 (https://arxiv.org/html/2606.28747#bib.bib49))。这些研究表明，智能体可以在公理化领域中进行自我改进，并发现定理或证明。Kasriel et al. (2025 (https://arxiv.org/html/2606.28747#bib.bib51)) 尤为接近，因为它从公理中发现定理，将其重复用于进一步搜索，并通过询问LLM裁判它们是否看起来有用来评估外部有用性。然而，这些定理能否在作为引理提供时提升外部推理智能体的证明性能，仍然是一个开放问题。我们解决了这个问题，并展示了我们的方法发现的定理既提升了智能体自身的证明搜索，也提升了LLM的证明搜索。

在本研究中，我们探讨智能体是否能在不依赖人类先验知识的情况下自主发现有用的定理。为了隔离这个问题，我们要求智能体仅从形式化公理系统的原始规则出发，不使用现有的定理库、证明语料库、自然语言先验知识或外部提供的训练问题集。人类编写的问题仅用于评估，而不用于训练智能体或构建定理库。我们在命题逻辑的希尔伯特公理系统中实例化这个形式化系统设置。这个设置是刻意简化的：它只有少数原始规则，但证明搜索仍然不平凡，并且每个发现的定理仍然是可形式化检查的。具体来说，我们将希尔伯特系统证明搜索表述为一个栈机器决策过程，其中状态是当前的证明栈，动作是将希尔伯特公理压入栈或应用肯定前件。因为在搜索过程中获得的公式可以被视为定理，所以证明搜索本身产生了定理候选。在这个栈机器表述的基础上，我们提出了一种自监督定理发现算法，该算法从智能体自身的证明搜索中增长一个定理库。智能体将在搜索过程中达到的定理重新用作未来的证明目标，并从达到这些定理的动作序列中学习一个目标条件策略。监督信号来自智能体自身的成功证明前缀：每当搜索达到一个定理时，相应的动作序列就成为再次证明该定理的训练信号。然后，它从发现的集合中提取有用的定理，并将它们添加为定理动作，这些动作可以在后续的证明搜索代中用作引理。通过这种方式，智能体不仅学会了发现定理，还学会了使用它们来证明新的定理。

实验表明，所提出的方法发现的定理无论对于智能体自身的证明搜索还是对于外部LLM的证明搜索都是有用的。具体来说，该智能体发现了数万个定理，并为人工编写的基准问题找到了证明。此外，当提取的定理被作为提示引文提供时，它们提升了LLM的证明性能。这些结果表明，有用的定理可以从仅基于公理和推理规则的证明搜索中涌现，并且它们不仅可以作为智能体的内部引文，还可以作为辅助外部推理系统的知识。我们的贡献可以总结如下：

1. 我们基于希尔伯特公理系统的公理和推理规则，将命题定理证明直接表述为一个栈机器决策过程。
2. 我们提出了一种自监督定理发现算法，该算法从希尔伯特公理系统的原始规则出发增长一个定理库，然后将提取的定理作为引文用于进一步的证明搜索。
3. 我们的实验表明，我们的智能体发现了数万个定理，并为人工编写的基准问题找到了证明。
4. 最后，我们展示了提取的定理在作为提示引文提供时，也提升了LLM的证明性能，作为LLM推理的外部知识。

## 2 预备知识

请参见图注

图 1: 希尔伯特系统及 `A→A` 的证明树。上方：三条公理和肯定前件。这些公理分别表示弱化、蕴含分配和换位。下方：一个证明树，从两个 `Ax1` 实例、一个 `Ax2` 实例和两个肯定前件步骤推导出 `A→A`。

本节定义了本文所使用的逻辑设置。它为第 3 节 (https://arxiv.org/html/2606.28747#S3) 中引入的栈机器决策过程提供了基础。

#### 命题公式的记号

为了保持语法简洁，本文仅使用蕴含 `→` 和假 `⊥` 构建公式。标准表述通常使用原始连接词，如否定 `¬`、合取 `∧`、析取 `∨`、蕴含 `→` 和双条件 `↔`。对于经典命题逻辑的表达能力，这些连接词不必都是原始的，因为蕴含和假构成了通常连接词的一个基 (Post, 1921 (https://arxiv.org/html/2606.28747#bib.bib9))。具体地，定义 `¬A := A→⊥`，`A∨B := (A→⊥)→B`，`A∧B := (A→(B→⊥))→⊥`。定义 `A↔B` 为 `(A→B)∧(B→A)`，并使用合取展开。因此，除非另有说明，每个公式仅使用 `→` 和 `⊥`，其他连接词是通过上述翻译展开的语法糖。

#### 希尔伯特系统的规则

希尔伯特系统是一种公理化证明系统，其中定理通过推理规则从公理推导出来 (Hilbert and Ackermann, 1950 (https://arxiv.org/html/2606.28747#bib.bib11); Mendelson, 2015 (https://arxiv.org/html/2606.28747#bib.bib10))。本文使用的系统如图 1 (https://arxiv.org/html/2606.28747#S2.F1) 所示，由三条公理 `Ax1`、`Ax2`、`Ax3` 和一条推理规则“肯定前件”组成。公理中的符号 `A`、`B`、`C` 代表任意公式。一个证明重复引入公理并应用肯定前件，从先前获得的公式 `X` 和 `X→Y` 推导出 `Y`。当最终公式与目标匹配时，它已被推导为一个定理。图 1 (https://arxiv.org/html/2606.28747#S2.F1) 的下方显示了一个定理 `A→A` 的证明树。它使用了两个 `Ax1` 实例、一个 `Ax2` 实例和两次肯定前件应用。通过这种方式，希尔伯特系统通过组合公理和推理规则来证明定理。

#### 可靠性与完备性

已知这个希尔伯特系统对于经典命题逻辑是可靠且完备的 (Church, 1996 (https://arxiv.org/html/2606.28747#bib.bib12))。可靠性意味着在该系统中推导出的每个公式在经典命题逻辑的标准语义下都是有效的。完备性给出了相反的保证，即经典命题逻辑中每个有效的公式都可以在这个希尔伯特系统中推导出来。这些性质证明了将希尔伯特系统视为经典命题逻辑的标准公理化系统之一的合理性。

#### 寻找证明的难度

虽然可靠性和完备性保证了正确性和证明的存在性，但它们并不意味着证明易于发现。事实上，判定命题有效性是一个 coNP-完全问题 (Cook, 1971 (https://arxiv.org/html/2606.28747#bib.bib13))。此外，从证明复杂性的角度来看，有效公式在给定的证明系统中不一定有短的证明，并且证明长度在不同证明系统之间可能有很大差异 (Cook and Reckhow, 1979 (https://arxiv.org/html/2606.28747#bib.bib14))。因此，在希尔伯特系统中高效地寻找证明是一个不平凡的问题。

## 3 定理证明的栈机器形式化

请参见图注

图 2: `A→A` 证明树的栈机器执行。图 1 (https://arxiv.org/html/2606.28747#S2.F1) 中的证明树被转换为线性动作序列：叶节点的公理实例作为压栈动作 `Ax1`、`Ax2` 和 `Ax3` 执行，内部的肯定前件节点作为 `MP` 动作执行。每个 `MP` 动作从栈中弹出一个蕴含式及其前件，并将相应的后件压入栈。这个示例表明，五个动作的序列 `Ax1`、`Ax1`、`Ax2`、`MP`、`MP` 是 `A→A` 的一个证明。

我们将希尔伯特系统中的证明构建形式化为一个由栈机器执行的动作序列。希尔伯特证明通常表示为由公理和肯定前件构建的证明树。然而，对于学习算法来说，将证明构建表示为顺序决策过程更为自然。因此，我们将证明树展平为栈操作序列。形式上，对于目标公式 `g`，我们将栈机器决策过程定义为一个确定性的、目标条件的决策过程，由元组 `(S, A, s0, P)` 给出，其中 `S` 是公式的有限栈的集合，`A = {Ax1, Ax2, Ax3, MP}` 是动作空间，初始状态 `s0` 是空栈。转移规则 `P` 是确定性的。每个公理动作将相应的希尔伯特公理模式压入栈。对于 `MP` 动作，我们在公式元变量上使用 Hindley-Milner 合一 (Hindley, 1969 (https://arxiv.org/html/2606.28747#bib.bib15); Milner, 1978 (https://arxiv.org/html/2606.28747#bib.bib16); Damas and Milner, 1982 (https://arxiv.org/html/2606.28747#bib.bib17))。如果栈顶公式可以与一个蕴含式 `X→Y` 合一，并且它下面的公式可以与 `X` 合一，那么 `MP` 动作是合法的，并且当应用时，它会弹出两个公式并压入得到的后件 `Y`。当栈仅包含单个公式 `g` 时，该过程对于目标 `g` 成功。我们在这个形式化中没有指定标量奖励函数，因为我们的方法中的学习信号是从自我发现的定理构建的，而不是由外部定义的奖励。图 2 (https://arxiv.org/html/2606.28747#S3.F2) 通过展示 `A→A` 的证明树作为栈机器执行来说明这个观点。在这个例子中，两个 `Ax1` 动作、一个 `Ax2` 动作和两个肯定前件动作在栈上产生了定理 `A→A`。遵循这个栈机器决策过程，希尔伯特风格的定理证明可以被视为一个顺序决策问题，其中智能体选择引入哪个公理以及何时应用肯定前件。

#