精选理由
MistralAI 的 Leanstral 1.5 用 6B 活跃参数就拿下 miniF2F 满分，每个问题才 4 美元，做数学证明的可以试试。
MistralAI 推出了 Leanstral 1.5，一个基于 Apache-2.0 许可证的 Lean 4 证明智能体。该模型采用 MoE 架构，总参数量 119B，仅激活 6B 参数。它在 miniF2F 上获得 100% 准确率，在 FATE-H 和 FATE-X 上分别达到 87% 和 34% 的新 SOTA。在 PutnamBench 上，它解决了 587/672 个问题，每问题成本约 4 美元。现在可通过 vLLM 进行部署。
AI 翻译 · 中文
MistralAI 推出了 Leanstral 1.5，一个基于 Apache-2.0 许可证的 Lean 4 证明智能体。该模型采用 MoE 架构，总参数量 119B，仅激活 6B 参数。它在 miniF2F 上获得 100% 准确率，在 FATE-H 和 FATE-X 上分别达到 87% 和 34% 的新 SOTA。在 PutnamBench 上，它解决了 587/672 个问题，每问题成本约 4 美元。现在可通过 vLLM 进行部署。
Congrats to @MistralAI on Leanstral 1.5! 🎉 An Apache-2.0 Lean 4 proof agent that punches way above its size: 🧩 MoE: 119B total, just 6B active 📐 100% on miniF2F 🎓 New SOTA on FATE-H (87%) & FATE-X (34%) ⚡ 587/672…