論文の概要: Can a Lightweight Automated AI Pipeline Solve Research-Level Mathematical Problems?
- arxiv url: http://arxiv.org/abs/2602.13695v1
- Date: Sat, 14 Feb 2026 09:36:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-17 14:17:28.347883
- Title: Can a Lightweight Automated AI Pipeline Solve Research-Level Mathematical Problems?
- Title（参考訳）: 軽量自動AIパイプラインは研究レベルの数学的問題を解くことができるか?
- Authors: Lve Meng, Weilong Zhao, Yanzhi Zhang, Haoxiang Guan, Jiyan He,
- Abstract要約: 大規模言語モデル(LLM)は、最近、厳密な数学的証明を生成することに成功している。
次世代モデル(例えば、Gemini 3 Pro, GPT-5.2 Pro)が洗練された研究グレードの問題を解決することを実証する。
- 参考スコア（独自算出の注目度）: 1.8139694172697178
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Large language models (LLMs) have recently achieved remarkable success in generating rigorous mathematical proofs, with "AI for Math" emerging as a vibrant field of research. While these models have mastered competition-level benchmarks like the International Mathematical Olympiad and show promise in research applications through auto-formalization, their deployment via lightweight, natural-language pipelines for research problems remains underexplored. In this work, we demonstrate that next-generation models (e.g., Gemini 3 Pro, GPT-5.2 Pro), when integrated into a streamlined automated pipeline optimized for citation-based verification, can solve sophisticated research-grade problems. We evaluate our pipeline on two novel datasets: (1) the ICCM problem sets (comparable to the S.-T. Yau College Student Mathematics Contest) proposed by leading mathematicians, and (2) the "First Proof" problem set, consisting of previously unpublished research questions. Our pipeline generated candidate proofs for all problems in the first two ICCM sets and the "First Proof" set. The solutions for the first two ICCM sets and Problem 4 of the "First Proof" set have been fully verified by our team. All generated proofs have been submitted to the official organization, and our generated results are publicly available. We plan to open-source the complete pipeline methodology in due course.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、最近、活発な研究分野として「数学のためのAI」が出現し、厳密な数学的証明を生み出すことに成功している。
これらのモデルは、International Mathematical Olympiadのような競合レベルのベンチマークを習得し、自動形式化による研究応用の約束を示す一方で、研究問題のための軽量で自然言語パイプラインによるデプロイメントは、まだ未定である。
本研究では,次世代モデル(Gemini 3 Pro, GPT-5.2 Proなど)を,引用に基づく検証に最適化された合理化自動パイプラインに統合することで,高度な研究グレードの問題を解決できることを実証する。
我々は,(1)先進数学者が提案するICCM問題集合(S.T.Yau大学数学コンテストと同等)と(2)未発表の研究課題からなる「最初の証明」問題集合の2つの新しいデータセット上でパイプラインを評価した。
私たちのパイプラインは、最初の2つのICCMセットと"First Proof"セットのすべての問題に対する候補証明を生成しました。
最初の2つのICCMセットと"First Proof"セットの問題4に対するソリューションは、私たちのチームによって完全に検証されています。
生成したすべての証明が公式組織に提出され、生成された結果が公開されています。
今後、完全なパイプライン方法論をオープンソース化する予定です。
関連論文リスト
- Towards Autonomous Mathematics Research [48.29504087871558]
Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。
具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。
我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
論文 参考訳（メタデータ） (2026-02-10T18:50:15Z) - Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。
本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。
我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
論文 参考訳（メタデータ） (2025-08-21T14:15:40Z) - Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems [9.041749463376599]
本稿では,自然言語の数学的コーパスから高品質な証明中心ベンチマークを合成するフレームワークProof2Hybridを提案する。
我々のフレームワークとベンチマークは、AIシステムの数学的インテリジェンスに関する、より深い研究の波の道を開く。
論文 参考訳（メタデータ） (2025-08-04T08:59:36Z) - REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning [12.343823629674368]
私たちはREAL-Proverという,Lean 4.0用の新たなオープンソースステップワイドな定理証明ツールを紹介します。
我々の証明者は、特に大学レベルの数学問題の解法における性能を高める。
実験では、教師付き微チューン定理のみを用いた証明器は23.7%の成功率で競合する結果が得られる。
論文 参考訳（メタデータ） (2025-05-27T01:26:11Z) - AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning dataset [8.13404599390294]
本稿では,AI Mathematical Olympiad-Progress Prize 2 (AIMO-2) コンペティションの受賞について述べる。
最先端の数学的推論モデルを構築するための私たちのレシピは、3つの重要な柱に依存しています。
論文 参考訳（メタデータ） (2025-04-23T17:13:04Z) - Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。
OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
論文 参考訳（メタデータ） (2025-03-27T11:20:17Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。