最近の国際数学オリンピック（IMO2025）で、ByteDance Seedチームの自動定理証明システム「Seed-Prover」が優れた成績を収め、大会の4つの問題を成功裏に解決しました。この成果は、Seed-Proverが数学証明分野において重要な進展を遂げたことを示し、複雑な数学問題の解決における人工知能の可能性を示しています。

QQ20250804-113057.png

Seed-Proverは、ByteDance Seedチームの重要な研究プロジェクトであり、深層学習と広範囲な推論技術を通じて、自動定理証明の能力を向上させることを目的としています。IMO2025で、このシステムは過酷な競技環境でも優れた性能を発揮し、以下の問題を成功裏に解決しました:

  • **第1問（組み合わせ論）**: この問題は大会中には適切に解決できませんでしたが、Seed-Proverは後日完全な証明を提供しました。
  • **第2問（幾何学）**: システムはわずか2秒で答えを生成し、検証しました。これにより、計算能力の高さが示されています。
  • **第3問（数論）**: この問題は3日間かけて解決され、証明の内容は2000行にも及んでおり、システムの厳密性を示しています。
  • **第4問（数論）**: 同様に3日間で解決され、詳細な証明として4000行が提供されました。
  • **第5問（組み合わせ論／代数学）**: 1日で解決され、その証明方法は既存の人間による解法とは少し異なっており、システムの革新性を示しています。

Seed-Proverは大会で目覚ましい成績を収めましたが、現在このプロジェクトのモデル重みは公開されていません。ユーザーはプロジェクト資料や関連論文にアクセスできます。チームは今後さらなる情報の公開を計画しており、学術界や開発者たちがこのシステムをよりよく理解し、活用できるようにする予定です。

ByteDance Seedチームのこの業績は、自動定理証明分野に新たな活力をもたらし、数学研究に新たなツールを提供しています。今後の応用と発展を期待しています。

論文のURL:https://arxiv.org/abs/2507.23726 

リポジトリのURL:https://github.com/ByteDance-Seed/Seed-Prover