論文の概要: 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生成数学的証明の大規模研究
• 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と同等に動作するモデルを得る。

関連論文リスト

• ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization [19.226502853809734]
  我々は、Lean 4.0で自動証明最適化のためのニューロシンボリックなフレームワークImProver 2を紹介します。 ImProver 2は、データ効率の高いエキスパートイテレーションパイプラインと、非公式な抽象化と並んで形式的な構造を公開する足場を組み合わせたものだ。 適切な足場とトレーニングを行うことで、小さなモデルは、複雑で多様なメトリクスに対して研究レベルの証明を効果的に再構成し、かなり大きなシステムにマッチし、証明最適化をスケーラブルで学習可能なタスクとして確立できることが示される。
  論文  参考訳（メタデータ） (2026-05-21T02:20:26Z)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness [7.694715050727414]
  大規模言語モデル(LLM)は数学的な問題解決に有効である。 ProofRankは、挑戦的な数学的競争から得られたベンチマークである。 正当性のみのベンチマークでは得られない証明品質にはかなりの違いがある。
  論文  参考訳（メタデータ） (2026-05-11T11:23:36Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。 Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
  論文  参考訳（メタデータ） (2025-10-17T14:45:30Z)
• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• 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)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• 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)
• Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code [0.0]
  Coqの証明アシスタントは、数学的アサーションとソフトウェアの正確性を検証するための厳格なアプローチで際立っている。 人工知能と機械学習の進歩にもかかわらず、Coq構文と意味論の特殊性は大規模言語モデル(LLM)に固有の課題をもたらす。 このデータセットは、10,000以上のCoqソースファイルのコレクションから派生したもので、幅広い命題、証明、定義を含んでいる。
  論文  参考訳（メタデータ） (2024-03-19T10:53:40Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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