Kimi技術チームは先日、Kimina-Proverプレビュー版の技術レポートを発表し、1.5Bと7Bパラメーターのモデル蒸留版、データ生成用のKimina-Autoformalizer-7Bモデル、そして改訂版miniF2Fベンチマークデータセットをオープンソース化しました。

Kimina-Proverは、NuminaとKimiチームが共同開発した数学定理証明モデルです。形式的定理証明の分野において、推論主導型の探索パラダイムを採用しており、優れた性能を示しています。

Kimina-ProverはQwen2.5-72Bモデルをベースに、Kimi k1.5の大規模強化学習（RL）プロセスを組み合わせた訓練を受けています。権威あるminiF2F形式数学ベンチマークテストにおいて、Kimina-Proverプレビュー版は、低いサンプリング予算(pass@8192)で80.7％の成功率を達成し、これまでの最良の結果であるBFS Proverの72.95％(pass@2048×2×600+)やDeepSeek-Proverの50.0％(pass@65536)を大幅に上回りました。

微信截图_20250417082955.png

形式的定理証明は、数学とコンピュータサイエンスにおける重要な研究分野であり、厳密な数学的論理とコンピュータプログラムを用いて数学定理の正しさを検証します。しかし、AIに形式的証明を習得させることは非常に困難で、従来の方法では複雑で深い洞察力と創造性を必要とする数学的問題に対処することが難しい場合がありました。近年、大規模言語モデル（LLM）の台頭により、この分野に新たな希望がもたらされましたが、既存の方法には、外部検索への依存、深い推論の捉えにくさ、モデル規模効果の不足など、多くの限界がありました。

これらの限界を克服するために、Kimina-Proverは、大規模強化学習（RL）と「形式的推論パターン」を深く融合させた新しいアプローチを採用し、モデルが完全な証明を生成するための内部「戦略」を直接最適化します。この方法により、モデルはトークンの生成プロセスにおいて、膨大な証明空間を暗黙的に探索し、推論経路を自律的にナビゲートできるようになり、計算コストの大幅な削減と、より柔軟で人間の直感に近い探索方法を実現しています。さらに、Kimina-Proverは最終結果に基づく報酬信号を導入しており、強化学習によるトレーニングプロセスは目標指向型であり、完全に正しく、コンパイラを通過できる証明のみが正の報酬を得ます。

Kimina-Proverの予備的研究成果は著しい進歩を遂げました。miniF2Fベンチマークテストにおいて、Kimina-Proverは80.7％の成功率を達成し、これまでの最良の結果を大幅に上回りました。また、非常に高いサンプル効率を示し、少ないサンプリング回数でも競争力のある結果を得ることができます。さらに、Kimina-Proverの性能はモデルパラメータ規模の増加に伴って継続的に向上しており、これは形式数学分野におけるニューラル定理証明器でこれほど明確な規模効果が観察された初めての事例です。最先端の汎用推論大規模モデルと比較して、Kimina-Proverは形式数学タスクにおいて圧倒的な優位性を示し、形式的に正しく、Leanコンパイラで検証可能な証明を安定的に生成できます。

Kimina-Proverの思考プロセスは高い説明可能性を備えており、ユーザーはモデルがどのように段階的に証明を導き出したかを確認できます。これはモデルの動作を理解し、失敗原因を診断するのに役立ち、数学教育補助ツールとしての可能性も秘めています。研究チームは、Kimina-Proverの性能はモデル規模とコンテキスト長の増加に伴って著しく拡張できると述べており、「推論に基づくニューラル証明器」の可能性を初期検証しました。大規模強化学習と人間のような推論パターンを組み合わせたこの方法は、自動化された推論、ひいては汎用人工知能（AGI）の発展に新たな道を切り開くでしょう。

コミュニティの参加と研究の進展を促進するために、Kimi技術チームはKimina-Proverの1.5Bと7Bパラメータの蒸留版、データ生成用のKimina-Autoformalizer-7Bモデル、そして改訂版miniF2Fベンチマークデータセットをオープンソース化しました。

  • Arxiv技術レポート:https://arxiv.org/abs/2504.11354

  • GitHubコードリポジトリ:‍https://github.com/MoonshotAI/Kimina-Prover-Preview‍

  • Hugging Faceモデルダウンロード:https://huggingface.co/collections/AI-MO/kimina-prover-preview-67fb536b883d60e7ca25d7f9