論文の概要: Can Code Specify a System Precisely Enough to Formally Verify It?

• arxiv url: http://arxiv.org/abs/2607.05076v1
• Date: Mon, 06 Jul 2026 13:39:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-07 22:26:30.164684
• Title: Can Code Specify a System Precisely Enough to Formally Verify It?
• Title（参考訳）: コードは形式的に検証するのに十分なシステムを正確に特定できるのか?
• Abstract要約: 本報告では,業務用レストラン・ポイント・オブ・セールシステムの支払ワークフローを実運用ソフトウェアで評価する。 コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。 生産用サンドボックスの1つのプローブは、全リカバリはしごを到達不能にする応答形状のばらつきを露呈した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is seldom applied to production software, because writing and maintaining a model has historically cost more than it returns. A companion study [1] extended SysMoBench [4] with a lower-cost alternative: specifications are graded against traces captured from the running system. It found that when large language models write the specifications, reliability is governed by the structure of the specification contract, not the language. This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system, which must keep the register, payment terminal, and payment processor in agreement. We report three results. First, the core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model. The audit found seven failure-handling gaps, nearly all with a common root cause; three were reproduced as real executions, and a patch closing them was re-checked with all failure gates enabled, after which a follow-up patch closed a defect the re-check itself exposed. Systematic extensions of the failure model (crash-restart, stale reads, two attempts) each found the windows they were designed to probe. Second, a single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable against the live API. The emulator-based audit could not detect it, because code and emulator share the same misreading: a correlated-oracle failure. Third, the companion study's central finding replicates across seven models from two vendors: contract structure, not language, governs what LLMs specify reliably. The replication concerns the ordering of contracts and the failure taxonomy, not the absolute level: only the strongest models reached the corpus ceiling, and the harder task restores discriminating power the benchmark had lost.
• Abstract（参考訳）: 形式的検証が本番ソフトウェアに適用されることは滅多にない。 SysMoBench [4] を低コストで拡張したコンパニオンスタディ[1] 仕様は、実行中のシステムから取得したトレースに対してグレードされる。 大規模な言語モデルが仕様を書くとき、信頼性は言語ではなく仕様契約の構造によって管理されることがわかった。 本報告では,店頭販売システムにおいて,レジ,支払い端末,支払処理装置の整合性を維持するための支払ワークフローを運用ソフトウェア上で評価する。 3つの結果が報告される。 第一に、コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。 3つは実際の実行として再現され、閉じたパッチはすべての障害ゲートを有効にして再チェックされ、その後、フォローアップパッチが欠陥をクローズし、再チェック自体が露出した。 障害モデルの体系的な拡張(クラッシュ・リスタート、スタイル・リード、2回の試み)はそれぞれ、調査用に設計されたウィンドウを見つけました。 第二に、製品支払いサンドボックスの単一のプローブがレスポンスシェイプのばらつきを露呈し、リカバリのはしご全体がライブAPIに対して到達不能になった。 エミュレータベースの監査では、コードとエミュレータは同じ誤読を共有しているため、検出できなかった。 第3に、コンパニオン研究の中心的な発見は、2つのベンダーから7つのモデルにまたがる複製である。 この複製は、絶対レベルではなく、契約の順序と失敗の分類に関するもので、最強のモデルだけがコーパスの天井に到達し、より難しいタスクは、ベンチマークが失ったパワーを識別する。

関連論文リスト

• Rebuild Dossier: Mechanically-Enforced Specs for Agentic App Rebuilds, and What Model-Tier Failures Reveal [0.0]
  restruct-dossierは、コードを記述する前にアプリケーションの実際のインターフェースをロックするオープンソースツールである。 自動チェックによるワンテスト・アズ・ア・タイムのビルドを強制する。
  論文  参考訳（メタデータ） (2026-08-22T01:26:56Z)
• From Subjective Judgments to Auditable Standards:Protocol-Guided AI Auditing of Website Redundancy [2.2917707112773593]
  ウェブサイトの冗長性は、単一の固定された意味を持っていない。 我々は,繰り返し負荷,正規利用税,障害領域回復予備費を別々に測定するCORAを導入する。
  論文  参考訳（メタデータ） (2026-08-21T07:17:35Z)
• The Working Set of a Coding Agent: Coherence Debt in Repository-Scale Tasks [14.070053515623883]
  リポジトリスケールのコーディングには、テスト、インポート、設定、マイグレーションルールを境界付けられたコンテキストウィンドウ内で一貫性を保つためのエージェントが必要である。 7つのモデルと5つのハーネスに障害を注入します。 リネームが実際のライブラリについて記憶したモデルを破ると、7つすべてが同じ場所で失敗し、同じテストがパスして失われる。
  論文  参考訳（メタデータ） (2026-08-17T14:30:41Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMASTは、実行トレースをコンパクトでエビデンスに基づく障害分類に変換する。 コードには手書きのコードはなく、人間による注釈もない。 エージェント・システム・サーチでは、失敗候補の分類コード診断が自由形式より優れている。
  論文  参考訳（メタデータ） (2026-07-17T17:41:16Z)
• From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
  製品化は、ソースバウンダリ、エンティティルーティング、回答コントラクト、再現可能なトレースの要件を追加します。 本稿では,このパターンをトレース可能な監査可能なLLMエージェントアーキテクチャに再構成するハーネスエンジニアリング手法を提案する。 韓国の5つの企業グループの公開データスライスでインスタンス化し、3つの研究課題を評価する。
  論文  参考訳（メタデータ） (2026-07-09T01:08:33Z)
• PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation [51.92442051257354]
  PairCoderは、実行のみではなく、完全な公式メトリックスイート上で、アーティファクトが検証可能なすべてのベンチマークを本質的に改善する。 TikZのコンパイルレートは、各モデルで10から30ポイント、シングルモデルの2.9から9.2倍である。
  論文  参考訳（メタデータ） (2026-07-02T08:36:02Z)
• Maestro Order: A Model-Agnostic Orchestration Harness [0.5414847001704247]
  本稿では、信頼できない解法を信頼性の高い問題解決システムに変換するモデルに依存しないオーケストレーションハーネスを提案する。 アーキテクチャ、メッセージおよび状態スキーマ、コントローラアルゴリズム、そして決定論的で観測可能でフォールトトレラントなエンジニアリングを提供します。 パラメータ化ソルバ/検証器モデル上でのハーネスの忠実なモンテカルロシミュレーションの結果を報告する。
  論文  参考訳（メタデータ） (2026-06-22T22:21:59Z)
• A Topology-Aware, Memory-Centric Architecture that Separates Root-Cause Derivation from Root-Cause Explanation [0.0]
  自律的な操作において欠落する要素は、より良い異常検出やより大きな言語モデルではなく、運用メモリである、と我々は主張する。 OPS C ORTEXは、動作中のマルチエージェントプロトタイプで、このメモリを4層に整理し、フィールドが通常混在している2つのタスクを分離する。
  論文  参考訳（メタデータ） (2026-06-18T09:20:20Z)
• A Universal Cliff and a Design Fingerprint: Cross-Section Defect Detection Under LLM Orchestration [0.0]
  生産言語モデルシステムは、労働者エージェントの目に見えないオーケストレーションにまたがってそれを拡大する要求に答える。 これは、単一のワーカーが見ることができない欠陥のクラスに何をもたらすか尋ねる。 1人の開発者から5世代にわたる10のシステムと、異なるアライメントパラダイムからの5つのプロバイダのみです。
  論文  参考訳（メタデータ） (2026-05-25T05:09:48Z)
• Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks [0.0]
  確率的検証パターン(自己整合性投票、レビュアー LLM アンサンブル)は、人工物ではなく、判断を生成する。 Pramana は、ワイヤフォーマットの欠如を定義している。すべての連続エージェント出力は、タイプ付き ClaimAttestation でラップされ、4つの変種のうちの1つでラップされる。 プラマナは3つの対称性を再現したモデル(38,563個の到達可能な状態、0個の不変な違反)でTLCの下で徹底的に検証された。
  論文  参考訳（メタデータ） (2026-05-19T17:00: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)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• Where LLM Agents Fail and How They can Learn From Failures [62.196870049524364]
  大規模言語モデル(LLM)エージェントは、複雑なマルチステップタスクの解決において有望であることを示す。 単一ルート原因エラーがその後の決定を通じて伝播する、障害のカスケードに対する脆弱性を増幅する。 現在のシステムは、モジュール的で体系的な方法でエージェントエラーを包括的に理解できるフレームワークを欠いている。 AgentErrorTaxonomyは、メモリ、リフレクション、計画、アクション、システムレベルの操作にまたがる障害モードのモジュール分類である。
  論文  参考訳（メタデータ） (2025-09-29T18:20:27Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。 ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。 我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。 我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
  論文  参考訳（メタデータ） (2025-04-07T03:57:41Z)
• Do Large Language Model Benchmarks Test Reliability? [66.1783478365998]
  モデル信頼性の定量化について検討する。 信頼性評価におけるこのギャップにより、我々はいわゆるプラチナベンチマークの概念を提案する。 我々は、これらのプラチナベンチマークにおいて、幅広いモデルを評価し、実際、フロンティアLSMは、単純なタスクで失敗を示す。
  論文  参考訳（メタデータ） (2025-02-05T18:58:19Z)

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

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