超越非正式 AI：Axiom Math 与验证式超智能之路

论点：验证是卓越的催化剂

形式化验证并非用于修复“糟糕”或消除幻觉的工具；它是扩展和复合超智能的主要机制。非正式 AI 依赖于人类偏好和随机判断，而验证式 AI 使用形式化语言提供基准真相（ground truth），从而允许 AI 扩展其卓越能力，就像严谨的证明写作将 Ramanujan 从一个直觉天才转变为更强大的数学家一样。

Axiom Math 的方法与 Putnam 成功案例

Axiom Math 利用一种名为 Action Prover 的系统，这是一个由使用强化学习 (RL) 和监督微调 (SFT) 在 Lean 数据上进行后训练的模型组成的集成系统。这种方法专注于验证式生成，而不仅仅是对现有输出的验证。

Putnam 基准测试

在 2025 年 12 月，Axiom 的系统在 Putnam 考试中获得了 120/120 的满分，超越了人类表现最佳者（得分为 110）以及其他领先的 LLM，如 DeepSeek（得分为 103）。这一结果表明，一个具有显著更少数据的形式化数学系统可以超越非正式 LLM 在超人类任务上的表现。

Lean 作为基础

Lean 是一种函数式编程语言和定理证明器，它通过 Curry-Howard 对应关系将证明转化为程序。Axiom 利用 Lean，因为它允许 AI 通过“策略”（tactics）处理低层逻辑演绎，从而使系统能够专注于导航高层直觉空间。

数学发现 vs. 证明

Axiom 区分了数学发现与形式化证明。证明是最终的验证，但发现是预先提出猜想的步骤，数学家在此步骤中寻找构造、序列或图表以形成直觉。

• 发现工具： Axiom 正在开源用于数学发现的代码库，以帮助理论家在尝试形式化证明之前寻找反例或构造（例如，解决存在 30 年之久的猜想）。
• 工作流程： 理想的流水线涉及一个非正式推理器提出规范或猜想，然后由一个形式化证明器（如 Action Prover）执行证明。

验证式 AI 的商业案例

凭借 2 亿美元的 A 轮融资和 16 亿美元的估值，Axiom 的市场策略已超越了小众学术数学领域，扩展到任何需要对 AI 生成的代码拥有“优先拒绝权”的领域。

硬核验证市场

某些行业对“基本验证”的结果零容忍：

• 硬件验证： GPU 没有部分分数；它要么工作，要么不工作。目前，ASIC 项目中从设计到验证的行业标准在团队规模和持续时间方面的比例为 1:3 到 1:4。
• 软件验证： 虽然“vibe coding”一个网站并不需要验证，但任务关键型分布式系统和监管严格的企业级智能体（agents）则需要。

规范问题

一个主要的瓶颈是“规范问题”：人类往往无法精确地规范他们想要的东西。Axiom 将其视为一个交互式过程，其中 AI 建议规范（猜想），而证明器验证它们，从而迭代地完善目标。

技术挑战与限制

Rice's Theorem 与可判定性

虽然 Rice's Theorem 指出，对于所有程序，程序的非平凡属性无法进行形式化验证，但 Axiom 专注于验证绝大多数有用的程序。其目标是将复杂的任务分解为足够小的组件，使其变得可证明。

扩展与上下文窗口

随着证明过程的增长（有时每 1 行代码对应 20 行证明），上下文窗口的限制成为一个问题。Axiom 通过以下方式解决此问题：

• 自动非正式化 (Auto-informalization)： 将形式化 Lean 代码转换回非正式摘要，以维持高层级的追踪。
• 循环一致性 (Cyclic Consistency)： 反复进行形式化与非正式化，以确保逻辑保持严密。

通往 AGI 的路径与递归自我改进

Carina Hong 断言，仅靠非正式数学系统永远无法达到数学 AGI，因为人类专家评分无法扩展。为了实现超智能，AI must 必须能够生成自己的验证式数据并进行递归自我改进，而无需依赖有限的人类专家库。

Axel API

为了加速生态系统，Axiom 提出发布了 Axel (Axiom Lean Engine)，一套用于 Lean 的元编程工具。这一基础设施允许其他开发者和前沿实验室进行大规模的证明验证与操作，从而可能作为其他 LLM 的验证伙伴。