Self-Supervised Theorem Discovery in a Formal Axiomatic System

背景

近年来，人工智能系统在数学推理领域取得了显著进展。然而，无论是大型语言模型（LLM）还是其他现有的数学AI方法，其成功在很大程度上都依赖于人类积累的先验知识——包括海量的数学文本、代码库以及结构化的定理库。这些人类先验知识为AI提供了丰富的起点和参考，但也带来了一个根本性的开放问题：如果一个智能体完全脱离这些人类提供的知识，仅凭最基础的数学规则，它是否依然能够自主地发现那些“有用”的定理？换句话说，有价值的数学定理能否从纯粹的逻辑推演中自然涌现，而非依赖人类的事先灌输？

核心内容

针对上述问题，本文提出了一种在形式化公理系统中进行自监督定理发现的方法。研究的核心在于开发一种智能体，它不依赖任何人类提供的定理库，而是仅从最基本的公理和推理规则出发，逐步构建并扩充一个“有用定理”库。

具体而言，该研究提出了一种自监督定理发现算法，该算法的核心机制在于两个交替进行的步骤：证明搜索与有用定理提取。在证明搜索阶段，智能体尝试在现有知识体系内推导出新的证明；随后，在有用定理提取阶段，系统会从这些新发现的证明中筛选出具有潜力的定理，将其作为引理（Lemma）加入到定理库中。这些被提取出的定理并非简单的推演堆砌，而是被判定为对后续证明搜索“有用”的知识模块。

这种机制形成了一个正向反馈循环：不断扩充的定理库为后续的证明搜索提供了更强大的引理支持，从而使得智能体能够攻克更复杂的证明；而更复杂的证明又会反过来产生更多、更深层的有用定理。实验结果令人瞩目，该智能体在没有任何人类定理库辅助的情况下，自主发现了数万个定理。更关键的是，这些被发现的定理不仅在形式上有效，它们还在两个方面证明了其“人类数学视角”下的价值：首先，智能体利用这些自主发现的定理，成功找到了人类编写的基准问题的证明；其次，当把这些提取出的定理作为提示词中的引理提供给 LLM 时，LLM 的证明性能得到了显著提升。这有力地证明，通过纯粹的证明搜索，确实可以涌现出对人类数学家和AI推理都有意义的定理。

关键要点

• 摆脱人类先验：研究首次在形式化公理系统中实现了完全不依赖人类提供的数学文本、代码或定理库的定理发现，仅从公理和推理规则出发。
• 自监督交替机制：算法核心采用“证明搜索”与“有用定理提取”交替进行的方式，实现知识的自我积累与演进。
• 定理库的动态构建与复用：新发现的定理作为引理被动态添加到定理库中，供后续证明搜索调用，形成知识增长的正反馈循环。
• 双重价值验证：自主发现的定理不仅被证明能够解决人类基准问题，还能作为外部知识增强 LLM 的证明能力，验证了其在真实AI推理场景中的实用性。
• 形式化可验证性：所有的发现和推演都在严格的形式化公理系统中进行，确保了结论的绝对严谨性和可验证性。

意义与影响

这项研究为数学人工智能领域带来了深远的启示。它首次通过严谨的实验证据表明，有价值的数学定理并非必须依赖人类的直觉或先验知识才能被发现，纯粹的自动化证明搜索本身就具备涌现有用知识的能力。

这一突破为构建自我演进（Self-evolving）的AI数学系统开辟了一条全新的道路。未来，数学AI不再仅仅局限于学习人类已有的知识，而是能够成为一个自主探索和发现新知识的“数学家”。此外，该研究也为LLM的推理能力增强提供了一种全新的范式——不再仅仅依赖扩大模型规模或增加训练数据，而是通过为LLM提供由形式化系统生成的、经过严格验证的外部定理库，来显著提升