自对弈定理证明算法的理论框架

自我对弈是一种使模型能够自我改进的训练算法，最近在使用 大语言模型 (LLM) 进行形式定理证明的背景下显示出了有希望的实证结果。 （Dong & Ma，2025）用两个合作代理实例化自我对弈：一个证明者，用于证明定理；以及一个猜想者，用于生成新定理作为证明者的课程。在本文中，我们提供了一个理论框架来理解用于定理证明的自我对弈算法的自我改进能力。首先，我们将定理集形式化为图，其中节点为定理，边为具有相似语义的定理对之间的边。我们引入了一组原始假设，这些假设描述了经过训练的证明者的保证以及猜想者如何访问图的结构。其次，我们表明，如果定理的基础图是良好连接的，那么证明者-猜想器系统（其中猜想算法基于可逆随机游走）足以以指数方式增长已证明的定理集。第三，受自博算法经验上遇到的问题的启发，其中猜想者倾向于生成人为复杂且非基本的定理，我们提出了一种用于猜想者生成的定理训练分布的多样性度量，以及一种改进的猜想算法，通过计算定理图中相邻定理之间的扩散相似性，局部最大化这种多样性度量。最后，我们描述了一种通过使用对比学习将节点嵌入到欧几里得空间中，然后计算嵌入之间的内积来计算扩散相似度的方法。