論文の概要: Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale
- arxiv url: http://arxiv.org/abs/2611.02285v1
- Date: Sun, 01 Nov 2026 23:29:34 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-11-03 20:08:13.12107
- Title: Modern Software Engineering with Verification Agents: A Spec-First Architecture for Autonomous Synthesis, Verification IRs, and Organizational Scale
- Title（参考訳）: 検証エージェントを用いた最新のソフトウェアエンジニアリング: 自動合成、検証IR、組織規模のためのスペックファーストアーキテクチャ
- Abstract要約: 本稿では,エージェントが認証したソフトウェアエンジニアリングのためのエンドツーエンドアーキテクチャを提案する。
スペックファーストスタックインバージョンとゼロコードレビューワークフローを組み合わせたロジックに依存しない基盤を確立する。
我々は、Personal Spec-CopilotsとShared Synthesis Fleetを使って、複数チーム間のコラボレーションをスケールします。
- 参考スコア（独自算出の注目度）: 0.0
- License:
- Abstract: When autonomous coding agents synthesize implementation code, formal specifications, and mechanical proofs simultaneously, the software engineering hierarchy inverts: the formal specification becomes the primary human-reviewed artifact, while source code and proof scripts become disposable build outputs. This paper presents an end-to-end architecture for agent-authored, formally verified software engineering. First, we establish a logic-agnostic foundation combining a spec-first stack inversion, a zero-code-review workflow gated by automated continuous integration (CI) checks, and a minimal Verification Intermediate Representation (VIR) lowered via a thin, verified translator. Second, we pair an extensional Computational Type Theory (CTT) specification layer with Higher-Order Abstract Syntax (HOAS) and linear resource typing in the VIR--eliminating rewrite friction for synthesis agents while defining an experiment, its protocol frozen before the first reader, to measure whether removing boundary coercions improves human specification readability. Third, we scale collaboration across multi-team organizations using Personal Spec-Copilots and a Shared Synthesis Fleet that detects cross-team Semantic Merge Conflicts and fuses modular contracts into zero-copy binaries. We illustrate this architecture on a zero-copy authenticated message router and distinguish our existing empirical baselines (salt, SaltBench, x86lean, and MetaPRL) from newly proposed components.
- Abstract（参考訳）: 自律的なコーディングエージェントが実装コード、正式な仕様、機械的証明を同時に合成すると、ソフトウェア工学の階層は逆転する: 正式な仕様は、人間がレビューした主要なアーティファクトとなり、ソースコードと証明スクリプトは、使い捨てのビルド出力となる。
本稿では,エージェントが認証したソフトウェアエンジニアリングのためのエンドツーエンドアーキテクチャを提案する。
まず、仕様ファーストスタックのインバージョン、自動化された継続的インテグレーション(CI)チェックによってゲートされるゼロコードレビューワークフロー、そして、薄型で検証されたトランスレータによる最小限の検証中間表現(VIR)を組み合わせたロジックに依存しない基盤を確立する。
第2に、拡張計算型理論(CTT)仕様層と高次抽象構文(HOAS)と、VIRの線形リソースタイピングとを組み合わせ、第1読取機の前に凍結されたそのプロトコルである実験を定義しながら、合成エージェントの書き換え摩擦を除去し、境界の強制的除去が人間の仕様の可読性を向上させるかどうかを測定する。
第3に、Personal Spec-Copilotsと、チーム間のセマンティックマージ競合を検出し、モジュール契約をゼロコピーバイナリに融合する共有合成フリートを使用して、複数のチーム間のコラボレーションをスケールします。
本稿では、このアーキテクチャをゼロコピー認証メッセージルータ上に記述し、既存の経験的ベースライン(salt、SaltBench、x86lean、MetaPRL)を新たに提案したコンポーネントと区別する。
関連論文リスト
- Code as Representation: A Compilable Parsing Paradigm for Academic Documents [50.40789738182074]
Compilable Academic Document Parsing (CADP)は、コンテキストラプラス実行可能なPythonとして全ページを再構築するパラダイムである。
テキストと複数のSAEタイプを含む全学術ページのエキスパート検証ベンチマークであるCADP-Benchを紹介する。
その結果、フロンティアモデルでさえも、高忠実度で実行可能な再構築を行うのに苦戦していることがわかった。
論文 参考訳（メタデータ） (2026-08-18T09:10:43Z) - PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
PRIMAは、複数時間にわたる協調型マルチエージェント研究システムとして運用されている。
主なコントリビューションは、生存可能な障害モードのための3つの運用パターンである。
グラフ同型ケーススタディは、生成されたアーティファクトのアーキテクチャ的クレームを根拠にしている。
論文 参考訳（メタデータ） (2026-05-23T23:27:46Z) - Code as Agent Harness [107.31925305395957]
新興のエージェントシステムでは、コードはもはや単なる目標出力ではない。
コードはエージェントの推論、行動、環境モデリング、実行ベースの検証のための運用上の基盤としてますます役立っている。
この調査は、実行可能、検証可能、ステートフルなAIエージェントシステムに向けた統一されたロードマップを提供する。
論文 参考訳（メタデータ） (2026-05-18T17:59:03Z) - Reversa: A Reverse Documentation Engineering Framework for Converting Legacy Software into Operational Specifications for AI Agents [0.0]
本稿では,レガシソフトウェアをAIエージェントのトレーサブルな運用仕様に変換するためのリバースドキュメンテーションエンジニアリングフレームワークであるReversaを紹介する。
特殊なエージェントは、プロジェクト表面をマッピングし、モジュールを分析し、暗黙のルールを抽出し、アーキテクチャを合成し、ユニットレベルの仕様を書き、生成されたクレームをレビューする。
提案では,コードと仕様間のトレーサビリティ,明確な信頼性マーキング,人間の検証のためのギャップの保存という,3つのメカニズムを強調している。
論文 参考訳（メタデータ） (2026-05-18T17:23:13Z) - From I/O to Code with Discovery Agent [103.88427301265669]
IO2Codeの発見エージェントであるDIO-Agentを提案する。
本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。
大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
論文 参考訳（メタデータ） (2026-05-14T18:57:32Z) - Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
LeetProofは、Leanに埋め込まれたマルチモーダル検証ツールであるVelvet上に構築されたエージェントパイプラインである。
動的検証、自動証明、インタラクティブな証明スクリプティングを1つの基礎フレームワークで組み合わせる。
我々は、認定合成に関する先行研究から得られたベンチマークに基づいてLeetProofを評価する。
論文 参考訳（メタデータ） (2026-04-17T14:56:45Z) - Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。
本稿では,再構築による理解という,新しいパラダイムを提案する。
マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-11T09:23:20Z) - Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。
その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。
本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
論文 参考訳（メタデータ） (2025-08-28T13:00:28Z) - VeriMind: Agentic LLM for Automated Verilog Generation with a Novel Evaluation Metric [4.590930025882158]
We propose VeriMind, a agentic LLM framework for Verilog code generation。
本稿では,従来のpass@k測度とARC(Average Refinement Cycles)を組み合わせた新しい評価手法を提案する。
様々なハードウェア設計タスクの実験結果によると、我々のアプローチはpass@kメトリックで最大8.3%、pass@ARCメトリックで最大8.1%向上した。
論文 参考訳（メタデータ） (2025-03-15T23:43:06Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。