論文の概要: Soundness Checking of Taint Flow Models

• arxiv url: http://arxiv.org/abs/2609.28750v1
• Date: Wed, 23 Sep 2026 19:47:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-25 21:10:09.539159
• Title: Soundness Checking of Taint Flow Models
• Title（参考訳）: 音質流れモデルの音質検査
• Abstract要約: 命令型プログラミング言語の既存の静的な流れ解析は、大規模アプリケーションに拡張可能である。 手動で正確にメソッドのテナントフローをモデル化するのは面倒で、潜在的に不正確です。 提案手法は,(1)メソッドの正確なテナントフローモデルを生成するLLMエージェント,(2)モデルの音質をチェックするシンボリックアルゴリズムである。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Existing state-of-the-art static taint flow analyses for imperative programming languages can scale to large applications by using precise user-provided taint flow models of library methods. However, manually and precisely modeling a method's taint flows is tedious and potentially unsound. Furthermore, automatically modeling the method via an inter- procedural taint analysis can be inefficient. To solve this problem, we propose a guess-and-check approach: (1) an LLM agent that generates a precise taint flow model of a method and (2) a symbolic algorithm to check the soundness of the model. The algorithm deduces which taint flows must not occur in the method for the LLM's taint flow model to be sound, and uses lightweight static analyses (e.g., type system and pointer analysis) to prove these must-not-flows. When these analyses are insufficient, the algorithm deduces maximally-general callee models and recursively verifies their soundness, avoiding a full inter-procedural taint analysis in most cases. Since a more precise model requires fewer must-not-flows to be verified, the precision of the LLM's model directly determines the efficiency of our approach. We evaluate our approach on 97 LLM-generated taint flow models for methods in 6 large Go codebases and prove the models sound for 93% of the methods they cover. The proven-sound LLM-generated models are also precise, resulting in no new false-positives when proving taint flow properties.
• Abstract（参考訳）: 既存の命令型プログラミング言語の静的なテントフロー解析は,ライブラリ手法の正確なユーザ提供によるテントフローモデルを用いて,大規模アプリケーションに拡張可能である。 しかし、メソッドのテナントフローを手動で正確にモデル化するのは面倒で、潜在的に不正確である。 さらに、手続き間テイント解析による手法の自動モデリングは非効率である。 この問題を解決するために,(1)メソッドの正確な張力フローモデルを生成するLCMエージェント,(2)モデルの音質をチェックするシンボリックアルゴリズムを提案する。 このアルゴリズムは、LLMのテイントフローモデルが音になる方法において、どのテイントフローが発生してはいけないかを推定し、軽量な静的解析(例えば、型システムやポインタ解析)を用いて、これらの必須でないフローを証明する。 これらの分析が不十分な場合、アルゴリズムは最大一般の呼び出し者モデルを導出し、ほとんどの場合において、プロシーダ間テナント解析を完全に回避して、その音質を再帰的に検証する。 より正確なモデルでは、検証する必要のないフローが少なくなるため、LLMモデルの精度は我々のアプローチの効率を直接決定する。 大規模Goコードベース6つのメソッドに対する97 LLM生成のテントフローモデルに対するアプローチを評価し,その93%のメソッドに対して,モデルが健全であることを示す。 実証されたLLM生成モデルも正確であり、テントフロー特性を証明する際に新しい偽陽性は生じない。

関連論文リスト

• Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
  本稿では、構造と解の両方の観点から、デュアルサイド検証(Opt-Verifier)を用いた新しいフレームワークを提案する。 一般的なベンチマーク実験により、我々の手法は精度が20%以上向上していることが示された。
  論文  参考訳（メタデータ） (2026-05-28T08:09:52Z)
• Differentiable Calibration of Inexact Stochastic Simulation Models via Kernel Score Minimization [11.955062839855334]
  そこで本研究では,勾配降下によるカーネルスコア最小化による出力レベルデータを用いて,シミュレーションモデルの異なる入力パラメータを学習する。 モデル不正確性を考慮した新しい正規化結果を用いて,学習した入力パラメータの不確かさを定量化する。
  論文  参考訳（メタデータ） (2024-11-08T04:13:52Z)
• Local Flow Matching Generative Models [19.859984725284896]
  フローマッチング(英: Flow Matching, FM)は、2つの分布を補間する連続的かつ非可逆的な流れを学習するためのシミュレーション不要な手法である。 FMサブモデルのシーケンスを連続的に学習するLFM(Local Flow Matching)と呼ばれるステップワイズFMモデルを提案する。 FMと比較して, LFMの訓練効率と競争的生成性能の改善を実証的に実証した。
  論文  参考訳（メタデータ） (2024-10-03T14:53:10Z)
• DALD: Improving Logits-based Detector without Logits from Black-box LLMs [56.234109491884126]
  大規模言語モデル(LLM)はテキスト生成に革命をもたらし、人間の文章を忠実に模倣する出力を生成する。 我々は、ブラックボックステキスト検出における最先端性能を再定義する革新的なフレームワークであるDLD(Dis Distribution-Aligned LLMs Detection)を提案する。 DALDは、サロゲートモデルの分布を未知の目標LLMの分布と整合させ、高速モデルの反復に対する検出能力とレジリエンスを向上するように設計されている。
  論文  参考訳（メタデータ） (2024-06-07T19:38:05Z)
• Towards Stable Machine Learning Model Retraining via Slowly Varying Sequences [6.067007470552307]
  そこで本研究では,リトレーニングを繰り返して安定なモデル列を見つけるためのモデルに依存しないフレームワークを提案する。 最適モデルの復元が保証される混合整数最適化の定式化を開発する。 平均的に、予測力の2%の低下は、安定性の30%の改善につながることが判明した。
  論文  参考訳（メタデータ） (2024-03-28T22:45:38Z)
• Language Rectified Flow: Advancing Diffusion Language Generation with Probabilistic Flows [53.31856123113228]
  本稿では,言語認識フロー (ours) を提案する。 本手法は, 標準確率流モデルの再構成に基づく。 実験およびアブレーション実験により,本手法は多くのNLPタスクに対して汎用的,効果的,有益であることが示されている。
  論文  参考訳（メタデータ） (2024-03-25T17:58:22Z)
• Discrete Denoising Flows [87.44537620217673]
  分類的確率変数に対する離散的フローベースモデル(DDF)を提案する。 他の離散フローベースモデルとは対照的に、我々のモデルは勾配バイアスを導入することなく局所的に訓練することができる。 そこで本研究では, DDFs が離散フローより優れていることを示し, 対数類似度で測定した2値MNIST と Cityscapes のセグメンテーションマップをモデル化した。
  論文  参考訳（メタデータ） (2021-07-24T14:47:22Z)
• Active and sparse methods in smoothed model checking [2.28438857884398]
  スパース変分法とアクティブラーニングに基づくモデルチェックの平滑化の拡張について検討する。 スパース変分ガウス過程推論アルゴリズムのオンライン拡張は、スムーズなモデル検査のための能動的学習手法を実装するためのスケーラブルな方法を提供する。
  論文  参考訳（メタデータ） (2021-04-20T13:03:25Z)
• Distilling Interpretable Models into Human-Readable Code [71.11328360614479]
  人間可読性は機械学習モデル解釈可能性にとって重要で望ましい標準である。 従来の方法を用いて解釈可能なモデルを訓練し,それを簡潔で可読なコードに抽出する。 本稿では,幅広いユースケースで効率的に,確実に高品質な結果を生成する分別線形曲線フィッティングアルゴリズムについて述べる。
  論文  参考訳（メタデータ） (2021-01-21T01:46:36Z)
• Macroscopic Traffic Flow Modeling with Physics Regularized Gaussian Process: A New Insight into Machine Learning Applications [14.164058812512371]
  本研究では,古典的トラフィックフローモデルを機械学習アーキテクチャにエンコードする,物理正規化機械学習(PRML)という新しいモデリングフレームワークを提案する。 提案手法の有効性を実証するため,ユタ州I-15高速道路から収集した実世界のデータセットについて実験的検討を行った。
  論文  参考訳（メタデータ） (2020-02-06T17:22:20Z)

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

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