FVSpec: Realweltliche eigenschaftsbasierte Tests als Lean-Herausforderungen

Zusammenfassung

Wir stellen einen Benchmark zur Bewertung von KI-Modellen und -Agenten anhand realer formaler Softwareverifikationsaufgaben vor. Zunächst sammeln wir 11.039 eigenschaftsbasierte Tests (Property-Based Tests, PBTs) aus realen Python-Repositorien, dann übersetzen wir automatisch 2.772 davon (25 %) in 9.415 Lean-4-Spezifikationen mit Sorry-Platzhaltern (etwa 3 Formalisierungen pro PBT; wir behalten mehrere Versuche, wenn keiner bei Qualitätsmetriken dominiert). Die Übersetzung von PBTs in Lean-Spezifikationen ist anspruchsvoll: Sie erfordert die Modellierung der Python-Semantik in Lean, die Ableitung der logischen Eigenschaft, die in einem imperativen PBT kodiert ist, sowie die Bewältigung der inhärenten Schwierigkeiten abhängig typisierter Programmierung in einer selten verwendeten Sprache. Wir beschreiben eine Drei-Agenten-LLM-Pipeline zur Transpilierung von PBTs in Lean-Spezifikationen, evaluieren Abdeckungs- und Qualitätsmetriken und liefern Basislinien für die Beweiserstellung mittels mehrerer automatisierter und modellbasierter Ansätze. Der gesamte Code (Scraper und Agenten) sowie die Daten (PBTs und Lean-Spezifikationen) sind Open Source. Unser Benchmark zielt darauf ab, Fortschritte bei dem bislang wenig erforschten Problem der KI-gestützten formalen Verifikation realer Software zu fördern, das zunehmend an Bedeutung gewinnt, da KI immer mehr Code der Welt produziert.

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.