論文の概要: Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs

• arxiv url: http://arxiv.org/abs/2603.15510v1
• Date: Mon, 16 Mar 2026 16:37:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-17 18:28:58.602612
• Title: Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
• Title（参考訳）: すべての不変量に等しくない - SLMによるプログラム検証の高速化を目的としたトレーニングデータのキュレーション
• Authors: Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu, Nina Narodytska, Guy Katz,
• Abstract要約: WondaはASTベースの正規化を通じてノイズの多いデータを洗練するパイプラインであり、続いてセマンティックリライトと保証可能な品質保証による拡張が続く。 我々は、このキュレートされたデータセット上の微調整された小言語モデル(SLM)が、一貫性と顕著な性能向上をもたらすことを実証する。
• 参考スコア（独自算出の注目度）: 6.863007247776099
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The synthesis of inductive loop invariants is a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on hard instances, generating invariants that are invalid or computationally ineffective. While fine-tuning is a natural route to mitigate this limitation, obtaining high-quality training data for invariant generation remains an open challenge. We present a rigorous data curation pipeline designed to extract high-quality training signals from raw verifier-generated invariants. First, we formalize the properties required for a high-quality training invariant. Second, we propose Wonda, a pipeline that refines noisy data via AST-based normalization, followed by LLM-driven semantic rewriting and augmentation with provable quality guarantees. We demonstrate that fine-tuning Small Language Models (SLMs) on this curated dataset result in consistent and significant performance gain. In particular, a fine-tuned 4B parameter model matches the utility of a GPT-OSS-120B baseline and approaches the state-of-the-art GPT-5.2, without incurring reasoning-time overhead. On challenging instances from the recent InvBench evaluation suite, our approach doubles the invariant correctness and speedup rates of base models; and improves their Virtual Best Performance (VBP) rates on the verification task by up to 14.2%.
• Abstract（参考訳）: 帰納ループ不変量の合成は、自動プログラム検証において重要なボトルネックとなる。 LLM(Large Language Models)はこの問題の緩和を約束するが、ハードインスタンスでは失敗することが多く、無効あるいは計算的に非効率な不変値を生成する。 微調整はこの制限を緩和する自然な方法であるが、不変生成のための高品質なトレーニングデータを取得することはオープンな課題である。 原検証器生成不変量から高品質なトレーニング信号を抽出するための厳密なデータキュレーションパイプラインを提案する。 まず、高品質なトレーニング不変量に必要な特性を定式化する。 第2に,ASTをベースとした正規化によるノイズの多いデータを洗練するパイプラインであるWondaを提案する。 我々は、このキュレートされたデータセット上の微調整された小言語モデル(SLM)が、一貫性と顕著な性能向上をもたらすことを実証する。 特に、微調整された4BパラメータモデルはGPT-OSS-120Bベースラインの実用性と一致し、推論時間オーバーヘッドを発生させることなく最先端のGPT-5.2にアプローチする。 最近のInvBench評価スイートの課題インスタンスでは、ベースモデルの不変の正しさとスピードアップ率を2倍にし、検証タスクにおけるVBP(Virtual Best Performance)レートを最大14.2%改善しています。

関連論文リスト

• Benchmarking Few-shot Transferability of Pre-trained Models with Improved Evaluation Protocols [123.73663884421272]
  より強力な事前訓練モデルと改良された適応アルゴリズムによって、わずかなショット転送が革新されている。 FEWTRANSは10種類のデータセットを含む総合的なベンチマークである。 FEWTRANS をリリースすることにより,数発の転写学習研究において再現性の向上を合理化するための厳密な "ルーラー" の提供を目指す。
  論文  参考訳（メタデータ） (2026-02-28T05:41:57Z)
• InstructDiff: Domain-Adaptive Data Selection via Differential Entropy for Efficient LLM Fine-Tuning [35.89674702985539]
  InstructDiffは、ドメイン適応選択基準として微分エントロピーを運用する統合フレームワークである。 InstructDiffは、数学的推論に関する完全なデータトレーニングよりも17%の相対的な改善を達成し、一般的な命令追従の52%を実現している。
  論文  参考訳（メタデータ） (2026-01-30T14:15:44Z)
• Winning the Pruning Gamble: A Unified Approach to Joint Sample and Token Pruning for Efficient Supervised Fine-Tuning [71.30276778807068]
  サンプルプルーニングとトークンプルーニングを戦略的に協調する統合フレームワークを提案する。 Q-Tuningは、トレーニングデータの12.5%しか使用せず、全データSFTベースラインに対する平均38%の改善を実現している。
  論文  参考訳（メタデータ） (2025-09-28T13:27:38Z)
• Uncertainty Aware Learning for Language Model Alignment [97.36361196793929]
  異なるタスクシナリオのモデルアライメントを改善するために,不確実性認識学習(UAL)を提案する。 トレーニングのラベルの平滑化値を個々のサンプルの不確実性に応じて適応的に設定する。 広く使われているベンチマーク実験では、我々のUALは標準教師あり微調整よりも著しく優れています。
  論文  参考訳（メタデータ） (2024-06-07T11:37:45Z)
• Adversarial Fine-Tuning of Language Models: An Iterative Optimisation Approach for the Generation and Detection of Problematic Content [0.0]
  大規模言語モデル(LLM)における意図しない有害コンテンツ生成の課題に挑戦する。 私たちの2つのアプローチでは、潜在的に有害なプロンプトを生成するために微調整された敵モデルと、これらのプロンプトを反復的に識別するように最適化された判断モデルを採用しています。 本研究は, 初歩的なモデルテキストタダを用いて, わずか数ラウンドでGPT-4よりも13%高い精度を達成できることを示す。
  論文  参考訳（メタデータ） (2023-08-26T05:20:58Z)
• Constraining Generative Models for Engineering Design with Negative Data [11.432911164773488]
  本稿では,制約を満たす出力に向けて生成モデルを導くための新しいトレーニング手法を提案する。 我々の負データ生成モデル(NDGM)の定式化は、古典的モデルよりも容易に優れている。
  論文  参考訳（メタデータ） (2023-06-27T02:47:59Z)
• PTP: Boosting Stability and Performance of Prompt Tuning with Perturbation-Based Regularizer [94.23904400441957]
  損失景観を平滑化できる摂動型正規化器を即時チューニングに導入する。 我々は乱数ノイズベースと逆数ベースを含む2種類の摂動型正規化器を設計する。 我々の新しいアルゴリズムは,SuperGLUEベンチマークとFewGLUEベンチマークでそれぞれ1.94%,2.34%の最先端のプロンプトチューニング手法を改善した。
  論文  参考訳（メタデータ） (2023-05-03T20:30:51Z)
• Conditional Denoising Diffusion for Sequential Recommendation [62.127862728308045]
  GAN(Generative Adversarial Networks)とVAE(VAE)の2つの顕著な生成モデル GANは不安定な最適化に苦しむ一方、VAEは後続の崩壊と過度に平らな世代である。 本稿では,シーケンスエンコーダ,クロスアテンティブデノナイジングデコーダ,ステップワイズディフューザを含む条件付きデノナイジング拡散モデルを提案する。
  論文  参考訳（メタデータ） (2023-04-22T15:32:59Z)
• Training Discrete Deep Generative Models via Gapped Straight-Through Estimator [72.71398034617607]
  再サンプリングのオーバーヘッドを伴わずに分散を低減するため, GST (Gapped Straight-Through) 推定器を提案する。 この推定子は、Straight-Through Gumbel-Softmaxの本質的な性質に着想を得たものである。 実験により,提案したGST推定器は,2つの離散的な深部生成モデリングタスクの強いベースラインと比較して,優れた性能を享受できることが示された。
  論文  参考訳（メタデータ） (2022-06-15T01:46:05Z)

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

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