Technische Samenvatting: FVSpec

Probleemstelling

Het artikel adresseert de kritieke kloof in AI-ondersteunde formele verificatie (FV) voor real-world software. Voorstellen voor AI-veiligheid leunen steeds vaker op autonome agenten om door AI gegenereerde code formeel te verifiëren, maar huidige benchmarks slagen er niet in dit doel te ondersteunen. Bestaande benchmarks (bijv. Minif2f, PutnamBench) richten zich op wiskundige Olympiade-problemen of door experts geschreven theorem prover-code, wat aanzienlijk verschilt van het "normale" software engineering landschap. Real-world software omvat complexe afhankelijkheidsbomen, black-box externe API's en componenten geschreven in verschillende talen, wat het inherent moeilijker maakt om te verifiëren dan monolithische, gesloten systemen. Bovendien is er een gebrek aan hoogwaardige, grootschalige datasets afgeleid van code geschreven door engineers zonder intentie tot formele verificatie, wat noodzakelijk is om agenten te trainen die "out-of-distribution" kunnen opereren ten opzichte van hun trainingsdata.

Methodologie

De auteurs introduceren FVSpec, een benchmark-generatiepijplijn die real-world Property-Based Tests (PBT's) transformeert naar formele verificatie-uitdagingen in Lean 4. Het proces bestaat uit drie hoofdfasen:

1. Dataverzameling (FVSpec:PBT):

   • Het team heeft 11.039 unieke PBT's gescraped uit 333 open-source Python-repositories met behulp van het Hypothesis-framework.
   • Repositories werden gefilterd op basis van permissieve licenties en duplicaten (inclusief forks) werden verwijderd om diversiteit te waarborgen.
   • Het resulterende corpus vertegenwoordigt "gewone" software engineering, met tests variërend van triviale asserties tot complexe multi-strategie tests.

2. Agentic Transpilatie (FVSpec:FV):

   • Een drievoudige agent LLM-pijplijn vertaalt de Python PBT's en de bijbehorende code naar Lean 4.
   • Function Discovery: Gebruikt tree-sitter om de Function Under Test (FUT) en de transitieve afsluiting van de lokale afhankelijkheden te extraheren.
   • Vertaling: Een formalisatie-agent genereert twee bestanden: Impl.lean (een berekenbare port van de functie) en Spec.lean (theorem statements die overeenkomen met de PBT-asserties, waarbij bewijzen worden achtergelaten als sorry placeholders).
   • Iteratieve Reparatie: De pijplijn hanteert een Language Server Protocol (LSP) loop. Als de gegenereerde Lean-code niet compileert (via lake build), worden de compiler-diagnostieken teruggekoppeld naar de agent voor revisie. Deze loop draait tot 16 iteraties.
   • Afhandeling van Effecten: Voor code die te maken heeft met side-effects (bijv. Redis, file I/O), axiomatiseert de agent deze externe systemen als ongeïnterpreteerde interfaces. Theorems worden gesteld over deze axioma's, waardoor de bewijslast betekenisvol blijft met betrekking tot de logica van de code, zelfs als de concrete implementatiedetails worden geabstraheerd.

3. Post-productie en Filtering:

   • Gegenereerde samples ondergaan een rigoureuze validatie. Mislukkingen worden gecategoriseerd (bijv. timeouts, type mismatches, onbekende identifiers).
   • Een "structurele getrouwheidsscore" wordt berekend op basis van vijf sub-metrieken: parameter coverage, type correspondence, strategy coverage, assertion coverage en dependency coverage.
   • Samples worden gegradeerd op moeilijkheidsgraad (Easy/Hard) met behulp van een gekalibreerde LLM-judge (claude-haiku-4-5).
   • De uiteindelijke dataset behoudt meerdere formalisaties per PBT als geen enkele poging domineert op kwaliteitscriteria, wat resulteert in 9.415 uitdagingen afgeleid van 2.772 unieke PBT's.

Belangrijkste Bijdragen

1. FVSpec:PBT: Een corpus van 11.039 gededupliceerde Python PBT's gescraped uit open-source repositories, wat de eerste grootschalige, licentie-schone dataset van PBT's uit gewone softwareontwikkeling vertegenwoordigt (exclusief competitieve programmering of gecureerde ITP-code).
2. FVSpec:FV: Een dataset van 9.415 Lean 4 formele verificatie-uitdagingen. Elke uitdaging bevat de originele Python-code, de originele PBT, een Lean-implementatie en een Lean theorem statement met bewijslasten. De dataset heeft een mediane structurele getrouwheid van 0,65, waarbij 62% van de uitdagingen als "hard" wordt geclassificeerd.
3. Baseline Evaluaties: Prestatie-metrieken voor frontier-modellen (Claude Sonnet 4.6, Claude Opus 4.7, en GPT-5.4). De modellen behaalden een gemiddeld succespercentage van 70% op "easy" problemen en 49% op "hard" problemen, wat aangeeft dat de benchmark nog niet verzadigd is.
4. Open Source Release: De volledige pijplijn (scraper, dependency extractor, formalization agent en scripts) en datasets worden uitgebracht onder een dubbele MIT/Apache licentie.

Resultaten

• Pipeline Opbrengst: De transpilatie-pijplijn slaagde erin om 25% van de initiële 11.039 PBT's om te zetten in geldige Lean-uitdagingen (9.415 samples).
• Kwaliteitsmetrieken: De mediane structurele getrouwheidsscore is 0,65. Type correspondence (1,00) en assertion coverage (0,97) zijn hoog, terwijl parameter coverage (0,24) en dependency coverage (0,48) lager zijn, wat aangeeft op welke gebieden de vertaalgetrouwheid varieert.
• Modelprestaties: Baseline-modellen losten 70% van de easy samples op en 49% van de hard samples. De refusal rates waren laag (4–8% voor easy, 3–25% voor hard), wat suggereert dat modellen de taken over het algemeen proberen uit te voeren.
• Complexiteit: De mediane sample bevat 6 theorems. De dataset bevat een breed scala aan complexiteit, van eenvoudige sorteeralgoritmes tot complexe workflow job schedulers die te maken hebben met timeouts en state transitions.

Betekenis en Claims

Het artikel beweert dat FVSpec een noodzakelijke fundering biedt voor het bevorderen van AI-ondersteunde formele verificatie van real-world software. In tegen tegenstelling tot eerdere benchmarks die vertrouwen op door experts geschreven bewijzen of wiskundige problemen, afleidt FVSpec specificaties van engineers die geen intentie tot formele verificatie hadden. Dit zorgt ervoor dat de problemen "out-of-distribution" zijn ten opzichte van standaard model trainingsdata, wat een strengere test biedt voor het vermogen van een agent om te generaliseren.

De auteurs positioneren dit werk als een stap naar "Guaranteed Safe AI" en "Scalable Formal Oversight", waarbij autonome agenten software moeten verifiëren even snel en effectief als ze deze schrijven. Door een grootschalige, realistische benchmark te bieden, beoogt FVSpec vooruitgang te stimuleren in het trainen van agenten die in staat zijn de complexiteit van moderne software-ecosystemen aan te kunnen, inclusief externe afhankelijkheden en side-effects, die vaak genegeerd worden in synthetische benchmarks. Het artikel erkent bescheiden beperkingen, zoals het potentieel dat axiomatisering specifieke side-effect semantiek kan missen en het gebrek aan menselijke expert-baselines voor moeilijkheidsgraad-kalibratie.