Mistral AI、Lean 4向け形式検証モデル「Leanstral 1.5」を公開

Mistral AIは、Lean 4での形式検証に対応したApache-2.0ライセンスのモデル「Leanstral 1.5」を公開した。総パラメータ119B、アクティブパラメータ6Bで、miniF2Fを飽和させ、PutnamBenchでは672問中587問を解いた。FATE-Hで87%、FATE-Xで34%と新たなstate-of-the-artを達成し、Hugging Faceと無料APIで利用できる。