論文の概要: Theorem Prover as a Judge for Synthetic Data Generation

• arxiv url: http://arxiv.org/abs/2502.13137v1
• Date: Tue, 18 Feb 2025 18:57:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-19 14:02:11.100644
• Title: Theorem Prover as a Judge for Synthetic Data Generation
• Title（参考訳）: 合成データ生成の判断者としての定理証明
• Authors: Joshua Ong Jun Leang, Giwon Hong, Wenda Li, Shay B. Cohen,
• Abstract要約: RLHF(Reinforcement Learning from Human Feedback)において、人間のアノテーションを定理証明に置き換える枠組みを提案する。 複数の大規模言語モデル(LLM)でTP-as-a-JudgeとRFを適用し、ベンチマークをわずか3,508サンプルで改善し、MultiArithmのMistral-7Bで5.56%の精度を達成した。
• 参考スコア（独自算出の注目度）: 22.124954482278536
• License:
• Abstract: The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuring the validity of intermediate reasoning steps remains a significant challenge, affecting data quality. While formal verification via theorem provers effectively validates LLM reasoning, the autoformalisation of mathematical proofs remains error-prone. In response, we introduce iterative autoformalisation, an approach that iteratively refines theorem prover formalisation to mitigate errors, thereby increasing the execution rate on the Lean prover from 60% to 87%. Building upon that, we introduce Theorem Prover as a Judge (TP-as-a-Judge), a method that employs theorem prover formalisation to rigorously assess LLM intermediate reasoning, effectively integrating autoformalisation with synthetic data generation. Finally, we present Reinforcement Learning from Theorem Prover Feedback (RLTPF), a framework that replaces human annotation with theorem prover feedback in Reinforcement Learning from Human Feedback (RLHF). Across multiple LLMs, applying TP-as-a-Judge and RLTPF improves benchmarks with only 3,508 samples, achieving 5.56% accuracy gain on Mistral-7B for MultiArith, 6.00% on Llama-2-7B for SVAMP, and 3.55% on Llama-3.1-8B for AQUA.
• Abstract（参考訳）: 数学的推論における合成データの需要は、大規模言語モデル(LLM)の数学的能力を高める可能性から増大している。 しかし、中間的推論ステップの有効性を保証することは、データ品質に影響を与える重要な課題である。 定理証明器による形式的検証はLLM推論を効果的に検証するが、数学的証明の自己形式化は誤りを起こしやすい。 これに対し、反復的自己形式化は、定理証明者の形式化を反復的に洗練し、誤りを軽減し、リーン証明者の実行率を60%から87%に向上させるアプローチである。 そこで我々は, 定理証明の形式化を利用して, LLM中間推論を厳格に評価し, 自動形式化と合成データ生成を効果的に統合する手法であるTheorem Prover as a Judge (TP-as-a-Judge)を紹介した。 最後に,Reinforcement Learning from Theorem Prover Feedback (RLTPF)について述べる。 TP-as-a-Judge と RLTPF はベンチマークをわずか3,508サンプルで改善し、MultiArithのMistral-7Bで5.56%、SVAMPのLlama-2-7Bで6.00%、AQUAのLlama-3.1-8Bで3.55%の精度向上を達成した。

関連論文リスト

• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  推論能力は汎用知能の重要な構成要素である。 OpenAIのoシリーズモデルなどのプロプライエタリ企業による最近の進歩は、推論タスクに顕著な進歩をもたらした。 本稿では、数学的推論タスクのための textbfOutcome textbfREwtextbfArd ベースの強化 textbfLearning により達成できる性能限界を追求する新しい RL フレームワーク OREAL を提案する。
  論文  参考訳（メタデータ） (2025-02-10T18:57:29Z)
• Bridging Internal Probability and Self-Consistency for Effective and Efficient LLM Reasoning [53.25336975467293]
  パープレキシティや自己整合性などの手法の第一理論誤差分解解析について述べる。 パープレキシティ法は、適切な整合関数が存在しないため、かなりのモデル誤差に悩まされる。 本稿では、自己整合性とパープレキシティを統合したReasoning-Pruning Perplexity Consistency(RPC)と、低確率推論経路を排除したReasoning Pruningを提案する。
  論文  参考訳（メタデータ） (2025-02-01T18:09:49Z)
• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,より優れたサンプル効率を有する定理証明手法であるProofAugを提案する。 本手法は,オープンソースのDeepseek-math-7bベースモデルとIsabelle証明アシスタントを用いて,miniF2F-testベンチマークで検証した。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• 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)

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

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