論文の概要: RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
- arxiv url: http://arxiv.org/abs/2609.00062v1
- Date: Sun, 30 Aug 2026 14:23:48 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-02 16:31:35.806507
- Title: RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving
- Title（参考訳）: RePro: LLM数学的問題解決の信頼性評価のための証明済みベンチマーク書き換え
- Abstract要約: 本稿では,Lean-oriented Neural theorem proversをベンチマーク書き換えに統合するために,Proof-Verified Benchmark Rewriting (RePro)を提案する。
ReProは問題を書き直し、リーン検証の証明によって確認された正確さで回答を再生する。
GSM8KとMATHの実験では、ReProの保持された再書き込みインスタンスが100%明確に定義され、実現可能であり、答えの正しさが得られることが示されている。
- 参考スコア（独自算出の注目度）: 27.43470148162019
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Data contamination undermines the reliable evaluation of large language models (LLMs) on mathematical problem solving. While rewriting-based evaluation mitigates memorization, existing methods lack guarantees of problem validity and answer correctness. We propose Proof-Verified Benchmark Rewriting (RePro), the first framework to integrate Lean-oriented neural automated theorem provers (ATPs) into benchmark rewriting, which rewrites problems and regenerates answers with correctness ensured by Lean-verified proofs. Experiments on GSM8K and MATH show that RePro's retained rewritten instances achieve 100% well-definedness, feasibility, and answer correctness, while existing methods still produce invalid or incorrect instances. Moreover, several models exhibit accuracy drops on proof-verified rewritten benchmarks, suggesting that their performance is sensitive to surface-level and structural variations and may partly reflect memorization effects. Our source code and data are available at https://github.com/AI4Engi/RePro.
- Abstract（参考訳）: データ汚染は、数学的な問題解決における大規模言語モデル(LLM)の信頼性評価を損なう。
書き直しに基づく評価は暗記を緩和するが、既存の手法では問題の有効性と答えの正しさの保証が欠如している。
これは、リーン指向の神経自動定理プローバ(ATP)をベンチマーク書き換えに統合する最初のフレームワークであり、問題を書き直し、リーン検証された証明によって保証された正確さで回答を再生する。
GSM8KとMATHの実験では、ReProの保持されたリライトされたインスタンスが100%明確に定義され、実現可能であり、答えの正しさが得られた。
さらに、いくつかのモデルは証明検証された再記述されたベンチマークに精度低下を示し、それらの性能は表面レベルや構造の変化に敏感であり、部分的に記憶効果を反映する可能性があることを示唆している。
ソースコードとデータはhttps://github.com/AI4Engi/ReProで公開されています。
関連論文リスト
- Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving [13.87786274932945]
リーンで証明されたLCM支援定理のベンチマークは、すべての解決されたインスタンスがマシンチェックされた証明を持ってくるため、本質的に信頼できるものとして扱われることが多い。
コーパススケールの静的チェッカーを用いて4,833個の結果を得た。
本稿では,フォールト分類法,自動チェッカーとリコール指向のセマンティック監査プロンプト,および公式な数学データセットの作成を導くための標準リリースを提案する。
論文 参考訳（メタデータ） (2026-06-28T16:46:36Z) - Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs [6.320612572570053]
Mask-Proofは、実際の証明を自動チェック可能なマスク付きタスクに変換するパイプラインだ。
結果として得られたMask-ProofBenchは、様々な研究領域で292のキュレートされた問題を含んでいる。
我々の評価器は、専門家アノテータとの96.8%の合意を達成し、忠実で再現性があり、ステップレベルの数学的推論に匹敵する測定を可能にする。
論文 参考訳（メタデータ） (2026-06-13T11:26:09Z) - Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts [19.455779459310982]
このギャップは,ほとんどのエビデンス生成パイプラインにおいて,コンパイル優先の目的が暗黙的であることに起因している,と我々は主張する。
本稿では,人間の証明リファクタリングに触発されたプロセス誘導アプローチを提案する。
論文 参考訳（メタデータ） (2026-06-02T14:56:10Z) - Learning to Repair Lean Proofs from Compiler Feedback [4.55626337217127]
教師付き学習問題としてリーン証明修復について検討する。
APRIL(Automated Proof repair in Lean)は、260,000の教師付き定理のデータセットである。
我々は、診断条件付き監視を、フィードバックを利用するプローバーのための補完的な訓練信号と見なしている。
論文 参考訳（メタデータ） (2026-02-03T01:53:56Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。
本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。
トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
論文 参考訳（メタデータ） (2026-01-05T10:16:41Z) - Incorporating Self-Rewriting into Large Language Model Reasoning Reinforcement [54.63337314382886]
自己書き起こしフレームワークを導入し、モデルが独自の推論テキストを書き直し、その後、書き直し推論から学習し、内部思考プロセスの品質を向上させる。
アルゴリズム設計において、モデルの一貫した正当性によって定義される「単純な」サンプルのみを書き換える選択的な書き換え手法を提案する。
モデルサイズが異なる多様なタスクの実験は、自己書き換えの有効性を検証する。
論文 参考訳（メタデータ） (2025-11-20T13:10:52Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - Repairing vulnerabilities without invisible hands. A differentiated replication study on LLMs [5.10123605644148]
自動脆弱性修復(AVR: Automated Vulnerability repair)は、プログラム修復の急激な分岐である。
近年の研究では、大きな言語モデル(LLM)が従来の手法より優れていることが示されている。
論文 参考訳（メタデータ） (2025-07-28T16:39:16Z) - Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。
その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。
VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
論文 参考訳（メタデータ） (2025-05-17T04:16:36Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z) - LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
そこで我々は,SummEditsと呼ばれる10ドメインのベンチマークで不整合検出ベンチマークを作成し,実装する新しいプロトコルを提案する。
ほとんどのLLMはSummEditsで苦労しており、パフォーマンスはランダムに近い。
最も優れたモデルであるGPT-4は、推定された人間のパフォーマンスよりも8%低い。
論文 参考訳（メタデータ） (2023-05-23T21:50:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。