論文の概要: 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%の精度向上を達成した。

関連論文リスト

• The Surprising Effectiveness of Test-Time Training for Abstract Reasoning [64.36534512742736]
  モデル推論能力向上のためのメカニズムとして,テストタイムトレーニング(TTT)の有効性を検討する。 TTTはARCタスクのパフォーマンスを大幅に改善し、ベースとなる微調整モデルと比較して最大6倍の精度向上を実現した。 本研究は,ニューラルネットワークモデルにおける抽象的推論改善の道筋として,明示的な記号探索が唯一の道ではないことを示唆している。
  論文  参考訳（メタデータ） (2024-11-11T18:59:45Z)
• 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)
• 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)
• Scaling Relationship on Learning Mathematical Reasoning with Large Language Models [75.29595679428105]
  本研究では,事前学習損失,教師付きデータ量,拡張データ量が教師付きLDMの推論性能に与える影響について検討する。 複数のモデルからの拒絶サンプルは、LLaMA-7BをGSM8Kの49.3%の精度に押し上げ、監督された微調整(SFT)の精度を35.9%上回る結果となった。
  論文  参考訳（メタデータ） (2023-08-03T15:34:01Z)
• False Correlation Reduction for Offline Reinforcement Learning [115.11954432080749]
  本稿では,実効的かつ理論的に証明可能なアルゴリズムであるオフラインRLに対するfalSe Correlation Reduction (SCORE)を提案する。 SCOREは、標準ベンチマーク(D4RL)において、様々なタスクにおいて3.1倍の高速化でSoTA性能を達成することを実証的に示す。
  論文  参考訳（メタデータ） (2021-10-24T15:34:03Z)

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

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