論文の概要: Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
- arxiv url: http://arxiv.org/abs/2604.05820v1
- Date: Tue, 07 Apr 2026 12:53:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-08 17:42:09.828997
- Title: Reinforcement Learning with Negative Tests as Completeness Signal for Formal Specification Synthesis
- Title（参考訳）: 形式的合成のための完全性信号としての負検定による強化学習
- Authors: Zhechong Huang, Zhao Zhang, Zeyu Sun, Huifeng Sun, Yingfei Xiong,
- Abstract要約: 本稿では,Dafny における仕様記述のための強化学習フレームワーク SpecRL を提案する。
我々は、仕様完全性の信号として、候補仕様によって拒否された負のテストのごく一部を用いる。
実験により、SpecRLはSFTおよびRLよりも仕様強度と検証成功の両方を改善していることが示された。
- 参考スコア（独自算出の注目度）: 7.936959383169967
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The specification synthesis task aims to automatically generate specifications, together with any necessary auxiliary verification annotations, for existing programs. This task is important because such specifications serve as behavioral contracts that support modular reasoning and reusable verification across a codebase. At the same time, it remains challenging because verifier-only feedback is fundamentally incomplete: passing verification establishes soundness, but cannot distinguish weak specifications from strong ones. What is missing is a fine-grained signal for specification completeness. We present SpecRL, a reinforcement learning framework for specification synthesis in Dafny. SpecRL introduces a self-contained pipeline that generates negative tests, i.e., input-output pairs that can never be produced by the program. We use the fraction of these negative tests rejected by a candidate specification as a signal of specification completeness, which is integrated into the reward for RL training. Experiments across four model sizes show that SpecRL improves both specification strength and verification success over SFT and RL with a binary specification-strength reward, generalizes to an out-of-distribution benchmark, and remains competitive on that unseen benchmark compared to much larger general-purpose LLMs.
- Abstract（参考訳）: 仕様合成タスクは、既存のプログラムに必要な補助的な検証アノテーションとともに、仕様を自動的に生成することを目的としている。
このような仕様は、コードベースをまたいだモジュラー推論と再利用可能な検証をサポートする振る舞い契約として機能するため、このタスクは重要です。
検証のみのフィードバックは基本的に不完全であり、検証をパスすることは健全性を確立するが、弱い仕様と強い仕様を区別することはできない。
欠けているのは、仕様の完全性のためのきめ細かい信号です。
本稿では,Dafny における仕様合成のための強化学習フレームワーク SpecRL を提案する。
SpecRLは自己完結型パイプラインを導入し、負のテスト、すなわちプログラムでは生成できない入出力ペアを生成する。
仕様完全性の信号として候補仕様によって拒絶されたこれらの負のテストのごく一部を使用し、RLトレーニングの報奨として統合する。
4つのモデルサイズにわたる実験により、SpecRLはSFTとRLの仕様強度と検証成功の両方をバイナリ仕様強度の報奨で改善し、アウト・オブ・ディストリビューション・ベンチマークに一般化した。
関連論文リスト
- VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications [0.3240750198587795]
自動JML仕様合成における古典的手法と急進的手法を比較した。
提案手法は,構造化された検証フィードバックを用いて,プロンプトを進化させることにより,合成品質をさらに向上させることができるかを検討する。
本稿では,検証誘導型エージェントフレームワークであるVeriActを提案する。
論文 参考訳（メタデータ） (2026-03-31T22:12:15Z) - Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。
本稿では,Cプログラムのメモリ対応形式関数仕様を自動生成するニューロシンボリックフレームワークを提案する。
我々は,メモリ対応の形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。
論文 参考訳（メタデータ） (2026-03-12T15:02:26Z) - CVeDRL: An Efficient Code Verifier via Difficulty-aware Reinforcement Learning [57.24524263804788]
コード検証は、LLMベースのコード生成の検証後において重要な役割を果たす。
既存の教師付き微調整手法は、データの不足、高い失敗率、推論効率の低下に悩まされている。
機能的な報酬しか持たない単純RLは、難しいブランチやサンプルに対して効果的な単体テストを生成することができないことを示す。
論文 参考訳（メタデータ） (2026-01-30T10:33:29Z) - CoT-Saliency: Unified Chain-of-Thought Reasoning for Heterogeneous Saliency Tasks [96.64597365827046]
本稿では,3つの運用上不均一なサリエンシタスクを共同で処理する,最初の統合フレームワークを提案する。
タスクの不均一性を橋渡しする視覚言語モデル(VLM)において、チェーン・オブ・ソート(CoT)推論プロセスを導入する。
我々は,全タスクにまたがる特別なSOTA手法と強力なクローズドソースVLMの整合性を示す。
論文 参考訳（メタデータ） (2025-11-01T04:37:01Z) - EvoSyn: Generalizable Evolutionary Data Synthesis for Verifiable Learning [63.03672166010434]
我々は、進化的、タスクに依存しない、戦略を導いた、実行可能検証可能なデータ合成フレームワークを紹介します。
問題、多様な候補解、検証成果物を共同で合成する。
これは、人間による注釈付きチェックと戦略によるチェックの合意を強制する一貫性に基づく評価器を通じて戦略を反復的に発見する。
論文 参考訳（メタデータ） (2025-10-20T11:56:35Z) - You only need 4 extra tokens: Synergistic Test-time Adaptation for LLMs [50.54173262572369]
大規模言語モデル (LLM) は、金融、医療、農業などの専門分野にますます導入されている。
本稿では,言語モデルに対するラベルフリーテスト時適応について検討し,追加の監督なしにモデルをオンザフライで適応する推論時フレームワークであるSyTTAについて述べる。
論文 参考訳（メタデータ） (2025-10-11T14:00:39Z) - Hybrid Reinforcement: When Reward Is Sparse, It's Better to Be Dense [36.71358559780692]
HEROは、検証者信号と報酬モデルスコアを構造化された方法で統合する強化学習フレームワークである。
HEROはRMのみのベースラインと検証者のみのベースラインを一貫して上回り、検証可能なタスクと検証しにくいタスクの両方で大きな利益を上げている。
論文 参考訳（メタデータ） (2025-10-08T17:09:41Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - Foreseeing the Benefits of Incidental Supervision [83.08441990812636]
本稿では,実験を行なわずに,特定の目標タスクに対して,様々な種類の偶発信号の利点を定量化できるかどうかを考察する。
本稿では,PABI(PAC-Bayesian motivated informativeness measure)を提案する。
論文 参考訳（メタデータ） (2020-06-09T20:59:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。