数学家工作方式存在的问题

数学研究是人类活动中最具智力挑战的工作之一，在许多方面也是自动化程度最低的领域。虽然AI系统已经改变了编程、写作和数据分析，但高等数学的形式化结构在很大程度上仍然超出AI的能力范围。证明必须通过严格的逻辑进行验证；抽象结构中的模式对使大型语言模型在文本处理中有效的统计模式匹配无效。一家名为Axiom Math的初创公司认为它已经找到了改变这一状况的方法，本周它为数学家发布了一个免费工具，它能在单台笔记本电脑上实现重要的模式发现能力。

这个工具叫做Axplorer，是PatternBoost的民主化版本——一个由Francois Charton开发的算法，他现在在Axiom工作，之前曾在Meta工作。在2024年，Charton使用PatternBoost在数千个超级计算机节点上运行三周，破解了图论中一个百年未解的问题——Turan四环问题。Axplorer可以在Mac Pro上用两个半小时达到同样的结果。

Axplorer如何工作

Axplorer底层的算法通过古典搜索和神经网络学习的迭代循环工作。它首先生成大量随机候选解，并保留表现最好的。然后在这些成功的例子上训练一个transformer神经网络，以学习表征好解决方案的特征。在下一轮中，训练好的网络生成改进的候选，这些候选作为另一个古典搜索阶段的种子。两个阶段交替进行，每一轮都产生逐步改进的解决方案。

关键的见解是神经网络不需要以任何深层的方式理解数学。它只需要识别迄今为止已经发现的解决方案中的结构模式，并使用这些模式来指导更好候选的生成。经过许多迭代，这会产生古典搜索单独不太可能找到的解决方案——特别是在搜索空间巨大的问题中，随机探索在计算上是不可行的。

Turan问题及其揭示的内容

Turan四环问题问道：给定一组点，你可以在它们之间绘制多少条边而不创建任何四点循环？该问题涉及组合学和图论中与实际网络分析相关的深层结构——社交媒体图、供应链和搜索引擎链接结构。在PatternBoost于2024年破解它之前，它已经抵御解决约一个世纪。

PatternBoost需要大规模超级计算机这个事实对于日常运行这种规模基础设施的Meta来说不是障碍。但对于世界上几乎每个想要将类似方法应用于自己开放问题的数学家来说，这都是一个障碍。通过设计Axplorer在消费级工作站上运行，Axiom改变了访问这类数学AI的分布。