論文の概要: Propose, Solve, Verify: Self-Play Through Formal Verification

• arxiv url: http://arxiv.org/abs/2512.18160v1
• Date: Sat, 20 Dec 2025 00:56:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-23 18:54:32.212423
• Title: Propose, Solve, Verify: Self-Play Through Formal Verification
• Title（参考訳）: Propose, Solve, Verify: 形式検証によるセルフプレイ
• Authors: Alex Wilf, Pranjal Aggarwal, Bryan Parno, Daniel Fried, Louis-Philippe Morency, Paul Pu Liang, Sean Welleck,
• Abstract要約: 形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。 本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。 そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
• 参考スコア（独自算出の注目度）: 75.44204610186587
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Training models through self-play alone (without any human data) has been a longstanding goal in AI, but its effectiveness for training large language models remains unclear, particularly in code generation where rewards based on unit tests are brittle and prone to error propagation. We study self-play in the verified code generation setting, where formal verification provides reliable correctness signals. We introduce Propose, Solve, Verify (PSV) a simple self-play framework where formal verification signals are used to create a proposer capable of generating challenging synthetic problems and a solver trained via expert iteration. We use PSV to train PSV-Verus, which across three benchmarks improves pass@1 by up to 9.6x over inference-only and expert-iteration baselines. We show that performance scales with the number of generated questions and training iterations, and through ablations identify formal verification and difficulty-aware proposal as essential ingredients for successful self-play.
• Abstract（参考訳）: 自己プレイのみによるトレーニングモデル(人間データなしで)は、AIの長年の目標だったが、大規模な言語モデルのトレーニングの有効性は、特にユニットテストに基づく報酬が不安定でエラーの伝播の傾向にあるコード生成において、いまだに不明である。 形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。 本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。 PSVを使ってPSV-Verusをトレーニングします。これは3つのベンチマークで、推論のみのベースラインとエキスパートイテレーションのベースラインよりも、pass@1を最大9.6倍改善します。 そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。

関連論文リスト

• Self-Questioning Language Models [58.73276539661649]
  本稿では,提案者がトピックを与えられ,解答者に対する質問を生成する非対称なセルフプレイフレームワークを提案する。 提案者と解答者はともに強化学習を通じて訓練される。 3桁の乗算、OMEGAベンチマークの代数問題、Codeforcesのプログラミング問題である。
  論文  参考訳（メタデータ） (2025-08-05T17:51:33Z)
• Can Large Reasoning Models Self-Train? [51.0277533541394]
  多数決投票を簡単な自己フィードバック機構として利用し、強化学習において自己学習が持続できるかどうかを検討する。 この基本的なアプローチは、モデルの推論性能だけでなく、次のRLイテレーションでより良い品質フィードバックを生成する能力も改善します。 しかし、我々の分析では、このような自己学習パラダイムの限界も明らかにしています - 自己回帰の長いRLは、報酬のハッキングにつながるため、突然、そして完全なパフォーマンスが崩壊します。
  論文  参考訳（メタデータ） (2025-05-27T17:16:00Z)
• Continuous Self-Improvement of Large Language Models by Test-time Training with Verifier-Driven Sample Selection [6.471199527741301]
  VDS-TTT(Verifier-Driven Sample Selection for Test-Time Training)と呼ばれる新しいフレームワークを導入する。 学習した検証器を用いて、生成された応答のプールをスコアし、高いランクの擬似ラベル付き例からのみ選び、微調整を施す。 低ランクなLoRAアダプタパラメータのみを微調整し、適応効率と高速収束を確保する。
  論文  参考訳（メタデータ） (2025-05-26T03:54:47Z)
• RLSR: Reinforcement Learning from Self Reward [0.0]
  大規模な言語モデルでは,参照解を使わずに自己判断によって効果的に自己改善できることを示す。 実験により, モデルが真理の答えを得られずに, 信頼性の高い報奨信号を提供できることを示した。 この作業は、自己指向学習を通じて継続的に改善される自律型AIシステムに向けた重要なステップである。
  論文  参考訳（メタデータ） (2025-05-12T23:51:04Z)

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

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