論文の概要: 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倍改善します。
そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
関連論文リスト
- Reasoning Core: A Scalable Procedural Data Generation Suite for Symbolic Pre-training and Post-Training [2.62112541805429]
Reasoning Coreは、コア形式ドメイン間で検証可能なシンボリック推論データを手続き的に生成するスケーラブルなスイートである。
各タスクは厳密な検証のための外部解決器と組み合わせられ、カリキュラム設計のための継続的な難易度制御が認められる。
実験によると、Reasoning Coreのデータを事前トレーニングに混ぜることによって、下流の推論が改善され、保存されたり、わずかに改善された言語モデリングの品質が向上する。
論文 参考訳（メタデータ） (2026-03-02T18:59:29Z) - Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
本稿では,Refinement Provenance Inference (RPI)監査タスクをRefinement Provenance Inference (RPI)として定式化する。
本稿では,ロジットレベルの信号で教師が強制する可能性機能を融合させるロジットベースのフレームワークであるReProを提案する。
トレーニング中、ReProはシャドウファインチューニングを通じて転送可能な表現を学び、訓練データアクセスなしで、見えない犠牲者の証明を推測するために軽量のリニアヘッドを使用する。
論文 参考訳（メタデータ） (2026-01-05T10:16:41Z) - LaSeR: Reinforcement Learning with Last-Token Self-Rewarding [54.72617309922891]
RLVR(Reinforcement Learning with Verifiable Rewards)は、Large Language Models(LLM)の推論能力を高めるためのコアパラダイムとして登場した。
従来、LLMは2つの異なるプロンプトテンプレートを使用してソリューションと自己検証をシーケンシャルに生成し、効率を大幅に低下させる必要があった。
本稿では,従来のRLVR損失をMSE損失で増大させるアルゴリズムであるLaSeR(Reinforcement Learning with Last-Token Self-Rewarding)を提案する。
論文 参考訳（メタデータ） (2025-10-16T17:55:11Z) - Self-Questioning Language Models [58.73276539661649]
本稿では,提案者がトピックを与えられ,解答者に対する質問を生成する非対称なセルフプレイフレームワークを提案する。
提案者と解答者はともに強化学習を通じて訓練される。
3桁の乗算、OMEGAベンチマークの代数問題、Codeforcesのプログラミング問題である。
論文 参考訳（メタデータ） (2025-08-05T17:51:33Z) - Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。
有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。
生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
論文 参考訳（メタデータ） (2025-07-22T08:13:01Z) - ReVeal: Self-Evolving Code Agents via Reliable Self-Verification [11.875519107421312]
自己検証とツールベースの評価を通じてコード生成を進化させる強化学習フレームワークであるReVealを紹介する。
推論において、この強化された自己検証により、3つしかトレーニングされていないLiveCodeBenchでは、自己構築されたテストとツールフィードバックを使用して、20ターン以上のコードを継続的に進化させることができる。
これらの調査結果は、RLトレーニングとテストタイムスケーリングのためのスケーラブルなパラダイムとしてのReVealの約束を強調し、より堅牢で自律的なAIエージェントへの道を開いた。
論文 参考訳（メタデータ） (2025-06-13T03:41:04Z) - 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) - Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。
しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。
本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
論文 参考訳（メタデータ） (2025-02-20T18:32:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。