論文の概要: Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains

• arxiv url: http://arxiv.org/abs/2603.21149v1
• Date: Sun, 22 Mar 2026 10:02:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-24 19:11:39.261796
• Title: Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains
• Title（参考訳）: 創発的な形式検証:6つのドメインにわたるSMTベースの安全を独立して発見する自律型AIエコシステム
• Abstract要約: 本稿では,共通APIを通じて6つの出力クラスすべてにZ3ベースの検証を適用する統一フレームワークを提案する。 提案手法を5つの実装ドメインで181のテストケースで評価し,100%の分類精度,0の偽陽性,0の偽陰性で評価した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: An autonomous AI ecosystem (SUBSTRATE S3), generating product specifications without explicit instructions about formal methods, independently proposed the use of Z3 SMT solver across six distinct domains of AI safety: verification of LLM-generated code, tool API safety for AI agents, post-distillation reasoning correctness, CLI command validation, hardware assembly verification, and smart contract safety. These convergent discoveries, occurring across 8 products over 13 days with Jaccard similarity below 15% between variants, suggest that formal verification is not merely a useful technique for AI safety but an emergent property of any sufficiently complex system reasoning about its own safety. We propose a unified framework (substrate-guard) that applies Z3-based verification across all six output classes through a common API, and evaluate it on 181 test cases across five implemented domains, achieving 100% classification accuracy with zero false positives and zero false negatives. Our framework detected real bugs that empirical testing would miss, including an INT_MIN overflow in branchless RISC-V assembly and mathematically proved that unconstrained string parameters in tool APIs are formally unverifiable.
• Abstract（参考訳）: フォーマルなメソッドに関する明確な指示なしに製品仕様を生成する自律型AIエコシステム(SubSTRATE S3)は、独立に、LLM生成コードの検証、AIエージェントのためのツールAPI安全性、蒸留後推論の正しさ、CLIコマンド検証、ハードウェアアセンブリ検証、スマートコントラクト安全性の6つの異なる領域にわたるZ3 SMTソルバの使用を提案した。 これらの収束した発見は、Jaccardと変種間の15%以下で13日間にわたって発生し、形式的検証はAIの安全性に有用なテクニックであるだけでなく、自身の安全性を推論する十分な複雑なシステムの創発的な性質であることを示唆している。 本研究では,共通APIを通じてZ3ベースの検証を6つの出力クラスすべてに適用する統合フレームワーク(サブストラクタガード)を提案し,これを5つの実装ドメインにわたる181のテストケースで評価し,100%の分類精度をゼロの偽陽性とゼロの偽陰性で達成する。 我々のフレームワークは、ブランチレスRISC-VアセンブリにおけるINT_MINオーバーフローなど、経験的テストが見逃すような本当のバグを検出し、数学的に、ツールAPIの制約なし文字列パラメータが公式には検証できないことを証明した。

関連論文リスト

• Non-Degenerate Risk Certification for Automated Security Decisions: A Decision-Contract Theory with ATT\&CK-Aligned Triage as a Worked Instance [1.4915002678801434]
  自動決定に縛られる無条件のリスクは、何も自動化せずに満足することができる。 リスク証明書は、決定契約上で定義され、システムが行動する入力に加えて、出力が正しいと判断する意味関係が定義される。 誤りを示すエラー保存法は, 有害な自動化, ヒューマン・デフェラル, セマンティック・マスキングによってのみ再割り当てされる。
  論文  参考訳（メタデータ） (2026-08-12T16:59:19Z)
• VATS: Exploiting Implicit Authority in Error-Path Injection via Systematic Mutation [0.3222802562733787]
  VATS (Vulnerability Analysis of Tool Streams) は、7つの構造的および言語的次元にわたる逆ペイロードを進化させる突然変異駆動型フレームワークである。 Gemini 3.1 Pro, GPT-5.5, GLM-5.1, Qwen3-Coderの4つのフロンティアモデルに対して, エラーパスインジェクションが標準間接インジェクションの成功率を3倍にすることを示す。
  論文  参考訳（メタデータ） (2026-06-06T06:07:52Z)
• Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
  本稿では,インダクティブ・デダクティブ・シンセシス(IDS)について述べる。 IDSは約6.8時間で7/7を達成し、1仕様あたり106ドル、専門家の努力の約200倍、SOTAエージェントの約17%を達成している。 IDSはパフォーマンスフィードバックを同じループに組み込んでおり、検証されたシステムよりも最大3倍高速な実装を実現している。
  論文  参考訳（メタデータ） (2026-05-22T00:05:36Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。 DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。 クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
  論文  参考訳（メタデータ） (2026-04-20T22:02:57Z)
• Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code [0.0]
  Broken by Defaultは、500のセキュリティクリティカルなプロンプトにまたがる7つの広くデプロイされたLLMによって生成される3500のコードアーティファクトの正式な検証研究である。 すべてのモデル全体で、55.8%のアーティファクトは少なくとも1つのCOBALT識別された脆弱性を含んでいる。 GPT-4oは62.4%(グレードF)、Gemini 2.5 Flashは48.4%(グレードD)である。
  論文  参考訳（メタデータ） (2026-04-07T00:55:42Z)
• You Told Me to Do It: Measuring Instructional Text-induced Private Data Leakage in LLM Agents [9.719776777345364]
  外部文書を自律的に処理する高特権のLLMエージェントは、タスクを自動化するためにますます信頼されている。 これらのエージェントには、最小限のセキュリティ監視で端末アクセス、制御、アウトバウンドネットワーク接続が与えられる。 emphTrusted Executor Dilemmaと呼ばれるこの信頼モデルの基本的脆弱性を測定する。 この脆弱性は、実装バグではなく、命令追従設計パラダイムの構造的な結果である。
  論文  参考訳（メタデータ） (2026-03-12T12:35:46Z)
• Synthesizing the Kill Chain: A Zero-Shot Framework for Target Verification and Tactical Reasoning on the Edge [12.201060368447251]
  本稿では,コンパクトな視覚言語モデル(VLM)を用いた軽量物体検出を実現する階層型ゼロショットフレームワークを提案する。 我々は,このパイプラインを,偽陽性フィルタリング(100%精度),損傷評価(97.5%),きめ細かい車両分類(55-90%)の3つのタスクで,バトルフィールド6の55個の高忠実合成ビデオ上で評価した。
  論文  参考訳（メタデータ） (2026-02-10T23:00:19Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• ReasAlign: Reasoning Enhanced Safety Alignment against Prompt Injection Attack [52.17935054046577]
  本稿では、間接的インジェクション攻撃に対する安全性アライメントを改善するためのモデルレベルのソリューションであるReasAlignを提案する。 ReasAlignには、ユーザクエリの分析、競合する命令の検出、ユーザの意図したタスクの継続性を維持するための構造化された推論ステップが組み込まれている。
  論文  参考訳（メタデータ） (2026-01-15T08:23:38Z)
• What Matters For Safety Alignment? [38.86339753409445]
  本稿では,AIシステムの安全アライメント能力に関する総合的研究について述べる。 本研究では,6つの重要な内在モデル特性と3つの外部攻撃手法の影響を系統的に検討し,比較した。 LRMs GPT-OSS-20B, Qwen3-Next-80B-A3B-Thinking, GPT-OSS-120Bを最も安全な3つのモデルとして同定した。
  論文  参考訳（メタデータ） (2026-01-07T12:31:52Z)
• OmniSafeBench-MM: A Unified Benchmark and Toolbox for Multimodal Jailbreak Attack-Defense Evaluation [94.61617176929384]
  OmniSafeBench-MMはマルチモーダル・ジェイルブレイク攻撃防御評価のための総合ツールボックスである。 13の代表的な攻撃方法と15の防衛戦略、9つの主要なリスクドメインと50のきめ細かいカテゴリにまたがる多様なデータセットを統合している。 データ、方法論、評価をオープンソースで再現可能なプラットフォームに統合することで、OmniSafeBench-MMは将来の研究のための標準化された基盤を提供する。
  論文  参考訳（メタデータ） (2025-12-06T22:56:29Z)
• Can AI Keep a Secret? Contextual Integrity Verification: A Provable Security Architecture for LLMs [0.0]
  我々は、暗号的に署名されたラベルを全てのトークンにアタッチする、既定のセキュリティアーキテクチャであるContextual Integrity Verification (CIV)を提示する。 CIVは、凍結したモデルに対して、前兆かつトーケン毎の非干渉保証を提供する。 Llama-3-8BとMistral-7Bのドロップイン保護を実証した。
  論文  参考訳（メタデータ） (2025-08-12T18:47:30Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Benchは、安全でないユーザ要求を認識し拒否する大規模言語モデル(LLM)能力を評価するためのベンチマークである。 まず、既存の手法では、安全でないトピックの粗い分類を使い、いくつかのきめ細かいトピックを過剰に表現している。 第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。
  論文  参考訳（メタデータ） (2024-06-20T17:56:07Z)
• ASSERT: Automated Safety Scenario Red Teaming for Evaluating the Robustness of Large Language Models [65.79770974145983]
  ASSERT、Automated Safety Scenario Red Teamingは、セマンティックなアグリゲーション、ターゲットブートストラップ、敵の知識注入という3つの方法で構成されている。 このプロンプトを4つの安全領域に分割し、ドメインがモデルの性能にどのように影響するかを詳細に分析する。 統計的に有意な性能差は, 意味的関連シナリオにおける絶対分類精度が最大11%, ゼロショット逆数設定では最大19%の絶対誤差率であることがわかった。
  論文  参考訳（メタデータ） (2023-10-14T17:10:28Z)

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

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