論文の概要: Specification-first convergence with an AI coding agent: a case study of dismantling a core architectural invariant across 189 files in a 717k-line codebase with no test oracle and no human code review
- arxiv url: http://arxiv.org/abs/2608.12440v2
- Date: Sat, 15 Aug 2026 11:27:55 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-18 13:30:43.58497
- Title: Specification-first convergence with an AI coding agent: a case study of dismantling a core architectural invariant across 189 files in a 717k-line codebase with no test oracle and no human code review
- Title（参考訳）: AIコーディングエージェントによる仕様ファーストコンバージェンス:テストオラクルがなく、人間のコードレビューもない717kラインコードベースにおいて、189のファイルにまたがるコアアーキテクチャ不変性を分解するケーススタディ
- Authors: Joel Abenhaim,
- Abstract要約: 本稿では,AI符号化エージェントによる大規模建築解体のケーススタディについて報告する。
ここで述べられているプロトコルの下で、エージェントはそれを正常に完了した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper reports a single, fully instrumented case study of a large-scale architectural refactoring by an AI coding agent under a specification-first protocol, with no human review of the generated code and no pre-existing oracle to validate the target behaviour. The task, dismantling a central invariant across a large interdependent codebase, was assessed by the author as effectively infeasible through incremental refactoring, the kind of change that conventionally calls for a rewrite instead. Under the protocol described here, the agent completed it successfully. The system is a 717,725-line production TypeScript application across 3,648 files. The task required dismantling a core lifetime invariant: the guarantee that a UI panel remains open for the duration of an AI request. The target behaviour was that a streaming generation survives the closing of its panel and can be reattached, on reopening, to the same live stream with no loss or duplication. The protocol: formal specification by the agent, 14 refinement cycles auditing that specification against the source code, atomic implementation, a compile/test feedback loop, then 17 verification cycles auditing the code against the frozen specification. Across 31 audit passes, 201 defects were corrected before any human executed the program. The convergence criterion was empirical: two consecutive verification passes returning zero findings. The change touched 189 files (31 new); with the extraction phase, the two commits total 288 files, 34,770 insertions, 16,422 deletions. Across the first and roughly thirty later sessions, the software behaved as specified, no bug observed. Elapsed: three days; cost: USD 2,430. The full specification and raw session logs, 1,500+ pages in French, are published as evidence, allowing inspection of the process and submission to a language model for consistency checking.
- Abstract（参考訳）: 本稿では,AIコーディングエージェントによる大規模アーキテクチャリファクタリングを,仕様優先のプロトコルで実施するケーススタディについて報告する。
このタスクは、大きな相互依存コードベースで中心的な不変性を分解し、インクリメンタルリファクタリングによって効果的に実現不可能であると著者によって評価された。
ここで述べられているプロトコルの下で、エージェントはそれを正常に完了した。
システムは、3,648ファイルにわたる717,725行のTypeScriptアプリケーションである。
このタスクでは、AI要求の間、UIパネルがオープンであることを保証するため、コアライフタイム不変性を分解する必要がある。
ターゲットとなる動作は、ストリーミング生成がパネルの閉じた状態に留まり、再開時に損失や重複なく同じライブストリームに切り替わることができることである。
プロトコル:エージェントによる正式な仕様、ソースコードに対してその仕様を監査する14の修正サイクル、アトミック実装、コンパイル/テストのフィードバックループ、そして凍結した仕様に対してコードを監査する17の検証サイクル。
31回の監査パスでは、人間がプログラムを実行する前に201の欠陥が修正された。
収束基準は経験的であり、2つの連続した検証がゼロの結果を返す。
この変更は189のファイル(31新)に触れ、抽出フェーズでは288のファイル、34,770の挿入、16,422の削除をコミットした。
最初のセッションとおよそ30回のセッションで、ソフトウェアは特定の振る舞いをし、バグは観測されなかった。
期間:3日、費用:2,430ドル。
完全な仕様と生のセッションログ(フランス語で1500ページ以上)はエビデンスとして公開され、プロセスの検査と一貫性チェックのための言語モデルへの提出が可能になる。
関連論文リスト
- Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
論文 参考訳（メタデータ） (2026-08-13T17:41:27Z) - Converted, Not Equivalent: Benchmarking Codebase Conversion via Observational Equivalence [56.25095230687242]
コーディングエージェントは、しばしば自身のローカル検証ルーチンを過度に信頼し、表面チェックを満たすアーティファクトの成功を宣言する。
この問題は、事前評価が結果駆動である変換において特に深刻である。
ブラインド・コンバージョンは26.7-28.9%に達し、スペック・パスレートは91.1%まで上昇した。
このことは、失敗は限られた予算やバックボーンの強さよりも、契約ミスによる自己検証に起因していることを示唆している。
論文 参考訳（メタデータ） (2026-05-27T19:57:15Z) - 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) - Scaling Human-AI Coding Collaboration Requires a Governable Consensus Layer [22.42181408084751]
ビブコーディングは正確で実行可能なコードを高速に生成するが、構造的なコミットメントや依存関係、証拠の記録は残っていない。
本稿では,操作可能な世界モデルであるコンセンサス層Cが,エンジニアリングの主要な成果物としてコードを置き換えるパラダイムであるエージェント・コンセンサスを提案する。
本稿では,チャットによるベースラインと比較して,コンセンサスに基づく人間の介入を減らすかどうかを測定するためのベンチマークタスクファミリーを提案する。
論文 参考訳（メタデータ） (2026-04-20T06:53:32Z) - The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
AIが生成するコード品質の問題に対する業界の主要な反応は、AIレビュアーをデプロイすることだ。
本稿では,実行可能な仕様が存在しない場合,この応答は構造的に円形であると主張している。
論文 参考訳（メタデータ） (2026-03-26T11:59:05Z) - SlopCodeBench: Benchmarking How Coding Agents Degrade Over Long-Horizon Iterative Tasks [55.76734816061826]
我々は20の問題と93のチェックポイントからなる言語に依存しないベンチマークであるSlopCodeBenchを紹介する。
我々は、冗長性、重複コードの割合、構造的侵食という2つの軌道レベルの品質信号を追跡する。
11モデルにまたがるエンドツーエンドの問題を解決するエージェントは存在しない。
論文 参考訳（メタデータ） (2026-03-25T19:26:44Z) - When the Specification Emerges: Benchmarking Faithfulness Loss in Long-Horizon Coding Agents [15.65681557926802]
実際の研究符号化は、しばしばそうではない: 意図されたシステムは、イン・テアアクションを通じて徐々に開示される。
この設定のためのベンチマークを導入し、Ss Loss Under eM ergent s Pecification (SLUMP)について研究する。
論文 参考訳（メタデータ） (2026-03-17T19:53:35Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
本稿では,22の大規模C/C++プロジェクトから得られた関数レベル修正の信頼性の高いベンチマークであるReDefを紹介する。
欠陥ケースはコミットの反転によって固定され、クリーンケースはポストホック履歴チェックによって検証される。
このパイプラインは3,164の欠陥と10,268のクリーンな修正をもたらし、既存のリソースよりも信頼性の高いラベルを提供する。
論文 参考訳（メタデータ） (2025-09-11T07:07:11Z) - Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。
この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。
バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
論文 参考訳（メタデータ） (2025-06-24T13:42:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。