論文の概要: Agentic Separation Logic Specification Synthesis

• arxiv url: http://arxiv.org/abs/2605.27531v1
• Date: Tue, 26 May 2026 18:05:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:55.3925
• Title: Agentic Separation Logic Specification Synthesis
• Title（参考訳）: エージェント分離論理の合成
• Authors: Tarun Suresh, David Korczynski, Julien Vanegue,
• Abstract要約: Spec-Agentは、大規模なC++で表現力のある、よく検証された仕様を合成するためのエージェントシステムである。 それぞれの関数に対して、Spec-Agentは静的解析とランタイムヒープトレースを使用して、適切なターゲット仕様言語を選択する。 数百万行のコードからなるオープンソースのC++上でSpec-Agentを評価する。
• 参考スコア（独自算出の注目度）: 4.177196802192322
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Specification synthesis, the task of automatically inferring formal specifications from program implementations and natural language, is important for refactoring, transpilation, optimization, and verification, yet remains an open challenge for large C++ repositories. Existing LLM-based approaches fail to simultaneously scale to such repositories, produce specifications expressive enough to capture systems-code features such as dynamic memory and heap-allocated data structures, and systematically validate those specifications to rule out incorrect candidates. We present Spec-Agent, an agentic system for synthesizing expressive, well-validated specifications across large C++ codebases. Spec-Agent targets a ladder of specification languages: propositional logic, first-order logic, propositional separation logic, and first-order separation logic. For each function, Spec-Agent uses static analysis and runtime heap tracing to select the appropriate target specification language, generalizes existing functional tests into fuzz harnesses, and iteratively refines LLM-generated candidates via counterexample-guided feedback. We evaluate Spec-Agent on open source C++ codebases comprising millions of lines of code. Spec-Agent synthesizes valid specifications for 85% of target functions, with no false positives observed under fuzzing and expert validation, outperforming Claude Code Opus 4.6 at 10x lower token cost.
• Abstract（参考訳）: プログラム実装と自然言語から正式な仕様を自動的に推測するタスクである仕様合成は、リファクタリング、トランスパイル、最適化、検証に重要であるが、大規模なC++リポジトリではオープンな課題である。 既存のLCMベースのアプローチは、そのようなリポジトリに同時にスケールできず、動的メモリやヒープに割り当てられたデータ構造といったシステムコードの特徴を捉えるのに十分な仕様を作成し、それらの仕様を体系的に検証して誤った候補を除外する。 提案するSpec-Agentは,大規模なC++コードベースにまたがって,表現力のある,十分に検証された仕様を合成するエージェントシステムである。 Spec-Agentは、命題論理、一階論理、命題分離論理、一階分離論理という一連の仕様言語をターゲットにしている。 それぞれの関数に対して、Spec-Agentは静的解析とランタイムヒープトレースを使用して、適切なターゲット仕様言語を選択し、既存の機能テストをファジハーネスに一般化し、反例誘導フィードバックを通じてLCM生成候補を反復的に洗練する。 数百万行のコードからなるオープンソースのC++コードベース上でSpec-Agentを評価する。 Spec-Agentはターゲット関数の85%の有効な仕様を合成するが、ファジングや専門家による検証では偽陽性は見られず、Claude Code Opus 4.6を10倍のトークンコストで上回っている。

関連論文リスト

• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  本稿では,この課題に対処するための2段階のLLMベースのワークフローを,インテリジェント車両サイバーセキュリティケーススタディで紹介する。 第一段階では、AIベースのルールマイナーが自然言語要求から検証可能なルールを抽出する。 第2段階では、AIベースのコード監査者が、抽出されたルールに対する実装証拠をチェックする。
  論文  参考訳（メタデータ） (2026-05-18T06:34:03Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  IO2Codeの発見エージェントであるDIO-Agentを提案する。 本手法は,プログラム空間上の進化的探索としてIO2Codeをフレーム化する。 大規模な実験により、DIO-Agentは従来のプログラムバイサンプル法とSOTA進化エージェントベースラインの両方を一貫して上回っていることが示された。
  論文  参考訳（メタデータ） (2026-05-14T18:57:32Z)
• Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
  メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。 本稿では,Cプログラムのメモリ対応形式関数仕様を自動生成するニューロシンボリックフレームワークを提案する。 我々は,メモリ対応の形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。
  論文  参考訳（メタデータ） (2026-03-12T15:02:26Z)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• SpecMap: Hierarchical LLM Agent for Datasheet-to-Code Traceability Link Recovery in Systems Engineering [8.235446273226277]
  組み込みシステムとそれに対応するコード実装の間のトレーサビリティは、システムエンジニアリングにおける根本的な課題である。 既存のトレーサビリティリンク回復アプローチは、語彙的類似性と情報検索技術に依存している。 本稿では,意味解析に大規模言語モデルを用いる階層型コードマッピング手法を提案する。
  論文  参考訳（メタデータ） (2026-01-16T11:50:18Z)
• Connecting the Dots: Training-Free Visual Grounding via Agentic Reasoning [63.109585527799005]
  GroundingAgentは、タスク固有の微調整なしで動作するビジュアルグラウンドティングフレームワークである。 広く使用されているベンチマークでは、平均ゼロショットグラウンドの精度は65.1%である。 また、強い解釈可能性を提供し、各推論ステップを透過的に照らす。
  論文  参考訳（メタデータ） (2025-11-24T03:11:08Z)
• SLD-Spec: Enhancement LLM-assisted Specification Generation for Complex Loop Functions via Program Slicing and Logical Deletion [29.231420590756954]
  SLD-Specは、複雑なループ構造を持つプログラムに適したLCM支援仕様生成方法である。 SLD-Specは最先端のAutoSpecよりも5つのプログラムの検証に成功し、ランタイムを23.73%削減した。
  論文  参考訳（メタデータ） (2025-09-12T01:40:27Z)
• AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
  LLM(Large Language Models)は、現実世界のエージェントアプリケーションにおいて高度な機能を示す。 AgentIFは、エージェントシナリオでLLM命令に従う能力を体系的に評価する最初のベンチマークである。
  論文  参考訳（メタデータ） (2025-05-22T17:31:10Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)

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

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