論文の概要: Template-Free Dynamic Invariant Detection

• arxiv url: http://arxiv.org/abs/2610.38130v1
• Date: Wed, 28 Oct 2026 01:07:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-03 18:49:36.663277
• Title: Template-Free Dynamic Invariant Detection
• Title（参考訳）: テンプレートフリーな動的不変検出
• Abstract要約: 動的不変検出器は、メソッドの前条件や後条件のような不変性を提案し、実行時に保持しないものを除外する。 大規模言語モデル (LLM) はテンプレートから派生したものの代わりに不変(invariant)を提案できる。 LLMが提案する不変量は、不変評価中に任意のコードを実行することができ、副作用や無限ループを引き起こす。
• 参考スコア（独自算出の注目度）: 1.5701252647539967
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A dynamic invariant detector proposes invariants, such as method pre- and postconditions, and rules out those that do not hold at run time. Traditional detectors propose invariants from a fixed library of templates, which limits their expressiveness. A large language model (LLM) can propose invariants instead of, or in addition to, template-derived ones. With the right prompt and context choices, we found that this idea can both improve the invariants' expressiveness and reduce the cost of inferring the invariants. Greater expressiveness brings complications: an LLM-proposed invariant can execute arbitrary code during invariant evaluation, causing side effects or infinite loops. Our novel instrumentation strategies mitigate these problems. We wrap each candidate and evaluate only one invariant per thread at a time, so nested invariant evaluations cannot trigger one another indefinitely. To recover from non-nested hangs, we monitor each run for stalls and retry it under a growing time budget. Because we cannot prove a candidate side-effect-free in advance, we use delta debugging over the invariants evaluated during a failing test to isolate and disable a side-effecting candidate without discarding the rest of the run. We compared our implementation, Oca, to the popular template-based Daikon invariant detector on real open-source Java projects. Oca produces more expressive invariants: on average, 28% of its held invariants call a project-specific method, which Daikon's templates cannot express. Its invariants are more often valid, with a false-positive rate of 18% in a manual inspection, vs. 76% for Daikon, and more useful: as properties for property-based testing, they exposed 9 of 25 real bugs, compared with 4 for Daikon. Oca also costs less, using 566 minutes and 27 GB of disk, compared with 2,817 minutes and 827 GB for Daikon.
• Abstract（参考訳）: 動的不変検出器は、メソッドの前処理や後処理のような不変性を提案し、実行時に保持しないものを除外する。 従来の検出器はテンプレートの固定されたライブラリから不変性を提案し、表現性を制限している。 大規模言語モデル (LLM) はテンプレートから派生したものの代わりに不変(invariant)を提案できる。 正しいプロンプトと文脈の選択により、このアイデアは不変量の表現性を改善し、不変量を推論するコストを削減できることが分かった。 LLMが提案する不変量は、不変評価中に任意のコードを実行することができ、副作用や無限ループを引き起こす。 我々の新しい計器戦略はこれらの問題を緩和する。 それぞれの候補をラップし、スレッド毎に1つの不変量しか評価しないので、ネストした不変度評価は互いに無期限にトリガできない。 非ネステッドハングから回復するために、我々は各ランの屋台をモニターし、成長する時間予算の下で再試行する。 候補が事前に副作用のないことを証明できないため、フェールテスト中に評価された不変量に対するデルタデバッグを使用して、残りの部分を破棄することなく、副作用のある候補を分離、無効にしています。 私たちは、私たちの実装であるOcaを、実際のオープンソースのJavaプロジェクトで人気のあるテンプレートベースのダイコン不変検出器と比較しました。 Ocaはより表現力のある不変量を生成する。平均して、保持されている不変量の28%はプロジェクト固有のメソッドと呼ばれ、ダイコンのテンプレートは表現できない。 その不変性は、手動検査で18%の偽陽性率で、大根の76%に対して有効であり、プロパティベースのテストのプロパティとして、大根の4つと比較して、25の実際のバグを9つ暴露した。 Ocaは566分と27GBのディスクを使用し、大根は2,817分と827GBである。

関連論文リスト

• Jeva: System One Models from First Principles [58.432996881401415]
  Jevaは4つの重要な構造的要件に対処する、決定ネイティブなアーキテクチャです。 共有エンコーダは独立して要求と各オプションを表現し、コンパクトな決定スタックは要求状態のみを洗練する。 Jevとオープンソースモデルに対する評価全般において、Jevaは強力な型付き決定性能とほぼ完璧なnull検出を組み合わせる。
  論文  参考訳（メタデータ） (2026-10-13T17:31:09Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• Programming over Thinking: Efficient and Robust Multi-Constraint Planning [54.77940831026738]
  SCOPEは、クエリ固有の推論をジェネリックコード実行から切り離すフレームワークである。 SCOPEは、コストとレイテンシを下げながら最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-01-14T02:58:07Z)
• Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version) [4.309079367183251]
  モデル検査に外部不変量を注入する拡張型検証アルゴリズムを提案する。 インジェクション不変により安全性の証明に必要なクエリ数が削減され,実行時の効率が向上することがわかった。
  論文  参考訳（メタデータ） (2024-03-12T17:02:53Z)
• Diagnosing and Rectifying Fake OOD Invariance: A Restructured Causal Approach [51.012396632595554]
  不変表現学習(IRL)は、不変因果的特徴から環境から切り離されたラベルへの予測を促進する。 最近の理論的結果は、IRLによって回復されたいくつかの因果的特徴は、訓練環境ではドメイン不変のふりをするが、目に見えない領域では失敗する。 本研究では,RS-SCMに関する条件付き相互情報に基づく手法を開発し,その効果を巧みに補正する。
  論文  参考訳（メタデータ） (2023-12-15T12:58:05Z)
• Winning Prize Comes from Losing Tickets: Improve Invariant Learning by Exploring Variant Parameters for Out-of-Distribution Generalization [76.27711056914168]
  Out-of-Distribution (OOD) 一般化は、分散固有の特徴に適合することなく、様々な環境によく適応する堅牢なモデルを学ぶことを目的としている。 LTH(Lottery Ticket hypothesis)に基づく最近の研究は、学習目標を最小化し、タスクに重要なパラメータのいくつかを見つけることでこの問題に対処している。 Invariant Learning (EVIL) における変数探索手法を提案する。
  論文  参考訳（メタデータ） (2023-10-25T06:10:57Z)
• Ranking LLM-Generated Loop Invariants for Program Verification [14.7590099354867]
  大規模言語モデルは、0ショット設定でプログラムのクラスに対するループ不変量を合成することができる。 これは、不変性を確立するためのプログラム検証者への多数の呼び出しにつながる可能性がある。 我々は正しい帰納的不変量と誤った試みを区別できるランク付け器を設計した。
  論文  参考訳（メタデータ） (2023-10-13T18:13:52Z)

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

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