最近、バイトダンスのシードAIチームは、シードプロバー1.5という数学的推論モデルを発表しました。このモデルは国際数学オリンピック（IMO）で優れた成績を収め、金メダルを獲得し、人工知能が数学分野でまた一つの飛躍を遂げたことを示しています。

シードプロバー1.5はScaling Law理論を採用しており、IMO2025の前5問を16.5時間で解き、1問を失った結果、35点を獲得し、金メダルの基準に達しました。この成績はグーグルのGeminiと同等であり、バイトが以前に開発したモデルは当時4問を3日かけて解いたものの、銀メダルにとどまりました。明らかに、シードプロバー1.5の成果はAI数学的推論モデルにとって新たな基準を設定しています。

image.png

このモデルの成功は偶然ではありません。その中心には大規模な強化学習の導入があります。訓練により、モデルの証明問題の成功率は最初の50％からほぼ90％まで上昇しました。さらに、シードプロバー1.5は北米数学コンテストであるパットナムで過去最高の成績を記録し、その問題解決能力の高さを示しています。

シードプロバー1.5の技術報告書には、Agentic ProverとSketch Modelという2つの重要な革新が紹介されています。Agentic Proverは新しい形式化数学的推論方法を採用し、Leanなどの形式言語を使って検証可能な証明を行います。この方法は従来の自然言語推論よりも厳密ですが、同時により困難でもあります。この難点を克服するために、シードプロバー1.5は推論中に複数のツールを呼び出すことができ、例えばLeanの数学ライブラリMathlibを検索したり、Pythonスクリプトを書いて計算を行うことができます。

image.png

一方、Sketch Modelはモデルが「下書き」を作成するのを支援するものです。このモデルは人間の数学者が問題を解決する思考法を模倣し、非公式な証明の下書きをまず行い、重要な補題やアイデアをリストアップした後、形式的な証明に変換します。混合報酬信号を使用した強化学習戦略により、Sketch Modelは全体的な論理構築能力を向上させ、複雑な問題の難易度を効果的に低下させています。

結論として、シードプロバー1.5はバイトがAI数学的推論分野において持つイノベーションと実力を示しており、今後の数学研究や教育にも新たな可能性をもたらしています。

論文のURL：https://arxiv.org/pdf/2512.17260