小Transformer能学会Coxeter群语言吗？

当数学家与AI研究员合作：用注意力模式证明猜想

机制可解释性（mechanistic interpretability）正成为数学与AI交叉研究的沃土。一篇来自rss的研究展示了这样的合作：训练一个小型Transformer学习Coxeter群仿射A2的语言，并通过观察其注意力模式，提出并证明了一个关于该群的词论猜想。

Coxeter群仿射A2是等边三角形密铺欧几里得平面的对称群，其语言由生成元及其关系构成。研究者选择这一相对简单的群，旨在探索小模型能否捕捉到群论结构。

Coxeter群是一类由反射生成的抽象群，在几何、李代数与组合数学中广泛出现。每个Coxeter群由生成元集合与关系（如生成元的阶数）通过呈现（presentation）定义，其词问题即判断两个生成元序列是否表示同一群元素。仿射A2是最简单的仿射Coxeter群之一，对应等边三角形密铺平面的对称性，其Coxeter图为一个三角形，每个生成元的平方为单位元，相邻生成元的乘积阶为3，且满足辫关系。它的词语言具有丰富的组合结构，是检验模型能否学习代数规则的理想测试平台。

方法：训练与观察

研究团队训练了一个小型Transformer，输入是Coxeter群的词（生成元的序列），任务是预测下一个生成元或判断词是否等价于单位元。这种设置迫使模型内化群的乘法规则。

训练完成后，研究者分析了模型的注意力模式，发现它学会了关注特定的生成元组合，这些模式与群的代数结构存在对应关系。

机制可解释性旨在逆向工程神经网络内部的计算机制，而非仅关注输入输出行为。常见技术包括注意力模式分析（观察注意力头关注哪些位置）、探针分类器（从隐藏状态预测特定属性）与因果干预（如激活修补）。在本研究中，研究者通过可视化注意力权重，识别模型是否学会了关注生成元之间的特定组合关系，从而将高维的模型行为映射到群论概念上。这种方法的关键在于假设模型内部存在可被人类理解的结构化表征，并通过实验验证这些表征与数学对象之间的对应。

从观察到证明：词论猜想的提出

基于注意力模式，研究者提出了一个关于仿射A2词论的猜想：某些词的模式在特定条件下必然出现。随后他们给出了数学证明，验证了猜想的正确性。这体现了机制可解释性如何反哺纯数学研究——模型提供了人类可能忽略的线索。

词论猜想通常指关于群的字（生成元序列）的组合性质或等价条件的命题。在仿射A2中，词问题可通过几何表示（如将生成元视为对三角形网格的反射）来研究，但某些模式可能难以从纯代数角度直接发现。注意力模式提供的线索可能指向特定的词形（如交替序列或重复块）在模型预测中具有特殊地位，从而启发数学家形式化一个可证明的猜想。这种“AI提示、人类证明”的流程区别于自动定理证明，强调可解释性作为发现工具而非证明引擎。

意义与展望

这项工作展示了小Transformer作为数学发现工具的潜力。虽然目前仅针对一个特定群，但方法可推广至其他Coxeter群甚至更广泛的代数结构。它也为AI辅助数学研究提供了新范式：不是让AI证明定理，而是让AI揭示结构，再由人类完成证明。

未来，随着模型规模和可解释性技术的进步，这种合作模式或将成为数学研究的标准工具之一。