Mistral Leanstral 1.5: 形式検証で数学ベンチマーク優位、実コード内のバグを5件検出
Mistral AI が Leanstral 1.5（Lean 4 形式検証モデル）をオープンソースでリリース。数学ベンチマークで100%達成、57のオープンソースリポジトリスキャンで未知のバグを発見。開発者・数学者向けの実用的なツール。
続きを読む
タグ一覧に戻る
Lean
記事数: 2 件
Google DeepMind の AlphaProof Nexus、56年間未解のエルデシュ問題を含む9件を自動解法――数学証明の新たなAI利用法を実証
形式化検証言語 Lean を用いた記号的フィードバックループにより、OpenAI の自然言語アプローチとは異なる数学証明戦略を確立。数百ドルの推論コストで業界のベンチマークを拡張。
続きを読む