拿满分数学验证的AI，竟揪出生产代码5个bug

周三，Mistral AI的工程师们盯着测试结果沉默了几秒——他们本来只想证明Leanstral 1.5在形式化数学上有多强，没想到这个开源模型顺手从57个代码仓库里挖出了5个从未被发现的漏洞。如果给验证能力打分，miniF2F基准上的100%正确率已经足够说明数学功力；但真正让开发者圈子骚动的，是它在一个叫varinteger的Rust库里定位到一个溢出bug——不是示例项目，是真实跑在生产环境里的代码。

Leanstral 1.5是为Lean 4语言构建的形式化验证模型。Lean 4本身就是一个既能写数学证明、也能做软件正确性验证的语言，而Leanstral 1.5的训练管线把这种双重能力推到了新高度。Mistral没有披露过多架构细节，只说明训练过程整合了中期训练（mid-training）、监督式微调（SFT）以及强化学习（RL），最终拿出一个采用Apache 2.0协议开源的模型，直接挂在Hugging Face上，还附赠免费API。这种分发姿态在形式验证圈子里并不多见，仿佛在说：别只把形式化验证锁在数学系的地下室，它应该下到CI/CD流水线里去干脏活。

先看它的数学成绩单。根据The Decoder的报道，Mistral让Leanstral 1.5在miniF2F基准上跑出了100%的分数。miniF2F是一个专门衡量形式化数学证明能力的测试集，题目跨度从高中难度一路延伸到数学奥林匹克层级。而在更硬核的PutnamBench上——那套包含了672道普特南数学竞赛原题的测试集——它解出了587道。普特南竞赛一直以刁钻著称，能在上面拿到近九成的正确率，证明模型并不只是背诵教科书套路，而是确实抓住了一些推理本质。此外，在检验硕士、博士级别代数能力的FATE-H和FATE-X基准上，Leanstral 1.5分别拿到87%和34%的最佳成绩，涉及的领域包括群论、环论等。当然，34%这个数字也提醒着人们，前沿数学推理的壁垒还在，但87%的高阶表现已经足够让不少研究生感到压力。

数学之外，代码验证成为这次发布真正的“出圈点”。Mistral虽然承认Leanstral 1.5的训练重心偏向数学，但“顺手”在代码审计上做的实验，却展示了形式化验证工具落地工业界的可行路径。工程师们把模型丢到57个开源仓库里进行验证扫描，结果找到5个“此前未知”的bug。其中最引人注目的一条，是varinteger这个Rust库中的溢出错误。整数溢出是系统编程中的经典隐患，静态检查工具往往只能抓到最浅层的模式，而由Lean 4驱动的模型能够在数学层面定义不变量，用证明的方式确保某些边界条件永不被打破。这种靠“证明”而非靠“穷举测试”的思路，一旦跑通，对持续集成流水线的影响会是结构性的。

这件事在叙事上带来的冲击，比对单个bug的修复本身更大。过去人们谈论形式化验证，脑海里浮现的画面大多是定理证明器在学术论文里优雅地推进哥德巴赫猜想，或者某个操作系统内核用成千上万行证明代码保证内存安全。Leanstral 1.5的价值在于，它用Apache 2.0的开源协议，以及一个只需调用API就能使用的交互方式，把这张“学术邮票”贴到了工兵铲上。开发者不再需要先花几个月啃《Software Foundations》才能写出第一条验证，而是可以考虑让自动化验证模型跑到PR的检查项里，和lint、单元测试并列。Mistral这一步，隐隐指向一个方向：传统模糊测试（fuzzing）和人工审计的边界会收窄，取而代之的是一层由形式化模型驱动的自动化证明外衣。

下一阶段值得追看的，是Mistral会不会放出Leanstral的更大变体，或者干脆把验证能力深度嵌入自家的API矩阵。另一个风向标是开源社区的真实动作：当第一个重磅Rust项目在技术博客里宣布把Lean 4验证接入CI流水线，并披露它早期拦截了多少线上事故时，形式化验证才真的从论文走向工单。目前这5个bug还只是“扫出来”的样本，但如果未来每周的开发者周报里都多出一栏“AI形式化验证发现的缺陷”，那么Mistral这次看似安静的模型发布，或许才是真正踩中了痛点。

当然，疑问并没有完全被解答。100%的miniF2F分数是否意味着模型对训练集中某些证明模式的过拟合？PutnamBench上错失的85道题卡在什么类型的推理上？34%的FATE-X正确率说明博士级代数推理的大门还只是推开了一条缝。不过，在一个急于把大语言模型包装成“思考机器”的年份，Leanstral 1.5提供了一种更克制、也更扎实的叙事——它不去聊AGI的时间表，而是说，我这里有一个100%能过数学验证的模型，它还找到了5个真实bug，代码和权重都开源了，不信你可以自己跑一遍。