論文の概要: Vero: Can AI Agents Build Formally Verified Software Repositories?
- arxiv url: http://arxiv.org/abs/2608.13522v1
- Date: Thu, 13 Aug 2026 17:41:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 18:29:38.621359
- Title: Vero: Can AI Agents Build Formally Verified Software Repositories?
- Title（参考訳）: Vero: AIエージェントは、形式的に検証されたソフトウェアリポジトリを構築することができるか?
- Abstract要約: Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
- 参考スコア（独自算出の注目度）: 45.09790101960906
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.
- Abstract（参考訳）: AIエージェントはますますプログラミングに使われていますが、生成されたコードの正確性を保証するものではありません。
エージェントが実装とマシンチェックによる仕様の証明の両方を生成する検証コード生成は、信頼できるAI生成ソフトウェアへの強力な道を提供する。
この方向の既存のベンチマークは個々の関数にフォーカスするか、提供された実装で検証生成のみを評価する。
エージェントが実際のマルチモジュールコードベース間でコヒーレントな実装と証明の選択を行えるかどうかはまだ未解決の問題である。
このギャップを埋めるために,リポジトリレベルで共同実装と証明合成を評価する最初のベンチマークであるVeroを導入する。
Veroには、Python、Dafny、Verus、Coqにまたがる実世界のリポジトリからソースされた43のマルチモジュールインスタンスが含まれており、暗号プロトコルから分散システムまでさまざまなドメインをカバーしている。
各インスタンスは、所定のAPIインターフェース、手動でキュレートされた形式仕様、およびリファレンス実装を備えたマルチモジュールのLean 4リポジトリで構成される。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さや参照コードの不正確さを正式に証明する監査メカニズムも含まれている。
リーンツールチェーンアクセスによるフロンティアコーディングエージェント構成の評価を行う。
最強のエージェントは43のインスタンスのうち27だけを完全に解決し、最も難しいリポジトリの仕様をクローズする。
Veroは、リポジトリスケールの検証済みソフトウェア合成に向けた進捗を測定するための具体的なテストベッドを提供する。
ベンチマーク、キュレーションパイプライン、評価ハーネスはhttps://github.com/sunblaze-ucb/vero.comで公開しています。
関連論文リスト
- SWE-Gate: Passing Functional Tests Is Not Enough for Software Engineering Agents [63.65682461568621]
ソフトウェアエンジニアリングエージェントのためのリポジトリレベルのベンチマークであるSWE-Gateを導入し、機能的正当性とともにレビュー制約コンプライアンスを明示的に評価する。
SWE-Gateは、実際のプルリクエストレビューコメントからレビュー制約を導き、これらの制約に関するリポジトリレベルの修復インスタンスを合成する。
各インスタンスは、非準拠およびゴールドパッチとともに、機能テストと制約テストの分離を提供し、イシュー解決能力とレビュー制約コンプライアンスの明確な分離を可能にする。
論文 参考訳（メタデータ） (2026-09-03T17:53:34Z) - Protocol-Driven Development: Governing Generated Software Through Invariants and Continuous Evidence [2.124730017640531]
ここでは、主要なソフトウェアアーチファクトがコードではなく、機械で強化可能なプロトコルであるプロトコル駆動開発(PDD)を紹介します。
PDDは、自動化されたソフトウェアエンジニアリングのためのガバナンスモデルを定義する。
論文 参考訳（メタデータ） (2026-05-13T04:23:14Z) - RepoZero: Can LLMs Generate a Code Repository from Scratch? [13.87780777614509]
RepoZeroは、完全に自動化された実行ベースのレポジトリレベルの生成をスクラッチから検証できる最初のベンチマークである。
我々の結果は、RepoZeroをエンドツーエンドのコード生成のための、困難でスケーラブルで信頼性の高いテストベッドとして確立しています。
論文 参考訳（メタデータ） (2026-05-08T01:56:02Z) - BUILD-AND-FIND: An Effort-Aware Protocol for Evaluating Agent-Managed Codebases [0.0]
BUILD-AND-FINDは、下流エージェントが生成されたリポジトリから意図した選択を復元できるかどうかを評価するプロトコルである。
各タスクに対して、ビルダーは隠されたリポジトリの仕様を見て、仕様に書かれた複数選択の質問バンクを作成します。
このプロトコルは、行動の正しさをアーティファクト側のリカバリから切り離し、リカバリの正確性、再現性、実装のカバレッジ、検査の労力を報告します。
論文 参考訳（メタデータ） (2026-05-07T12:35:27Z) - Code Broker: A Multi-Agent System for Automated Code Quality Assessment [0.0]
我々はGoogle Agent Development Kit ADKで構築されたマルチエージェントシステムであるCode Brokerを紹介する。
ファイル、ローカルディレクトリ、GitHubリポジトリからPythonコードを解析し、実行可能な品質評価レポートを生成する。
論文 参考訳（メタデータ） (2026-04-25T00:53:59Z) - RepoMod-Bench: A Benchmark for Code Repository Modernization via Implementation-Agnostic Testing [1.4069797812477614]
本稿では,実装に依存しない評価パラダイムに基づく,リポジトリレベルのコードモダナイゼーションのためのベンチマークフレームワークを紹介する。
RepoMod-Benchは8つの言語にまたがる、標準化されたインターフェースを備えた21の現実世界リポジトリのベンチマークである。
ベンチマークには1.6万行のコード(LOC)と11,616のテストが含まれており、リポジトリのサイズは14～211KLOCである。
論文 参考訳（メタデータ） (2026-02-26T01:25:00Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - Commit0: Library Generation from Scratch [77.38414688148006]
Commit0は、AIエージェントにスクラッチからライブラリを書くよう促すベンチマークである。
エージェントには、ライブラリのAPIを概説する仕様文書と、インタラクティブなユニットテストスイートが提供されている。
Commit0はまた、モデルが生成したコードに対して静的解析と実行フィードバックを受け取る、インタラクティブな環境も提供する。
論文 参考訳（メタデータ） (2024-12-02T18:11:30Z) - Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。
Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
論文 参考訳（メタデータ） (2024-10-02T09:11:10Z) - RepoCoder: Repository-Level Code Completion Through Iterative Retrieval
and Generation [96.75695811963242]
RepoCoderはリポジトリレベルのコード補完プロセスを合理化するフレームワークである。
類似性ベースのレトリバーと、事前訓練されたコード言語モデルが組み込まれている。
バニラ検索で拡張されたコード補完アプローチよりも一貫して優れています。
論文 参考訳（メタデータ） (2023-03-22T13:54:46Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。