Fugu-MT 論文翻訳(概要): Theorem Prover as a Judge for Synthetic Data Generation

論文の概要: 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 20:12:09.144277
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: http://creativecommons.org/licenses/by/4.0/
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%の精度向上を達成した。

関連論文リスト

R-PRM: Reasoning-Driven Process Reward Modeling [53.06844294668382]
プロセス・リワード・モデル(Process Reward Models, PRM)は、各推論ステップを評価することによって、有望なソリューションとして登場した。既存のPRMは評価スコアを直接出力し、学習効率と評価精度の両方を制限する。推論駆動プロセスリワードモデリング(R-PRM)を提案する。 R-PRMは限られたアノテーションからシードデータを生成し、効果的にモデルの推論能力をブートストラップします。
論文参考訳（メタデータ） (2025-03-27T09:23:08Z)
The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
大規模言語モデルの推論効率を向上させるために,Unsupervised Prefix Fine-Tuning (UPFT)を導入した。 UPFTはラベル付きデータや徹底的なサンプリングの必要性を取り除く。実験の結果,UPFTは教師付き手法の性能と一致していることがわかった。
論文参考訳（メタデータ） (2025-03-04T18:56:03Z)
DeLTa: A Decoding Strategy based on Logit Trajectory Prediction Improves Factuality and Reasoning Ability [3.2561294196141835]
本稿では,事実的精度と推論的推論を両立させる新しい復号法を提案する。提案手法は,トランスフォーマーの下位層から上位層へのロジットの軌跡を解析することにより,次の確率を調節する。 TruthfulQAの実験では、DeLTaはベースラインよりも4.9%改善されている。
論文参考訳（メタデータ） (2025-03-04T07:07:17Z)
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization [22.935127114462475]
本稿では,Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP)法を提案する。 LLMと既存の定理証明データを利用した嗜好データ構築手法を提案する。次に、この選好データ構築手法とカリキュラム学習を統合し、定理証明モデルを反復的に微調整する。
論文参考訳（メタデータ） (2025-02-25T03:07:02Z)
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)
Step Guided Reasoning: Improving Mathematical Reasoning using Guidance Generation and Step Reasoning [7.965282234763401]
Step Guidied Reasoningは、数ショット法よりも安定で一般化可能である。最先端言語モデルにおける数学的性能向上におけるステップガイド推論の意義を実証する。
論文参考訳（メタデータ） (2024-10-18T01:38:24Z)
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)

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

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