論文の概要: The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs

• arxiv url: http://arxiv.org/abs/2506.21621v1
• Date: Mon, 23 Jun 2025 13:31:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-30 21:12:22.933746
• Title: The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs
• Title（参考訳）: オープン証明コーパス: LLM生成数学的証明の大規模研究
• Authors: Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova, Margulan Ismoldayev,
• Abstract要約: 提案するOpen Proof Corpus(OPC, Open Proof Corpus)は, 最先端のLLMによって生成される5000以上の人的評価された証明からなるデータセットである。 OPCは、証明生成研究における幅広い適用性と下流利用のために特別に設計された。 本研究では,(1)自然言語と形式的証明生成のパフォーマンスギャップ,(2)最終回答精度と完全正当性との相違,(3)証明品質に対する最良選択の影響について考察する。
• 参考スコア（独自算出の注目度）: 7.20909461915203
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In recent months, large language models (LLMs) have made significant progress in mathematical proof generation, but further advancement is hindered by the lack of a large-scale, high-quality dataset of human-evaluated proofs. While expensive to create, such a dataset is essential for driving improvements in training and enabling a rigorous analysis of proof generation capabilities. In this work, we present the Open Proof Corpus (OPC), a dataset comprising over 5,000 human-evaluated proofs produced by state-of-the-art LLMs. The OPC was specifically designed for broad applicability and downstream usage in proof generation research and is the first to include a substantial number of correct, LLM-generated solutions to problems from prestigious mathematics competitions such as the USAMO and IMO. Using the OPC, we explore critical questions in automated proof generation: (1) the performance gap between natural language and formal proof generation, (2) the discrepancy between final-answer accuracy and full-proof validity, and (3) the impact of best-of-n selection on proof quality. Finally, to showcase the utility of the OPC, we finetune an 8B-parameter model on the dataset, obtaining a model that performs on par with the best model, Gemini-2.5-Pro, on the task of evaluating proof correctness.
• Abstract（参考訳）: 近年,大規模言語モデル (LLM) は数学的な証明生成において大きな進歩を遂げているが,人間の評価された証明の大規模かつ高品質なデータセットが欠如しているため,さらなる進歩が妨げられている。 作成には費用がかかるが、このようなデータセットはトレーニングの改善を推進し、証明生成能力の厳密な分析を可能にするために不可欠である。 本研究では,最先端のLLMによって生成される5000以上の人的評価された証明からなるデータセットであるOpen Proof Corpus(OPC)を提示する。 OPCは、証明生成研究における幅広い適用性と下流の使用のために特別に設計され、USAMOやIMOのような高名な数学コンペティションの課題に対する、かなり多くの正しいLCM生成ソリューションを含む最初のものである。 OPCを用いて,(1)自然言語と形式的証明生成のパフォーマンスギャップ,(2)最終回答精度と完全正当性との相違,(3)証明品質に対する最良選択の影響など,自動証明生成における重要な課題を探索する。 最後に、OPCの実用性を示すために、データセット上に8Bパラメータモデルを微調整し、検証正当性を評価するタスクにおいて、最良のモデルであるGemini-2.5-Proと同等に動作するモデルを得る。

関連論文リスト

• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-05-20T15:13:32Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。