北京
一个开源模型，拿下高中数学到奥赛难度的全部考题，顺手还能从开源库中捞出没人发现的溢出漏洞，这事真实发生了。Mistral AI近日把Leanstral 1.5放到了Hugging Face，附带免费API，用的还是Apache 2.0协议。它的专长不是聊天、不是写诗，而是对着数学证明和代码一行一行做形式化验证，在Lean 4编程语言里找逻辑裂缝。
形式化验证听起来门槛很高，说白了就是像裁判一样，用严格的逻辑规则检查每一步推导是否准确，数学证明能不能成立，软件会不会有隐藏错误。Mistral这次把这个能力全灌进了一个模型里。在数学基准miniF2F上，Leanstral 1.5直接拿了100%的正确率，题目覆盖从高中到数学奥林匹克难度。换到更考验功力的PutnamBench，672道来自Putnam数学竞赛的题目，它解出587道。抽象代数方面，FATE‑H和FATE‑X两项专门测试硕士、博士级别群论、环论任务的基准，也分别给出了87%和34%的顶尖成绩。这些数字放在一起，说明模型不是只背了题，而是在代数推理这一整套链条里跑通了。
更有意思的是代码验证那一半。虽然训练目标是数学，Leanstral 1.5在面对真实代码时照样顶用。Mistral公开的实验里，它一口气扫了57个开源仓库，从里面揪出5个此前没人发现的bug，其中一个出现在Rust的varinteger库，是个溢出问题。这类bug拖着不修，随时可能在线上环境崩出一地鸡毛。开源的模型能替开源项目自动查错，相当于给社区加了一条免费的防线。
技术路线也不复杂：中期训练、监督微调再加强化学习，把形式验证这个原本偏学术的领域，往实用方向推了一大步。对做数学研究的人，这是随时可调用的证明助手；对写关键系统的开发者，这是能跑在管线里的自动化督察。一个模型同时踩稳数学和代码两条船，还坚持开源，让人好奇接下来它还会翻出哪些藏在复杂逻辑深处的老漏洞。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
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.
