論文の概要: Towards Agentic Proof Harness Engineering
- arxiv url: http://arxiv.org/abs/2610.23241v1
- Date: Fri, 16 Oct 2026 10:08:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-20 00:56:07.863102
- Title: Towards Agentic Proof Harness Engineering
- Title（参考訳）: エージェントによるハーネス工学の証明に向けて
- Abstract要約: ソフトウェアプロジェクトから検証可能なハーネスを自動的に構築するエージェント実証ハーネスエンジニアを提案する。
カールおよびリブの探索的ケーススタディにおいて,本手法の有効性について検討した。
- 参考スコア（独自算出の注目度）: 1.7396274240172123
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Formal verification of real-world projects requires substantial manual effort, from specifying correctness properties to constructing the infrastructure needed to check them. We envision verification agents that assist developers throughout this process. Among the many tasks involved, one stands out as both foundational and amenable to automation: proof-harness engineering. A proof harness defines an isolated verification environment for a program unit, such as a function or module, by providing symbolic inputs, initialization code, and models of its dependencies. Today, proof-harness engineering remains largely a manual task performed by verification engineers. To explore the potential of coding agents for this task, we propose an agentic proof-harness engineer that automatically constructs verifier-ready harnesses from a software project and a designated verification target. We combine the agent with formal soundness and precision guards to validate generated abstractions and guide their refinement. We evaluate the feasibility of our approach in an exploratory case study on curl and libuv, using three historical assertion violations already embedded in the source code as verification properties. Our results show that the agent successfully constructs proof harnesses that enable CBMC to detect all three violations. We further demonstrate the potential for reusing these harnesses with other verification tools.
- Abstract（参考訳）: 実際のプロジェクトの形式的検証には、正確性プロパティの指定から、チェックに必要なインフラストラクチャの構築に至るまで、かなりの手作業が必要になります。
このプロセスを通じて開発者を支援する検証エージェントを構想する。
関連する多くのタスクの中で、自動化に基礎的かつ考慮すべきものとして際立っているのは、証明ハーネスエンジニアリングである。
証明ハーネスは、シンボル入力、初期化コード、依存関係のモデルを提供することにより、関数やモジュールなどのプログラムユニットの独立した検証環境を定義する。
今日では、証明ハーネスエンジニアリングは、検証エンジニアが行う手作業がほとんどである。
本課題のコーディングエージェントの可能性を探るため,ソフトウェアプロジェクトと指定された検証対象から検証可能なハーネスを自動的に構築するエージェント・証明・ハーネス・エンジニアを提案する。
エージェントを正規の音質と精密ガードと組み合わせて、生成した抽象化を検証し、その洗練を導く。
我々は,すでにソースコードに埋め込まれている3つの歴史的アサーション違反を検証特性として,curl と libuv の探索的ケーススタディにおいて,我々のアプローチの有効性を評価する。
以上の結果から,CBMCが3つの違反を全て検出できる証明ハーネスの構築に成功した。
さらに、これらのハーネスを他の検証ツールで再利用する可能性を実証する。
関連論文リスト
- AlphaDiana: A Measurement System for Agents in Verifiable Reasoning Tasks [70.52860945958031]
我々は、データセット、エージェント、環境、スコアラーの計測システムであるAlphaDianaを紹介する。
5つの回答ベースベンチマークで3つのオープンソースモデルと3つのオープンソースハーネスについて検討する。
ハーネスは推論の精度を常に改善しないことがわかった。
論文 参考訳（メタデータ） (2026-10-14T14:04:48Z) - AgentSWE: Can Coding Agents Build the Agent You Actually Want? [27.064072390170466]
本稿ではエージェント開発ライフサイクルの3段階にまたがるエージェントソフトウェアエンジニアリングのベンチマークであるエージェントSWEを紹介する。
25のタスクはそれぞれ、試験ではなく委員会としてフレーム化されている。
要求が要求するものを提供するにはほど遠いものはありません。
論文 参考訳（メタデータ） (2026-10-09T10:35:27Z) - Attestable Audit: Property-Based Attestation for Proprietary Workloads without Artifact Disclosure [0.0]
アーティファクトを開示することなく、このギャップを埋めるアーキテクチャを提案する。
Pythonコード上でBanditセキュリティアナライザを実行するGlamine Library OSによるIntel SGXの概念実証実装は、このアプローチの実用性を示している。
論文 参考訳（メタデータ） (2026-10-03T12:29:47Z) - Reality Is the Final Verifier: On Two Key Gaps in Agentic Software Engineering [78.51705689800838]
本稿では, 要求, モデル, 評価器の見直しに, 展開証拠を用いた保証・修正ループを提案する。
そこで我々は,人的判断,エージェント能力,計算能力に対する資源配分問題としてエージェント開発を保証した。
論文 参考訳（メタデータ） (2026-09-10T17:58:48Z) - Model-Based Agentic Software Engineering [6.7121681028919475]
コーディングエージェントは、プロジェクトの意図、システム構造、あるいは受け入れ証拠を明確化せずに、実装能力を高める。
モデルベースエージェントソフトウェア工学(MAGE)について紹介する。
MAGEは、コモディティインテリジェンスから信頼できる自律性を構築するためのフレームワークであり、理論である。
論文 参考訳（メタデータ） (2026-08-25T21:43:16Z) - Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
製品化は、ソースバウンダリ、エンティティルーティング、回答コントラクト、再現可能なトレースの要件を追加します。
本稿では,このパターンをトレース可能な監査可能なLLMエージェントアーキテクチャに再構成するハーネスエンジニアリング手法を提案する。
韓国の5つの企業グループの公開データスライスでインスタンス化し、3つの研究課題を評価する。
論文 参考訳（メタデータ） (2026-07-09T01:08:33Z) - From Question Answering to Task Completion: A Survey on Agent System and Harness Design [67.8241530947325]
本研究はモデルハーネスレンズを用いてLCMをベースとしたエージェントについて検討する。
まず, LLMをベースとしたエージェントを基礎モデルと実行ハーネスとして, エージェントの機能的定義と実装の視点を明らかにする。
次に、モデル中心のスケーリングの限界を分析し、エージェントエンジニアリングの4つのパラダイムをトレースし、実行ハーネスを6つの結合ランタイム責任に分解する。
論文 参考訳（メタデータ） (2026-06-14T05:40:16Z) - Code as Agent Harness [107.31925305395957]
新興のエージェントシステムでは、コードはもはや単なる目標出力ではない。
コードはエージェントの推論、行動、環境モデリング、実行ベースの検証のための運用上の基盤としてますます役立っている。
この調査は、実行可能、検証可能、ステートフルなAIエージェントシステムに向けた統一されたロードマップを提供する。
論文 参考訳（メタデータ） (2026-05-18T17:59:03Z) - AI Harness Engineering: A Runtime Substrate for Foundation-Model Software Agents [1.4323566945483497]
ファンデーションモデルは、自動コード生成を変革しましたが、現実的な開発環境では、自律的なソフトウェアエンジニアリングエージェントは信頼できないままです。
本稿では,基盤モデルエージェントがプロジェクトを観察し,それを処理し,フィードバックを受信し,変更が完了したことを確定する,モデルハーネス環境システムを提案する。
このフレームワークは、ファンデーションモデルがパッチを作成できるかどうかから、モデルハーネス環境システムが検証可能な正確さ、属性、メンテナンス可能な変更を生成できるかどうかという、自律的なソフトウェアエンジニアリングの中心的な疑問を再考する。
論文 参考訳（メタデータ） (2026-05-13T11:14:59Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。