北京
周四深夜，一位做嵌入式系统的开发者正对着测试脚本挠头——第无数次因为一个边界条件没覆盖，上线的前一晚又得重跑全量回归。手机忽然弹出一条开源动态，他扫了一眼，直接切了屏幕：Mistral发布了一个叫 Leanstral 1.5 的模型，专攻形式化定理证明，性能指标盖过了 Anthropic 的 Opus 4.6。用他的话说，“这不只是另一种聊天机器人，这是能写可验证数学证明的推理引擎。”
这一周，Mistral AI 的这枚“静默弹”并没有走“更大更强”的路子。Leanstral 1.5 只为 Lean 4 这门证明助手语言而生，直接对标 FLTEval 基准。结果很干脆：单次尝试通过率（Pass@1）达到 28.9%，相比初代版本的 21.9% 跳了一截；八次采样通过率（Pass@8）冲到 43.2%，把 Opus 4.6 的 39.6% 甩在身后。更关键的是，所有这些证明都由 Lean 4 的内核自动完成校验，逻辑链条里容不下半点想象——换句话说，这里没有模型“编故事”的空间，每一行推导要么完全正确，要么直接被机器拒绝。
为什么一群人对一个数学基准的通过率格外兴奋？因为这和写作文、画图不一样。Leanstral 干的是硬核的形式推理：指定一个定理，它输出一串从公理出发的严格推演，每一个步骤都被形式化语言锁死。就比如要证明“两个奇数的和是偶数”，模型不会输出含糊的自然语言解释，而是用 Lean 4 环环构造加法交换律、单位元等证明项，再由系统验证项的类型是否匹配。这种模式带来的零幻觉特性，恰好击中了眼下对 AI 可信性的焦虑——你可以不服模型的结论，但如果内核校验过，那就是真的。
跳出数学的小圈子，Leanstral 1.5 印证了一个更广的趋势：小体量、聚焦单一领域的模型，可以在特定任务上碾压通用大厂数倍参数量的产品。Mistral 没有堆万亿级参数，而是针对形式推理这块压缩出一套紧凑架构，效果不降反升。对于把形式验证工具（Lean、Coq、Isabelle 等）往生产级软件测试流程里推的团队来说，这个信号尤其强烈。一个能自动写出可验证证明的模型，等于给编译器提前塞了一整套自我检查能力——将来可能出现变更提交即触发形式化验证，在编译时就把低阶 bug 拦下来，而不是靠跑几十遍测试用例。
伴随模型一起放出的还有 FLTEval 评测全集的完全开源，模型权重在 Hugging Face 上随手可得，消费级显卡就能跑。Mistral 用这一套组合拳表明，开源社区拿到的不只是分数，而是可以直接复现、可迭代的工程地基。
当然，Leanstral 1.5 代替不了那些帮你写邮件的聊天机器人。但对任何在乎“可证明正确”的软件、经得起机器检验的数学，或者盯着 AI 推理底层逻辑的人来说，这个周三的发布确实值得多看两眼。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
