# Axiom 用形式化验证做数学推理，Putnam 竞赛 12 题全解，Verina 基准 187/189

> 原标题：🔬Scaling Past Informal AI - Carina Hong, Axiom Math

- 来源：Latent Space
- 发布时间：2026-06-03T19:27:49.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/35518
- 原文：https://www.latent.space/p/axiom

## 摘要

Axiom 这家成立七个月的初创公司，在 2025 年 Putnam 数学竞赛里解出了全部 12 道题，限时内得分 8/12，不限时则拿到满分 120 分，超过了已知的 DeepSeek 成绩（103/120）。CEO Carina Hong 说，他们的模型在 Verina ProofGen 基准上跑出了 187/189（约 99%），而 OpenAI...

## 推荐理由

HKR 三项都站得住：Putnam 限时成绩和 o3 的 4.9% 一对比，故事性就出来了；187/189 和 12 道题的具体数字让信息有抓手；话题本身踩在推理能力、评测公信力和 OpenAI 竞争这几个热点上。分数定在 80 是合适的，因为这是一篇 Latent Space 的访谈和研究分享，不是一次大规模模型发布，影响力范围有限。

## 锐评

Axiom 的思路是把数学证明交给 Lean 这类形式化验证工具去检查对错，而不是靠统计概率猜答案。这相当于给模型装了个不会放水的判卷老师，训练时能拿到绝对准确的反馈。他们在 Verina ProofGen 上拿了 187/189，而 OpenAI o3 上次公开的成绩只有 4.9%，差距很大。但这里得打个折：o3 的成绩是旧数据，而且 Axiom 没说自己模型多大、跑一次推理要烧多少钱。

Putnam 竞赛不限时拿满分确实厉害，说明模型在给定足够算力后能把难题啃下来。限时 8/12 则暴露了速度短板，可能推理链太长或者搜索步骤太多。Carina Hong 反复提“让聪明叠加”，本质是用可验证的正确结果当积木，一层层往上盖，避免模型在错误基础上瞎发挥。这个想法不新，但做出实际成绩的团队不多。

现在还缺三块信息：一是模型在数学之外的迁移能力，二是训练用了多少合成数据、有没有数据污染，三是推理成本到底多高。如果跑一道题要烧几千美元，那离实用还远。另外，正文没提他们和 DeepSeek 的对比是否在同等时间预算下进行，这点先别太激动。