在这期 The Neuron采访Axiom Math 的创始人兼 CEO Carina Hong 播客中，主持人采访了 Axiom Math 的 24 岁创始人兼 CEO Carina Hong（洪乐潼，曾获罗德学者，曾就读于牛津、斯坦福 PhD 辍学）。她的公司刚刚筹集了 6400 万美元，旨在构建“数学超级智能（Mathematical Superintelligence）”。
视频内容非常丰富，核心内容主要涵盖了以下六个方面：
一、 跨学科背景：神经科学与数学的交汇
Carina 曾作为罗德学者在牛津大学研究神经科学，她分享了神经科学、数学和 AI 之间非常迷人的五个交汇点：
- 网格细胞（Grid Cells）的完美几何结构： [02:04] 2005 年诺贝尔奖发现大鼠海马体中的网格细胞在空间导航时，其放电模式呈现出完美的正六边形（蜂巢状）。从数学理论来看，这正是二维空间中能量最小化和球体堆积的最优密铺方式。
- 中国剩余定理（Chinese Remainder Theorem）与脑容量： [03:04] 基础数论中的中国剩余定理，被 MIT 的研究团队用来计算和解释大脑中神经元的容量叠加和排列规律。
- 持续同调（Persistent Homology）在果蝇脑图谱的应用： [03:51] 利用应用代数拓扑学中的“持续同调”工具，通过不断提高连接阈值，来分析果蝇在丢失部分突触连接时，其神经回路的结构鲁棒性（静态图的时间序列分析）。
- 从计算神经科学走向 AI： [05:20] 著名的 Gatsby 计算神经科学研究所（由 Geoffrey Hinton 创立，DeepMind 创始人 Demis Hassabis 的学术摇篮）正是伦敦的 AI 枢纽。Carina 在这里利用数学和随机矩阵理论来研究单层线性 Transformer 的神经动力学，自此转向 AI 领域。
二、 什么是“数学超级智能”？
很多人听到超级智能会想到科幻，但在数学领域，它有非常具体且分阶段的定义：
- 第一阶段：匹配人类顶尖水平（缩小顶尖数学家之间的差距）： [08:39] 普通数学家在做研究时，经常会卡在验证一个技术引理（Technical Lemma）上长达数天或数周。而像陶哲轩（Terence Tao）这样的顶级天才，凭直觉就能自信地迈向下一步。AI 如果能自动生成正确的中间证明步骤，就能弥补普通高水平定量研究员与陶哲轩之间的鸿沟，让量化交易员或科研人员效率大增。
- 第二阶段：超越人类（Superhuman）： [10:18] 顶尖的国际数学奥林匹克（IMO）命题人一年可能只能出 5 道极具启发性的好题。而 AI 超级智能可以每秒钟生成数道极具数学价值的新题目。
- 第三阶段：自我进化（Self-Improving Loop）： [11:02] AI 系统将由三个核心模块无缝交织：猜想生成器（Conjecturer）、证明器（Prover）和人类已知的数学知识库。AI 能够自己出题、自己证明、并根据上一次的对错反馈调整后续的课程难度（Curriculum），在知识库的边界不断向外拓宽。
三、 当前数学 AI 领域的两大核心瓶颈
为什么现在不是每个大模型团队都能做到这一点？因为存在非常顽固的技术死结：
- 数据极度匮乏（Data Scarcity）： [13:46] 互联网上有超过 1 万亿 token 的 Python 代码，但真正用于数学形式化证明的 Lean 语言数据只有区区一千万（A dozen million）token。模型对 Lean 的理解力极低，存在严重的冷启动问题。
- 自动形式化（Auto-Formalization）： [14:21] 将人类用英文或自然语言写的数学证明，自动转换为 Lean 等可被计算机编译的代码。这比语言翻译难得多，因为自然语言和编程代码处于完全不同的抽象层级（代码要低级、具体得多）。这陷入了“无法自动转换自然语言数学 → 无法解决 Lean 数据匮乏”的鸡生蛋、蛋生鸡的怪圈。
四、 Axiom Math 的独特技术路线与突破
针对以上瓶颈，Axiom 采取了与追求通用（General approach）的硅谷前沿实验室（Frontier Labs）完全不同的路线：
- 数学能力的“横向迁移”价值： [18:13] 顶尖的数学人才通常也会精通物理、编程、金融和系统性法律（如合同、税务）。数学是“横向通识能力”。前沿大实验室试图从易到难全面推进，导致动作缓慢；而 Axiom 集中突破数学这一点，之后能迅速横向辐射到芯片设计、芯片验证、法律和科学领域的其他分支。它被视为 AI for Science（AI 科学应用）的算法支柱。
- 数学探索的双重工具箱（Pattern Boost & Int）： [25:53] 数学不仅是寻找证明（Formal math），还关乎“构建数学对象（Constructions）”以获得直觉或寻找反例。Axiom 同时布局了这两个岛屿：
- Pattern Boost（生成式方法）： 负责生成打破常规的、新颖的数学对象和反例。最近它成功证明了一个图论（Graph Theory）中长达 30 年的猜想。 [27:57]
Int（翻译式方法）： 针对问题-答案对进行整体预测。由于数学中“某个方向比另一个方向更容易”（例如求导容易、求积分难；Lean转英文容易、英文转Lean难），Int 利用了这种逆向翻译的技巧，成功解决了一个长达 130 年关于李雅普诺夫函数（Lyapunov Function）的非多项式系统动力学难题。 [30:57]
最大胆的破局点——合成数据（Synthetic Data）： [51:27] 为了解决 Lean 语言的数据冷启动，Axiom 并没有像普通人一样雇佣全世界的 Lean 开发者来人肉写代码。相反，他们采取了大胆的合成数据生成策略（Synthetic Data Generation Approach），用系统将现有的非形式化数学自动转换并成倍衍生出高质量的 formal 证明数据，类似于 AlphaGo 早期只用了极少的人类大师棋谱作为起点。
五、 如何防止 AI 生成数百万个“无用的垃圾定理”？
当主持人问到 AI 自我迭代时会不会产生大量无用废话时，Carina 提出了几种过滤器：
- 利用大模型作为品味评判员（LLM as Judges）： 对定理的“有趣程度”进行打分排序。
- 程序化分析依赖图（Dependency Graph）： 如果一个新定理的证明成功连接了两个此前完全没有交集的数学分支（例如代数与组合数学），[35:26] 系统就会自动判定该成果具有极高的“创新性（Novelty）”，因为它促进了跨学科的思想融合（Diffusion of ideas）。
六、 商业化落地、5年愿景与社区建设
- “检查检查者”（Who checks the checker）： [42:04] 形式化证明最完美的地方在于，一旦写成 Lean 代码且系统编译通过（Compiles），根据柯里-霍华德同构，它就是 100% 绝对正确的，人类甚至不需要去阅读它那冗长的底层代码。未来产品端会把复杂的 Lean 代码“隐藏”起来，用户只需看到绿色的“正确勾选标记”即可确信其无幻觉、绝对安全。
- 近期与远期商业应用： [44:04] 这种严密的逻辑验证能力可以完美延伸至芯片设计与验证、加密协议验证、智能合约审计，以及重度合规的金融审计。AWS 已经证明了基于神经符号推理的业务有多么受企业客户欢迎。
- 5年后的工作场景： [48:09] 5 年后，定量研究员、金融分析师或软件工程师的日常会是在一个 reasoning 平台（类似于一个专门的 IDE 界面）上工作。输入你想解决的问题和初步直觉，AI 会立刻自动为你推荐逻辑严密、无幻觉的中间步骤。
- 繁荣的 Lean 开源子文化： [23:22] Carina 提到，现在研究 Lean 的社区氛围非常像早期的 GPU 或 CUDA 社区，聚集了一群不为名利、纯粹由于“在写数学代码中获得快乐”而聚集的怪才（包括一边做 IP 律师一边贡献 GitHub 的人，以及直播打游戏和奥数解题的博主）。Axiom Math 深度融入其中，正在积极赞助并共同组织包括 NeurIPS 的 AI for Math 工作坊、一月份的联合数学会议（JMM）以及 ARUS 工作坊等行业内最重要的学术社区集会。
Top comments (0)