Daily Arxiv

世界中で発行される人工知能関連の論文をまとめるページです。
このページはGoogle Geminiを活用して要約し、非営利で運営しています。
論文の著作権は著者および関連機関にあり、共有する際は出典を明記してください。

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

Created by
  • Haebom

作者

Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang,ヨンウイウ、ユウヘンウウ、イーハングシア、ホアジアンシン、ファンヤン、ホイユアンヤング、ホンギイアン、チョンユアン、ティヤンジャン、チーチャン、ユエチャン、ジチョン、ティヤンウンハオ、Jianqiu Zhao、Yichi Zhou、トーマス

概要

この論文では、大規模言語モデル（LLM）の数学的推論能力を向上させるためのSeed-Proverという新しいモデルを提案します。 Seed-ProverはLeanと呼ばれる形式検証言語を活用し、強化学習を通じて証明プロセスを繰り返し改善します。 IMOレベルの問題解決のために3つの推論戦略を設計し、過去のIMO問題の78.1％を証明し、MiniF2Fデータセットで最高のパフォーマンスを達成し、PutnamBenchでも50％以上のパフォーマンスを示しました。従来の方法よりはるかに優れた性能を示し、Leanの幾何学的支援不足の問題を解決するためにSeed-Geometryという幾何推論エンジンをさらに開発し、IMO 2025で6問題のうち5問題を完全に証明する成果を収めました。これは、形式検証と長期的な思考プロセスを活用した自動化された数学的推論の分野における重要な進歩を意味します。

Takeaways、Limitations

•
Takeaways:
◦
LLMを用いた数学的定理証明の分野で大きな進歩を遂げました。
◦
Leanのような形式言語を活用した強化学習の効果を実証しました。
◦
Seed-ProverとSeed-Geometryは、従来の自動化された数学的推論システムよりもはるかに優れた性能を示しました。
◦
IMO 2025 実際の参加を通じてモデルの実用性を検証しました。
•
Limitations:
◦
Lean 言語への依存性が高い。他の形式言語へのスケーラビリティに関する研究が必要です。
◦
Seed-Geometry を含む geometry サポート拡張が必要です。
◦
すべての数学的問題を解決できるわけではなく、特定の種類の問題に強みを与えることができます。
◦
計算の複雑さと処理時間の分析が不足しています。
👍
Made with Slashpage