[arXiv 2024] 重新发现同调：通过多智能体协作开启数学自主发现的新范式

TL;DR

来自剑桥大学的研究团队提出了一种新型多智能体 AI 系统，模拟了人类数学家“猜想-反证-定义重构”的思维循环。该系统在仅具备线性代数背景知识的情况下，通过观察多面体数据，自主“重新发现”了拓扑学中极具深度的 同调（Homology） 概念和 欧拉示性数（Euler Characteristic） 的本质公式。

背景定位：数学不只是证明，更是“构造问题”的艺术

长期以来，AI 在数学领域的探索被划分为两个阵营：一类是以 AlphaProof 为代表的“证明派”，专注于在给定命题下寻找路径；另一类是“猜想派”，通过统计相关性寻找潜在规律。

然而，正如数学大师格罗滕迪克（Grothendieck）所言：“决定性的事情往往是看到那些尚未被看见的问题。”本文认为，数学是一个动态的、辩证的过程。单纯的证明器无法产生新概念，而单纯的统计模型无法保证逻辑严密。该系统将两者结合，标志着 AI 从“答题工具”向“研究助手”的跨越。

核心机制：推测与怀疑的博弈

该系统的核心由两个智能体和一个名为 MathWorld 的环境组成：

1. 推测智能体 (Conjecturing Agent, CA)：
   • 动机：生成既能解释数据又“可证明”的猜想。
   • 手段：采用符号回归（Symbolic Regression）从变量（如矩阵的秩 Rank、维数 Dim）中构建逻辑表达式。
2. 怀疑智能体 (Skeptical Agent, SA)：
   • 动机：防止 CA 投机取巧，提出只适用于简单子集的平庸命题。
   • 手段：通过调整数据权重 ${\lambda }_i$，向 CA 抛出“反例”（如从球体切换到带孔的环面数据）。

图 1：推测智能体通过符号回归生成命题，并将其翻译为 Lean 代码。

实验挑战：重新发现欧拉猜想

研究者设定了一个经典挑战：让 AI 重新走过 19 世纪拓扑学的道路。

• 输入数据：单纯复形（Simplicial Complexes）的入射矩阵（如点、线、面的关联）。
• 任务：定义出欧拉示性数 $\chi$。
• 难点：AI 不知道什么是“洞”（Genus），它必须发现 Betti 数（$b_i$），并理解为什么 $V-E+F$ 在拓扑变换中保持不变。

图 2：MathWorld 系统全流程。由于引入了证明反馈（Provability），系统能自动剔除那些统计上成立但在逻辑上无意义的伪命题。

深度洞察：为什么“证明”反能促进“发现”？

实验结果显示了一个有趣的物理直觉：

• 单一回归的挫败：如果只给 AI 运行符号回归（Only CA），它几乎永远无法发现 Betti 数。因为搜索空间太大，AI 会淹没在无意义的算式中。
• 证明的引导作用：当引入 Lean 的证明反馈后，系统表现出明显的倾向性——它开始发现那些包含秩和零化度（Rank-Nullity）的组合，因为这些组合更容易被线性代数定理证明。

这意味着，数学上的“有趣性”可以通过“可证明性”来逼近。当 CA 试图平衡数据的广泛适用性与逻辑的严密性时，它被迫“发明”了 Betti 数这样的抽象概念，作为数据压缩和逻辑闭环的桥梁。

总结与未来

这项研究证明，AI 不需要被显式教导“什么是洞”，只要给它足够的数据压力和严密的逻辑约束，它就能在博弈中涌现出深度的数学直觉。

局限性：目前系统仍依赖于预设的算子集（+, -, logicals）和特定的线性代数背景。 展望：随着大模型（LLM）驱动的自动形式化（Auto-formalization）技术成熟，未来此类系统或许能在更广阔的数学未知领域（如 Langlands Program 或新型图论猜想）中，扮演发现者的角色。

主编点评：本文最迷人之处在于，它用算法复刻了拉卡托斯（Lakatos）在《证明与反驳》中描述的数学史进程。它告诉我们，AI 走向智能的标志，不是它能做对多少道复杂的积分题，而是它能否在被反例打败后，冷静地修改自己的定义。