A Theoretical Framework for Self-Play Theorem Proving Algorithms
作者: Thomas Chen, Zhiyuan Li
分类: cs.LG
发布日期: 2026-06-01
💡 一句话要点
提出自博弈定理证明算法的理论框架，解决复杂定理生成问题。
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自博弈学习 定理证明 大型语言模型 对比学习 扩散相似性 随机游走 多样性度量
📋 核心要点
- 现有自博弈定理证明算法在生成定理时，容易产生人为复杂和非根本的定理，影响训练效率。
- 论文提出基于可逆随机游走的猜想算法，并引入多样性度量，鼓励生成更多样化的定理。
- 通过对比学习计算定理之间的扩散相似性，用于指导猜想器生成更具探索性的定理。
📝 摘要（中文）
本文为理解自博弈算法在定理证明中的自提升能力提供了一个理论框架。首先，将定理集合形式化为一个图，节点表示定理，边连接语义相似的定理。引入了一组基本假设，描述了训练后的证明器的保证以及猜想器如何访问图的结构。其次，证明了如果定理的底层图是良好连接的，那么基于可逆随机游走的猜想器足以使已证明的定理集合呈指数增长。第三，针对自博弈算法在实践中遇到的猜想器倾向于生成人为复杂和非根本定理的问题，提出了一种针对猜想器生成的定理训练分布的多样性度量，并提出了一种改进的猜想算法，通过计算定理图中相邻定理之间的扩散相似性来局部最大化这种多样性度量。最后，描述了一种通过使用对比学习将节点嵌入到欧几里德空间中，然后计算嵌入之间的内积来计算扩散相似性的方法。
🔬 方法详解
问题定义：现有自博弈定理证明算法，特别是使用大型语言模型（LLMs）时，存在一个问题：猜想器倾向于生成过于复杂或非根本的定理，导致证明器难以学习，降低了自提升的效率。这些“人为复杂”的定理可能缺乏内在价值，并且偏离了更有意义的定理证明路径。
核心思路：论文的核心思路是将定理证明过程建模为一个图上的探索问题。定理是图中的节点，定理之间的语义相似性构成边。通过设计一个能够有效探索这个图的猜想器，可以引导证明器学习更有价值的定理。关键在于，猜想器不仅要生成新的定理，还要保证生成定理的多样性，避免陷入局部最优。
技术框架：该框架包含两个主要组成部分：证明器和猜想器。证明器负责证明给定的定理，猜想器负责生成新的定理作为证明器的训练数据。整体流程如下：1. 猜想器根据当前已证明的定理生成新的猜想定理。2. 证明器尝试证明这些猜想定理。3. 根据证明结果更新已证明定理的集合。4. 使用对比学习计算定理之间的扩散相似性，并用于指导猜想器的定理生成过程。
关键创新：论文的关键创新在于提出了一个针对定理训练分布的多样性度量，并设计了一种改进的猜想算法，该算法通过计算定理图中相邻定理之间的扩散相似性来局部最大化这种多样性度量。这种方法鼓励猜想器生成更多样化的定理，从而提高证明器的学习效率和泛化能力。
关键设计：论文使用对比学习来计算定理之间的扩散相似性。具体来说，首先使用对比学习将定理嵌入到欧几里德空间中，然后计算嵌入之间的内积作为扩散相似性的度量。猜想器在生成新定理时，会考虑与已证明定理的扩散相似性，倾向于选择与当前定理集合差异较大的定理。此外，论文还提出了基于可逆随机游走的猜想算法，保证了定理图的有效探索。
📊 实验亮点
论文提出了多样性度量和基于扩散相似性的猜想算法，理论上证明了在良好连接的定理图上，该算法能够使已证明的定理集合呈指数增长。虽然论文没有提供具体的实验数据，但其理论分析为自博弈定理证明算法的改进提供了有力的指导。
🎯 应用场景
该研究成果可应用于自动定理证明、数学知识发现、程序验证等领域。通过提升自博弈算法的效率，可以帮助研究人员更有效地探索数学定理，并开发更强大的自动推理系统。此外，该方法还可以推广到其他需要探索复杂搜索空间的任务中，例如药物发现、材料设计等。
📄 摘要（原文）
Self-play, a type of training algorithm that enables a model to self-improve, has recently shown promising empirical results in the context of formal theorem proving using Large Language Models (LLMs). (Dong & Ma, 2025) instantiate self-play with two cooperating agents: a prover, which proves theorems, and a conjecturer, which generates new theorems as a curriculum to the prover. In this paper, we provide a theoretical framework for understanding the self-improvement capabilities of self-play algorithms for theorem proving. First, we formalize the set of theorems as a graph, with nodes as theorems and edges between pairs of theorems with similar semantics. We introduce a set of primitive assumptions that characterize the guarantees of a trained prover and how a conjecturer can access the structure of the graph. Second, we show that if the underlying graph of theorems is well-connected, then a prover-conjecturer system, where the conjecturing algorithm is based on a reversible random walk, is sufficient to grow the set of proved theorems exponentially. Third, motivated by an issue encountered empirically by self-play algorithms, where the conjecturer tends to generate artificially complex and non-fundamental theorems, we propose a diversity measure for a training distribution of theorems generated by a conjecturer and an improved conjecturing algorithm that locally maximizes this diversity measure, by computing the diffusion similarity between neighboring theorems in the theorem graph. Finally, we describe a method to compute the diffusion similarity by using contrastive learning to embed nodes into Euclidean space and then computing the inner-product between embeddings.