論文の概要: Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

• arxiv url: http://arxiv.org/abs/2606.15258v1
• Date: Sat, 13 Jun 2026 11:26:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 16:21:33.164982
• Title: Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
• Title（参考訳）: Mask-Proof: 数学的証明に基づくLLMベースの自動データキュレーションパイプライン
• Authors: Jierui Zhang, Siyuan Tan, Xinhang Li, Longzhuangzhi Lin, Dailin Li, Chengfeng Gu, Xinping Li, Yaxian Hao, Shengjia Liang, Yuxiang Ren, Wenhao Liu,
• Abstract要約: Mask-Proofは、実際の証明を自動チェック可能なマスク付きタスクに変換するパイプラインだ。 結果として得られたMask-ProofBenchは、様々な研究領域で292のキュレートされた問題を含んでいる。 我々の評価器は、専門家アノテータとの96.8%の合意を達成し、忠実で再現性があり、ステップレベルの数学的推論に匹敵する測定を可能にする。
• 参考スコア（独自算出の注目度）: 6.320612572570053
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) are increasingly capable of mathematical problem solving and can even assist with research-level proofs, yet we still lack a scalable and reproducible way to measure step-level reasoning in long proofs across diverse sources. This evaluation gap limits trustworthy AI assistance in proof-certified scientific progress. Existing evaluations often emphasize final answers or rely on costly expert grading, while end-to-end proof generation remains open-ended and hard to verify automatically. We introduce Mask-Proof, a pipeline that turns real proofs into automatically checkable masked-step tasks. It masks key formula steps, provides the necessary surrounding context, and evaluates model reconstructions with an LLM-based equivalence judge using repeated votes for stability. The resulting Mask-ProofBench contains 292 curated problems across diverse research areas. Experiments with 17 models show that reasoning-enhanced models outperform standard models by 12% to 27%. Our evaluator achieves 96.8% agreement with expert annotators, enabling faithful, reproducible, and comparable measurement of step-level mathematical reasoning. Benchmark, annotations, and code are available at https://github.com/weating/Mask-Proof.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、数学的な問題解決能力が増し、研究レベルの証明も支援できるようになりましたが、様々な情報源の長い証明においてステップレベルの推論を測定するためのスケーラブルで再現可能な方法がまだ欠けているのです。 この評価ギャップは、証明された科学的進歩において信頼できるAI支援を制限する。 既存の評価では、最終回答を強調したり、コストのかかる専門家の格付けに依存している場合が多いが、エンドツーエンドの証明生成は、自動検証が難しいままである。 実際の証明を自動チェック可能なマスク付きタスクに変換するパイプラインであるMask-Proofを紹介します。 重要な定式化ステップを隠蔽し、必要な環境を提供し、安定のための繰り返し投票を用いてLLMベースの同値判定器を用いてモデル再構成を評価する。 結果として得られたMask-ProofBenchは、様々な研究領域で292のキュレートされた問題を含んでいる。 17モデルの実験では、推論強化モデルは標準モデルの12%から27%を上回っている。 我々の評価器は、専門家アノテータとの96.8%の合意を達成し、忠実で再現性があり、ステップレベルの数学的推論に匹敵する測定を可能にする。 ベンチマーク、アノテーション、コードはhttps://github.com/weating/Mask-Proof.comで入手できる。

関連論文リスト

• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
  論文  参考訳（メタデータ） (2026-04-07T01:19:41Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Omanic: Towards Step-wise Evaluation of Multi-hop Reasoning in Large Language Models [60.418191092851636]
  OmanicはオープンドメインのマルチホップQAリソースであり、推論プロセスを分析するための構造アノテーションとして分解されたサブクエストと中間回答を提供する。 10,296個の機械によるトレーニング例(Omanic Synth)と967個の専門家による注釈付き評価例(OmanicBench)を含む。
  論文  参考訳（メタデータ） (2026-03-17T15:23:37Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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