Leanstral 1.5：誰でも使える形式検証ツール

Leanstral 1.5 は、無料の Apache-2.0 ライセンスモデルで、119B の総パラメータと 6B のアクティブパラメータを持ち、形式検証において大きな性能向上を実現しました。miniF2F を飽和させ、PutnamBench で 587/672 の問題を解決し、FATE-H (87%) と FATE-X (34%) で最先端の結果を達成。中間トレーニング、教師ありファインチューニング、CISPO を用いた強化学習を経て、エージェント指向の証明工学と実世界のコード検証で優れた能力を発揮し、57 のリポジトリで 5 つの未知のバグを発見しました。完全にオープンソース化され、Hugging Face と無料 API から利用可能で、Lean 4 での実用的な証明工学が可能になりました。