開発チームは本日、形式検証および数学的推論に特化した大規模言語モデルLeanstral 1.5を正式に公開した。Apache-2.0ライセンスのもと無料公開され、推論時には6Bパラメータのみを動員するスリムアーキテクチャを採用している。本モデルはミニF2Fベンチマークを完全攻略し、プットナム数学コンテストの672問中587問を解決。さらにFATE-Hで87％、FATE-Xで34％の正答率を記録し、それぞれの新規記録を更新した。 学習プロセスは中間学習、教師あり微調整、CISPOによる強化学習の3段階で構成される。定理に対してコンパイラフィードバックを基に証明を反復推敲するマルチターン環境と、ファイルシステムや言語サーバーを活用して実コードの検証を行うエージェント環境で訓練された結果、数百万トークン規模の長距離推論でも解題を継続し、計算リソースを直接的な解題数へ変換する高いスケーラビリティを実現した。推論コストは問題あたり約4ドルと、競合の大幅な低コスト化に成功している。 実務応用における実証も進んでおり、形式手法が実際の開発ワークフローに直結する可能性を示した。木構造データ構造の平衡化アルゴリズムAVL木の時間計算量O(log n)の厳密な形式証明に成功。また、RustコードをLeanに変換するパイプラインと組み合わせた自動検証では、57リポジトリを対象に検証した結果、11件の重大な欠陥を特定。そのうち5件は従来のテストでは発見が困難な未報告バグだった。 重量はHugging Faceで公開され、APIエンドポイントも無料で提供を開始した。開発チームは統合環境の推奨と公式ドキュメントの公開を通じて、一般の開発者および研究者が実用的な形式証明環境を容易に構築できるよう支援する。本リリースにより、難解な形式検証ツールがオープンソース化され、数学研究から堅牢なソフトウェアエンジニアリングまで、実用的な推論基盤としての普及が加速すると期待される。