論文の概要: COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery

• arxiv url: http://arxiv.org/abs/2604.12172v1
• Date: Tue, 14 Apr 2026 00:56:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-15 19:11:32.179792
• Title: COBALT-TLA: A Neuro-Symbolic Verification Loop for Cross-Chain Bridge Vulnerability Discovery
• Title（参考訳）: COBALT-TLA:クロスチェーンブリッジ脆弱性発見のためのニューロシンボリック検証ループ
• Authors: Dominik Blain,
• Abstract要約: COBALT-TLAは、TLC(TLA+モデルチェッカー)とLCMをペアリングする神経象徴的検証ループである。 我々は,Nomad $190Mエクスプロイトの忠実なモデルを含む,3つのクロスチェーンブリッジターゲットに対してシステムを評価する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present COBALT-TLA, a neuro-symbolic verification loop that pairs an LLM with TLC, the TLA+ model checker, in an automated REPL. The LLM generates bounded TLA+ specifications; TLC acts as a semantic oracle; structured error traces are parsed and injected back into the model's context to drive convergence. We evaluate the system against three cross-chain bridge targets, including a faithful model of the Nomad $190M exploit. COBALT-TLA reaches a verified BUG_FOUND state in at most 2 iterations on all targets, with TLC execution consistently below 0.30 seconds. Notably, the system autonomously discovers an unprompted vulnerability class -- the Optimistic Relay Attack -- not present in the human-written baseline specification. We argue that deterministic prover feedback is sufficient to neutralize LLM hallucination in formal methods, transforming zero-shot code generation into a convergent proof-finding strategy.
• Abstract（参考訳）: 本稿では,LLMとTLC(TLA+モデルチェッカー)をペアリングする神経シンボル的検証ループであるCOBALT-TLAについて,自動REPLで紹介する。 LLM は有界な TLA+ 仕様を生成し、TLC は意味的なオラクルとして機能し、構造化されたエラートレースを解析してモデルのコンテキストに注入して収束を駆動する。 我々は,Nomad $190Mエクスプロイトの忠実なモデルを含む,3つのクロスチェーンブリッジターゲットに対してシステムを評価する。 COBALT-TLAは、全ての目標に対して少なくとも2回はBUG_FOUND状態に到達し、TLCの実行は0.30秒以下である。 注目すべきなのは,人間が記述したベースライン仕様には存在しない,予期せぬ脆弱性クラス – Optimistic Relay Attack -- が自動で検出されることだ。 決定論的証明フィードバックは、形式的手法でLLM幻覚を中和するのに十分であり、ゼロショットコード生成を収束的証明フィニング戦略に変換する。

関連論文リスト

• Benchmarking Zero-Shot Reasoning Approaches for Error Detection in Solidity Smart Contracts [0.0]
  本稿では,400契約のバランスデータセットを用いて,Solidityスマートコントラクト分析の最先端LCMについて検討する。 モデルは、ゼロショット、ゼロショット・オブ・ソート(CoT)、ゼロショット・オブ・ソート(ToT)を含むゼロショット・プロンプト戦略を用いて評価される。
  論文  参考訳（メタデータ） (2026-02-17T18:08:56Z)
• Trajectory Guard -- A Lightweight, Sequence-Aware Model for Real-Time Anomaly Detection in Agentic AI [0.0]
  トラジェクトリガードはシームズ・リカレント・オートエンコーダであり、コントラスト学習によるタスク・トラジェクトリアライメントと、再構成によるシーケンシャル・アライメントを共同で学習するハイブリッド・ロス機能を備えている。 32ミリ秒のレイテンシで、当社のアプローチは LLM Judge のベースラインよりも17-27倍高速で動作し、実運用環境におけるリアルタイムの安全性検証を可能にします。
  論文  参考訳（メタデータ） (2026-01-02T00:27:11Z)
• On GRPO Collapse in Search-R1: The Lazy Likelihood-Displacement Death Spiral [59.14787085809595]
  この障害を引き起こす中核的なメカニズムとしてLazy Likelihood Displacement(LLD)を同定する。 LDDは早期に出現し、自己強化性LDDデススパイラル(LDD Death Spiral)を引き起こす。 本稿では,GRPO のための軽量な確率保存正則化 LLDS を提案する。
  論文  参考訳（メタデータ） (2025-12-03T19:41:15Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  大規模言語モデル(LLM)は、有害な出力を誘導するために安全ガードレールをバイパスするジェイルブレイク攻撃に弱いままである。 CKA-Agent(Correlated Knowledge Attack Agent)は、ターゲットモデルの知識基盤の適応的木構造探索としてジェイルブレイクを再構成する動的フレームワークである。
  論文  参考訳（メタデータ） (2025-12-01T07:05:23Z)
• Evaluating Embedding Generalization: How LLMs, LoRA, and SLERP Shape Representational Geometry [0.0]
  本研究では,SLERPモデルがタスク固有適応によって導入された超特殊化を緩和する程度について検討する。 モデルの4つのファミリを比較する: ゼロから訓練された非LLMエンコーダ、パラメータ係数法(LoRA)に適応したLLMベースのエンコーダ、LoRAを用いたLLMベースのエンコーダ、ベースウェイトにマージしたモデルスープ、および同じLoRA適応LLMはチェックポイントやステージをまたいだSLERPを用いてマージされる。
  論文  参考訳（メタデータ） (2025-11-16T17:28:06Z)
• When LLMs Copy to Think: Uncovering Copy-Guided Attacks in Reasoning LLMs [30.532439965854767]
  大規模言語モデル(LLM)は、脆弱性検出やコード理解といったタスクを可能にする自動コード解析に不可欠なものになっている。 本稿では,CGA(Copy-Guided Attacks)と呼ばれる,新たなプロンプトベースの攻撃のクラスを特定し,検討する。 CGAは、コード解析タスクにおいて、無限ループ、早期終了、偽の拒絶、意味的歪みを確実に誘導することを示す。
  論文  参考訳（メタデータ） (2025-07-22T17:21:36Z)
• Teaching Your Models to Understand Code via Focal Preference Alignment [70.71693365502212]
  既存の手法では、テストケースの成功率に基づいてn個の候補解が評価される。 このアプローチは、特定のエラーを特定するのではなく、失敗するコードブロック全体を整列するので、意味のあるエラーと訂正の関係を捉えるのに必要な粒度が欠けている。 我々は、人間の反復デバッグを模倣してコードLLMを洗練させる新しい優先順位調整フレームワークであるTarget-DPOを提案する。
  論文  参考訳（メタデータ） (2025-03-04T16:56:34Z)
• Attribute Controlled Fine-tuning for Large Language Models: A Case Study on Detoxification [76.14641982122696]
  本稿では,属性制御付き大規模言語モデル(LLM)の制約学習スキーマを提案する。 提案手法は, ベンチマーク上での競合性能と毒性検出タスクを達成しながら, 不適切な応答を少ないLCMに導出することを示す。
  論文  参考訳（メタデータ） (2024-10-07T23:38:58Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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