06:24
官方一手marktechpost@Asif Razzaq
官方一手marktechpost@Asif Razzaq推荐理由：Mistral开源了Leanstral 1.5，一个能解数学竞赛题的Lean 4代码模型，Apache-2.0免费商用，实测解决587道Putnam难题，值得看看。
代码Agent
共 1 条相关 AI 资讯
7月4日
06:24
Mistral AI发布Leanstral 1.5，一个Apache-2.0许可的Lean 4代码代理模型。该模型采用混合专家架构，总参数119B，每次推理仅激活6.5B参数。它在miniF2F基准上达到饱和，并在PutnamBench数学竞赛题中解决了587/672道问题。文章还介绍了其架构设计、基准测试结果和真实bug发现案例。