精选理由
Mistral开源了Leanstral 1.5，一个能解数学竞赛题的Lean 4代码模型，Apache-2.0免费商用，实测解决587道Putnam难题，值得看看。
Mistral AI发布Leanstral 1.5，一个Apache-2.0许可的Lean 4代码代理模型。该模型采用混合专家架构，总参数119B，每次推理仅激活6.5B参数。它在miniF2F基准上达到饱和，并在PutnamBench数学竞赛题中解决了587/672道问题。文章还介绍了其架构设计、基准测试结果和真实bug发现案例。
AI 翻译 · 中文
Mistral AI发布Leanstral 1.5，一个Apache-2.0许可的Lean 4代码代理模型。该模型采用混合专家架构，总参数119B，每次推理仅激活6.5B参数。它在miniF2F基准上达到饱和，并在PutnamBench数学竞赛题中解决了587/672道问题。文章还介绍了其架构设计、基准测试结果和真实bug发现案例。
Mistral AI released Leanstral 1.5, a free Apache-2.0 code agent model for Lean 4. It saturates miniF2F and solves 587 of 672 PutnamBench problems. The 119B mixture-of-experts activates 6.5B parameters per token. We break…