論文の概要: Agentic Model Checking

• arxiv url: http://arxiv.org/abs/2605.21434v1
• Date: Wed, 20 May 2026 17:25:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-21 19:19:56.811025
• Title: Agentic Model Checking
• Title（参考訳）: エージェントモデルチェック
• Abstract要約: 本稿では,LLMエージェントと境界モデルチェックバックエンドを結合するパラダイムを提案する。 我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で評価する。
• 参考スコア（独自算出の注目度）: 12.832868209928039
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verifying LLM-generated systems code is hard: bugs are prevalent, formal specifications are missing, and safety contracts are encoded implicitly at call sites rather than enforced at function boundaries. We propose agentic model checking, a paradigm that couples LLM agents with a bounded model checking backend under the principle agents propose, solvers verify: agents handle tasks requiring semantic judgment (spec inference, check selection, counterexample classification, refinement proposal) while BMC discharges every soundness-relevant decision. The paradigm rests on three commitments. Specifications are inferred top-down from caller context in a restricted DSL that translates deterministically into the backend's assume/assert primitives, with optional functional-correctness clauses lifting verification from panic-freeness to behavioural faithfulness. Verification is compositional: each function is checked in isolation against its spec with callees replaced by postcondition-constrained stubs, so per-query cost scales with a single function's state space and refinements propagate automatically to callers. Counterexamples are not bug reports: they pass through a validation pipeline (reachability, callee feasibility, dynamic replay, realism audit) that distinguishes active in-tree crashes from latent public-API failures, while modelling artifacts drive a refinement loop rather than being suppressed. We instantiate the approach in BMC-Agent and evaluate it on LLM-generated kernel and compiler code in C and Rust alongside mature OSS-Fuzz-hardened libraries, confirming real defects, producing bounded clean verifications on heavily-fuzzed surfaces, and establishing functional equivalence on selected algorithmic functions.
• Abstract（参考訳）: バグが頻繁に発生し、正式な仕様が失われ、安全契約が関数境界で強制されるのではなく、コールサイトで暗黙的にエンコードされる。 エージェントは意味的判断を必要とするタスク(特定の推論、チェック選択、逆例分類、精査提案)を処理し、BMCはすべての音質関連決定を出力する。 パラダイムは3つのコミットメントに依存します。 仕様は制限付きDSLで呼び出しコンテキストからトップダウンで推論され、決定論的にバックエンドのsum/assertプリミティブに変換される。 検証は構成的であり、各関数はその仕様に対して独立してチェックされ、呼び出し元は条件制約後のスタブに置き換えられる。 検証パイプライン(到達可能性、呼び出し者実現性、動的リプレイ、リアリズム監査)を通過して、ツリー内のアクティブなクラッシュと、潜在的にパブリックAPIの障害を区別する一方で、アーティファクトのモデル化は、抑制されるのではなく、リファインメントループを駆動する。 我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で、成熟したOSS-Fuzz処理ライブラリとともに評価し、実際の欠陥を確認し、密閉面上で境界付きクリーンな検証を生成し、選択されたアルゴリズム関数に関数同値性を確立する。

関連論文リスト

• PluginEval: A Diagnostic Benchmark for Fine-Grained Error Attribution in Function Calling [11.1017602726296]
  大規模言語モデルは、ますます自律的なエージェントとして機能している。 現在のベンチマークには3つの制限がある。 Evalは、2段階のフレームワークで構築されたベンチマークである。
  論文  参考訳（メタデータ） (2026-08-09T13:25:54Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMは、オフチェーン実行の正しさを保証するゼロ知識を生成する。 微妙な実装上のバグは、意味的に欠陥のある状態を証明する有効な証明につながる可能性がある。 SMTソルバによる形式検証は、これを防止できるが、仕様によってボトルネックとなる。 Rustから実行可能なPython/Z3検証モデルを合成するフレームワークであるVeri Synthを提案する。
  論文  参考訳（メタデータ） (2026-07-22T06:20:36Z)
• PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
  我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。 セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。 SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。 ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
  論文  参考訳（メタデータ） (2026-07-18T04:46:53Z)
• Kani: A Model Checker for Rust [3.019677299390329]
  KaniはRustのオープンソースモデルチェッカーである。 バグフィニング以外のバウンドモデルチェックをプッシュして、正確性を保証する。 KaniはプロダクションCIで大規模に運用されており、コード変更毎に16,000以上のハーネスが検証されている。
  論文  参考訳（メタデータ） (2026-07-01T22:05:33Z)
• What to Test Next: Interpretable Coverage Gap Discovery in Driving VLMs [52.50210189669399]
  視覚言語モデル(VLM)を駆動するには,操作設計領域(ODD)が定義する様々な条件のシーンを正確に理解する必要がある SliceScorerは、欠落したスライス推薦のための決定論的スコアリングルールである。 SliceNavは, 従来のスライス発見法よりも, 高リスクカバレッジギャップを効果的に表面化することを示す。
  論文  参考訳（メタデータ） (2026-06-01T03:18:01Z)
• VerifyMAS: Hypothesis Verification for Failure Attribution in LLM Multi-Agent Systems [79.51005192758262]
  大規模言語モデル駆動型マルチエージェントシステムは複雑なタスクで優れている。 しかし、信頼性の低いエージェントは、システムレベルの信頼性にとって重要なボトルネックである。 本稿では,エージェント故障の帰属に関する仮説検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-05-17T14:09:35Z)
• Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
  LLM駆動のランタイムによってどのようにスキルが消費されるかに忠実なスキル行動に関する正確なセマンティクスを提供します。 本稿では,定式化や定式化によるスキル向上を両立させる構成可能な3つの手法を提案する。 これら3つのメソッドに加えて、バンドルプロデューサと再チェッカーは、オープンソースエンクロードフレームワークのゼロ依存JavaScriptモジュールとして出荷される。
  論文  参考訳（メタデータ） (2026-05-09T19:27:38Z)
• The Context Gathering Decision Process: A POMDP Framework for Agentic Search [38.92972416925679]
  大規模言語モデル(LLM)エージェントは複雑な環境にデプロイされる。 明示的なインフラストラクチャがなければ、エージェントの動作メモリは、検索状態の損失のある表現に分解される可能性がある。 我々はこの課題をコンテキスト収集決定プロセス(CGDP)として定式化する。 反復LDM剤に対する2つのプラグ・アンド・プレイ介入法を導出する。
  論文  参考訳（メタデータ） (2026-05-07T23:45:07Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols [1.5229705287183657]
  SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。 RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。 Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
  論文  参考訳（メタデータ） (2026-04-29T09:57:07Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• A Trace-Based Assurance Framework for Agentic AI Orchestration: Contracts, Testing, and Governance [0.22940141855172028]
  本稿では,Large Language Models (LLM) を用いたエージェントAIシステムの保証フレームワークを提案する。 実行は、明示的なステップとトレースコントラクトを備えたメッセージ・アクション・トレース(MAT)として実装される。 このフレームワークは、有界摂動に対する予算付き反例探索として定式化されたストレステストを含む。
  論文  参考訳（メタデータ） (2026-03-18T10:23:48Z)
• RULERS: Locked Rubrics and Evidence-Anchored Scoring for Robust LLM Evaluation [15.787947727055611]
  本稿では,自然言語ルーブを実行可能な仕様に変換するコンパイラ・エグゼクタフレームワークであるRULERSを紹介する。 RULERSは、基準をバージョニングされた不変バンドルにコンパイルし、決定論的証拠検証による構造化復号を強制し、軽量なワッサーシュタインベースのポストホックキャリブレーションを適用する。
  論文  参考訳（メタデータ） (2026-01-13T15:31:42Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。 数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。 我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
  論文  参考訳（メタデータ） (2025-08-05T17:55:24Z)
• Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
  Retrieval-augmented Generation (RAG) は知識基底型大規模言語モデル(LLM)を実現するためのパラダイムとして広く採用されている。 RAGパイプラインは、モデル推論が得られた証拠と整合性を維持するのに失敗することが多く、事実上の矛盾や否定的な結論につながる。 批判駆動アライメント(CDA)に基づく新しい反復的枠組みであるAlignRAGを提案する。 AlignRAG-autoは、動的に洗練を終了し、批判的な反復回数を事前に指定する必要がなくなる自律的な変種である。
  論文  参考訳（メタデータ） (2025-04-21T04:56:47Z)

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

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