論文の概要: Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs
- arxiv url: http://arxiv.org/abs/2608.07947v1
- Date: Sat, 08 Aug 2026 06:22:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-11 19:16:36.579899
- Title: Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs
- Title（参考訳）: 分散並列AIプログラムの検証のためのニューロシンボリック確率的実行法
- Abstract要約: 我々は,Large Language Model (LLM) によるスケジュール予測と,シンボリック制約とカバレッジ誘導突然変異を併用したハイブリッドテストフレームワークである Directed Neuro-Symbolic Execution (DNSSE) を提案する。
我々は、分散AI実行を非決定論的遷移系としてモデル化し、線形時間論理における正当性を規定し、健全性、有界性、確率的完全性を証明する。
PyTorchとRayのスケーラブルな実装は、最強のベースラインよりも2.9%多くのバグを検出し、5つの現実的な分散AIベンチマークで平均ブランチカバレッジを68.6%から91.6%に引き上げている。
- 参考スコア（独自算出の注目度）: 0.5716454975957338
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Distributed parallel Artificial Intelligence (AI) programs expose reliability gaps that conventional testing cannot close: parallel executions are non-deterministic, and AI workloads bring high-dimensional inputs and non-linear operations that defeat fuzzing and symbolic execution in isolation. We present Directed Neuro-Symbolic Stochastic Execution (DNSSE), a hybrid testing framework that couples schedule prediction guided by a Large Language Model (LLM) with symbolic constraint solving and coverage-guided stochastic mutation. We model distributed AI executions as non-deterministic transition systems, specify correctness in linear temporal logic, and prove soundness, bounded completeness, and probabilistic completeness of the hybrid solver, together with an expected-cost analysis of LLM-guided schedule exploration. A scalable implementation on PyTorch and Ray detects 2.9% more concurrency bugs than the strongest baseline and raises average branch coverage from 68.6 % to 91.6 % across five realistic distributed AI benchmarks.
- Abstract（参考訳）: 並列実行は非決定論的であり、AIワークロードは高次元の入力と非線形操作をもたらし、ファジィやシンボル的な実行を分離して破壊する。
我々は,Large Language Model (LLM) が指導するスケジュール予測と,シンボル的制約解決と包括的確率的突然変異を併用したハイブリッドテストフレームワークである Directed Neuro-Symbolic Stochastic Execution (DNSSE) を提案する。
我々は、分散AI実行を非決定論的遷移系としてモデル化し、線形時間論理における正当性を規定し、LLM誘導スケジュール探索の予測コスト分析とともに、ハイブリッドソルバの健全性、有界完全性、確率的完全性を証明する。
PyTorchとRayのスケーラブルな実装は、最強のベースラインよりも2.9%の並行性バグを検出し、平均ブランチカバレッジを5つの現実的な分散AIベンチマークで68.6%から91.6%に向上させる。
関連論文リスト
- Synergistic Directed Execution and LLM-Driven Analysis for Zero-Day AI-Generated Malware Detection [0.12891210250935145]
自動マルウェア生成のためのLLMのウェポン化は、従来の検出パラダイムに現実的な脅威をもたらす。
本稿では,エスココール実行とエンフディープ学習に基づく脆弱性分類を組み合わせた,新しいハイブリッド分析フレームワークを提案する。
2,500 LLM合成サンプルからなるベンチマークでは、従来のマルウェアでは98.7%、AIによる脅威では97.5%の精度が達成されている。
論文 参考訳（メタデータ） (2026-03-10T00:25:41Z) - Para-B&B: Load-Balanced Deterministic Parallelization of Solving MIP [50.917107318582715]
MIP(Mixed-integer Programming)は、連続型と整数型の両方の決定変数を組み込むことで線形プログラミングを拡張する。
本稿では,高性能MIPソルバであるHiGHSに対して,決定論的並列分岐結合の完全なオープンソース実装を初めて提案する。
本手法では,ワーカスレッド間で完全なソルバ状態を複製することにより,厳密な決定性を保証する新しいデータ並列アーキテクチャを提案する。
論文 参考訳（メタデータ） (2026-02-10T14:17:53Z) - Efficient Thought Space Exploration through Strategic Intervention [54.35208611253168]
本稿では,この知見を2つの相乗的コンポーネントを通して操作するHint-Practice Reasoning(HPR)フレームワークを提案する。
フレームワークの中核となる革新は、動的に介入点を識別する分散不整合低減(DIR)である。
算術的および常識的推論ベンチマークによる実験は、HPRの最先端の効率-精度トレードオフを実証している。
論文 参考訳（メタデータ） (2025-11-13T07:26:01Z) - Scalable, Symbiotic, AI and Non-AI Agent Based Parallel Discrete Event Simulations [0.0]
本稿では,複数のAIエージェントと非AIエージェントを組み合わせた並列離散イベントシミュレーション(PDES)手法を提案する。
我々は、4つの異なるドメインから4つの問題を解き、その結果をAIモデルだけで比較することで、我々のアプローチを評価する。
その結果,バニラモデルの精度が23%未満であるため,アプローチ全体の精度は68%であった。
論文 参考訳（メタデータ） (2025-05-28T17:50:01Z) - Reviving Any-Subset Autoregressive Models with Principled Parallel Sampling and Speculative Decoding [55.2480439325792]
任意の順序言語モデルでは、正しい関節分布からトークンを並列にサンプリングする方法がオープンな問題である。
我々は,任意のサブセット自動回帰モデル (AS-ARM) という,異なるモデルのクラスが解を持っていることを発見した。
我々は,AS-ARMがベンチマークタスクを埋め込んだ200M未満のパラメータモデル間で最先端の性能を実現し,コード生成における50倍のモデルの性能とほぼ一致していることを示す。
論文 参考訳（メタデータ） (2025-04-29T06:33:13Z) - MindFlayer SGD: Efficient Parallel SGD in the Presence of Heterogeneous and Random Worker Compute Times [49.1574468325115]
最適勾配を計算できる複数の並列作業者の設定において、滑らかな非関数の期待を最小化する問題について検討する。
この文脈における課題は、任意に不均一で分散された計算時間の存在である。
本稿では,このギャップに対処する新しい並列SGD法であるMindFlayer SGDを紹介する。
論文 参考訳（メタデータ） (2024-10-05T21:11:32Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳（メタデータ） (2022-12-01T17:36:30Z) - Incremental Verification of Fixed-Point Implementations of Neural
Networks [0.19573380763700707]
インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
論文 参考訳（メタデータ） (2020-12-21T10:03:44Z) - General stochastic separation theorems with optimal bounds [68.8204255655161]
分離性の現象が明らかになり、機械学習で人工知能(AI)システムのエラーを修正し、AI不安定性を分析するために使用された。
エラーやエラーのクラスタは、残りのデータから分離することができる。
AIシステムを修正する能力は、それに対する攻撃の可能性も開き、高次元性は、同じ分離性によって引き起こされる脆弱性を誘発する。
論文 参考訳（メタデータ） (2020-10-11T13:12:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。