FVSpec: 現実世界のプロパティベーステストをリーンチャレンジとして

要旨

本稿では、実世界の形式的ソフトウェア検証タスクにおけるAIモデルおよびエージェントの評価のためのベンチマークを提案する。まず、実在のPythonリポジトリから11,039件のプロパティベーステスト（PBT）を収集し、そのうち2,772件（25％）を自動的に9,415件のLean 4仕様（sorryプレースホルダー付き）に変換する（PBTあたり約3件の形式化；品質指標で支配的なものが存在しない場合、複数の試行を保持する）。PBTをLean仕様に変換する作業は困難を伴う。なぜなら、Pythonの意味論をLean上でモデル化し、命令型PBTに符号化された論理プロパティを推論し、さらに使用頻度の低い言語における依存型プログラミング特有の難しさに対処する必要があるからである。本稿では、PBTをLean仕様に変換するための3エージェントLLMパイプラインを説明し、カバレッジと品質指標を評価するとともに、自動化手法およびモデルベース手法を用いた証明生成のベースラインを提供する。すべてのコード（スクレイパーおよびエージェント）とデータ（PBTおよびLean仕様）はオープンソースとして公開されている。本ベンチマークは、AIが生成するコードが増加する中で注目が高まっている、現実世界のソフトウェアに対するAI支援による形式的検証という未開拓の課題の進展を促進することを目的とする。

English

We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.