一道普特南数学竞赛题,用高配置证明模型跑一遍,过去动辄三百美元起。Mistral 这次给出的成绩单里,同样量级的题目,四美元。
这个数字比模型跑分本身更值得停下来看一眼。Mistral 刚发布的 Leanstral 1.5,是一个开源证明模型,专攻 Lean 4 形式化证明——让机器写出能被编译器逐字验证、不容狡辩的数学或代码证明。
发生了什么:参数、协议、跑分一次讲清
Leanstral 1.5 是 119B 总参数、6B 激活参数的 MoE 结构,Apache-2.0 协议开源,权重挂在 Hugging Face,还配了一个免费 API。
三个基准的成绩:miniF2F 验证集和测试集都是 100%;PutnamBench 672 道题解出 587 道;研究生和博士级抽象代数基准 FATE-H、FATE-X,分别解出 87 题和 34 题,官方称为新纪录。
跑分本身不新鲜,几乎每家做证明模型的都能在某个基准上刷到高分。真正的分水岭在下一节的成本对照上。
便宜在哪:同一道题,不同门派报价不一样
同样解 PutnamBench,Seed-Prover 1.5 的高配设置估计要花 300 美元以上一题,单题预算是 10 个 H20-day;Aleph Prover 大概 54 到 68 美元一题。
要注意,跑分比它高的几家,有的靠自然语言提示指路,有的是拿更高的推理预算硬堆出来的。这不是同一条起跑线的比赛,只是同一件事上,Leanstral 给出了更低的报价。
工程基准 FLTEval 也一起开源了,这是基于费马大定理仓库真实 PR 构建的测试集。pass@8 从 31.9 提到 43.2,超过 Opus 4.6 的 39.6,成本只有对方的七分之一。
代码里能不能找到真 bug
比跑分更有说服力的是两个真实案例。第一个是给 AVL 树的插入删除操作证明 O(log n) 时间复杂度,模型跑了 270 万 token、22 次上下文压缩才收尾。
第二个案例更有意思:用 Aeneas 把 Rust 代码翻译成 Lean,让 Leanstral 自己推断代码意图、生成正确性命题,证不出来就反过来证伪。
57 个开源仓库里跑了一遍,标出 47 处违反命题,其中 11 个是真实 bug,5 个此前无人上报。一个例子是 datrs/varinteger 库的 zigzag 解码,输入达到 U64.MAX 时整数溢出,debug 模式崩溃、release 模式静默出错。
这类边界情况,常规测试和模糊测试通常抓不住。但 47 处里只有 11 个是真 bug,其余是命题定义本身有偏差——说明这套流程目前更像补充手段,替代不了人工审计,也替代不了模糊测试。
不同团队看到这个结果,反应会不一样:
| 关注方向 | 更现实的做法 |
|---|---|
| 关心推理成本的技术决策者 | 拿它验证证明生成的成本能否控制,但要用同等预算复测,不能直接照搬官方数字 |
| 做代码审查、漏洞排查的团队 | 当成静态验证的补充工具,和模糊测试、人工审计并行,不要单独依赖它 |
| 想接入生产流程的团队 | 先把要证明的规范和验证目标定义清楚,这一步模型不会替你想 |
便宜之后,门槛去哪儿了
Leanstral 展示的核心曲线是 test-time scaling:把每次尝试的 token 预算从 5 万拉到 400 万,PutnamBench 上解题数从 44 一路爬到 587,曲线全程单调向上,没有饱和迹象。模型不是想不出就放弃,而是一直改文件、一直推演,直到预算耗尽或者证完。这是它和一般数学模型的分界线:不只是会写证明,还知道怎么在长时间尺度上把算力换成结果。
这像极了编译器刚出现时的处境。机器码不再需要手写,门槛从怎么写转移到了要写什么。形式化验证现在也是同样的位移:证明这一步变便宜了,难的是先把规范定义清楚——要证明什么性质、验证目标怎么设、证明结果怎么接进现有工程流程。这些不是模型能替你想的。
跑到 400 万 token 才拿到最高分,也说明便宜是相对的:省下来的是单题美元成本,烧掉的是时间和推理算力,这笔账企业接入时得自己算清楚。
接下来值得盯的,不是下一个跑分纪录,而是三件事:同等预算下的成本对比会不会被更多团队复现;它在企业内部真实代码库、而不是开源示例库上的表现如何;Seed-Prover 这类对手会不会也走上降成本这条路。证明确实变便宜了,但决定这套东西能不能用起来的,从来不是模型会不会证,而是你有没有能力先把要证的东西说清楚。