論文の概要: Reliable Fine-Grained Evaluation of Natural Language Math Proofs

• arxiv url: http://arxiv.org/abs/2510.13888v1
• Date: Tue, 14 Oct 2025 02:59:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-17 21:15:14.5138
• Title: Reliable Fine-Grained Evaluation of Natural Language Math Proofs
• Title（参考訳）: 自然言語数学証明の信頼性評価
• Authors: Wenjie Ma, Andrei Cojocaru, Neel Kolhe, Bradley Louie, Robin Said Sharif, Haihan Zhang, Vincent Zhuang, Matei Zaharia, Sewon Min,
• Abstract要約: 本稿では,0-7スケールの微粒なスコアをモデル生成数学の証明に割り当てる評価器を開発するための体系的手法を提案する。 ProofBenchは,6つの主要な数学コンペティションから145の問題にまたがる,詳細な証明評価のエキスパートによる最初のデータセットである。 本稿では,強力な推論バックボーンLMと参照解とマーキングスキームからのリッチコンテキストを組み合わせた評価器ProofGraderと,シンプルなアンサンブル手法を提案する。
• 参考スコア（独自算出の注目度）: 30.992321135182905
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers; however, generating and verifying natural language math proofs remains an open challenge. We identify the absence of a reliable, fine-grained evaluator for LLM-generated math proofs as a critical gap. To address this, we propose a systematic methodology for developing and validating evaluators that assign fine-grained scores on a 0-7 scale to model-generated math proofs. To enable this study, we introduce ProofBench, the first expert-annotated dataset of fine-grained proof ratings, spanning 145 problems from six major math competitions (USAMO, IMO, Putnam, etc) and 435 LLM-generated solutions from Gemini-2.5-pro, o3, and DeepSeek-R1. %with expert gradings. Using ProofBench as a testbed, we systematically explore the evaluator design space across key axes: the backbone model, input context, instructions and evaluation workflow. Our analysis delivers ProofGrader, an evaluator that combines a strong reasoning backbone LM, rich context from reference solutions and marking schemes, and a simple ensembling method; it achieves a low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming naive baselines. Finally, we demonstrate its practical utility in a best-of-$n$ selection task: at $n=16$, ProofGrader achieves an average score of 4.14 (out of 7), closing 78% of the gap between a naive binary evaluator (2.48) and the human oracle (4.62), highlighting its potential to advance downstream proof generation.
• Abstract（参考訳）: 数学推論のための大規模言語モデル(LLM)の最近の進歩は、最終解を容易に検証できるタスクに主に焦点を当てているが、自然言語の数学的証明の生成と検証はオープンな課題である。 我々は, LLM 生成数学証明の信頼性, 微粒化評価器の欠如を臨界ギャップとみなす。 そこで本研究では,0-7スケールの微粒なスコアをモデル生成数学の証明に割り当てる評価器を開発し,検証するための体系的手法を提案する。 そこで本研究では,Gemini-2.5-pro,o3,DeepSeek-R1の6大数学コンペ(USAMO,IMO,Putnamなど)と435 LLM生成ソリューションから145の課題にまたがる,詳細な証明評価のエキスパートによる最初のデータセットであるProofBenchを紹介する。 %であった。 ProofBenchをテストベッドとして使用し、バックボーンモデル、入力コンテキスト、インストラクション、評価ワークフローなど、キー軸間の評価器設計空間を体系的に探索する。 我々の分析では,強力な推論バックボーンLM,参照解とマーキングスキームからのリッチコンテキスト,および単純なアンサンブル手法を組み合わせた評価器ProofGraderが,0.926の低い平均絶対誤差(MAE)を専門家のスコアに対して達成し,ナイーブベースラインを著しく上回る結果を得た。 ProofGraderは平均スコア4.14(7点中7点)を達成し、単純二項評価器(2.48点)と人間のオラクル(4.62点)のギャップの78%を閉じ、下流の証明生成を前進させる可能性を強調した。

関連論文リスト

• RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflows [8.700422995850152]
  State-of-the-art (SOTA) LLMは、証明ベースのOlympiad問題から、IMO 2025問題のほとんどを解決するまで、進歩してきた。 本稿では,90 Gemini 2.5 Pro生成ソリューションのコーパスを用いて,詳細なエラーアノテーションを用いた1-4スケールで評価を行った。 分析の結果、モデルが不正確な解を確実にフラグ付けできるが、部分クレジットの割り当て方法にキャリブレーションのギャップがあることがわかった。
  論文  参考訳（メタデータ） (2025-10-10T05:47:40Z)
• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• UTMath: Math Evaluation with Unit Test via Reasoning-to-Coding Thoughts [7.856746367263317]
  本稿では,大規模言語モデルの評価を目的とした頑健な評価フレームワークであるUTMath Benchmarkを紹介する。 これは9つの数学領域にまたがる1053個の最先端問題を含み、平均68個のテストケースがある。 最高の性能モデルであるo1-miniはわずか32.57%の問題を解き、o1-previewは27.16%、GPT-4oは26.93%であった。
  論文  参考訳（メタデータ） (2024-11-11T18:59:02Z)
• 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)

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

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