Mistral推出代码验证智能体Leanstral 性价比超越Claude

AI可能需要另一个AI来监督其工作。法国AI公司Mistral正在致力于提高AI代码生成的可靠性，推出了Leanstral，这是一个使用开源Lean编程语言构建的代码验证智能体。

Mistral认为，形式化代码验证减少了人工代码审查的需求，这是一个可能耗时的过程。证明、测试、代码检查和规范可以帮助AI代码智能体立足现实，从而产生更好的输出。

Leanstral已经以开放权重（Apache 2.0）的形式发布，作为Mistral Vibe中的智能体模式，并通过免费API端点提供。它还配有一个名为FLTEval的基准测试结果，这是一个尚未发布的测试，专门用于评估AI模型如何处理工程证明。

根据Mistral的说法，Leanstral-120B-A6B在FLTEval上的表现超越了参数更多的开源竞争对手，如GLM5-744B-A40B、Kimi-K2.5-1T-32B和Qwen3.5-397B-A17B。

但更值得注意的可能是Leanstral对成本的影响。

该AI公司声称："Leanstral作为Claude套件的高价值替代方案，以极低的价格提供竞争性能：Leanstral pass@2达到26.3分，超过Sonnet 2.6分，而运行成本仅为36美元，相比之下Sonnet需要549美元。在pass@16时，Leanstral达到31.9分，轻松超过Sonnet 8分。"

至于Claude Opus 4.6，Anthropic目前的旗舰模型，它在FLTEval上的得分确实高于Leanstral（pass@16时39.6分对比31.9分）。但Opus的成本为1650美元，而Leanstral在16次通过时仅需290美元，或者单次通过21.9分仅需18美元。

为了证明Leanstral在测试驱动开发方面的熟练处理能力，Mistral让这个编码智能体解决了一个来自Proof Assistant Stack Exchange的实际问题，关于Lean 4代码中的一个bug。

公司报告称，Leanstral成功构建了测试代码来重现故障，然后正确地发现并修复了缺陷。

Mistral还发布了Mistral Small 4，设计为一个全能模型，可以处理推理、编码和指令对话任务，因此用户无需在专门模型之间切换。

Q&A

Q1：Leanstral是什么？它有什么特别之处？

A：Leanstral是Mistral公司推出的代码验证智能体，使用开源Lean编程语言构建。它的特别之处在于能够进行形式化代码验证，减少人工代码审查需求，并且性价比极高，在保持竞争性能的同时成本远低于Claude等竞品。

Q2：Leanstral的性价比优势体现在哪里？

A：Leanstral在FLTEval基准测试中，pass@2模式下仅需36美元就能达到26.3分，超过Claude Sonnet的549美元成本。即使是pass@16模式下达到31.9分，也只需290美元，而Claude Opus达到39.6分需要1650美元。

Q3：Mistral Small 4有什么功能？

A：Mistral Small 4是一个全能模型，可以同时处理推理、编码和指令对话任务，用户无需在不同的专门模型之间切换。它设计为一体化解决方案，简化了用户的使用体验。