Technische Samenvatting: VeriScale: Adversariale Test-Suite Schaling voor Verifieerbare Codegeneratie

Probleemstelling

Naarmate Large Language Models (LLM's) steeds vaker worden ingezet voor software-engineering, is het evalueren van hun vermogen om niet alleen functionele code, maar ook formeel verifieerbare specificaties en bewijzen te genereren, cruciaal geworden. Bestaande benchmarks voor verifieerbare codegeneratie, zoals VERINA en CLEVER, vertrouwen sterk op test-suite-evaluatie om Specificatiegeneratie (SpecGen) en Codegeneratie (CodeGen) te beoordelen. Deze benchmarks lijden echter aan een fundamentele beperking: ze worden beperkt door een schaarste aan hoogwaardige testgevallen, met name negatieve testgevallen (onverwachte invoer en onverwachte uitvoer).

Huidige benchmarks bieden doorgaans slechts een beperkt aantal positieve invoer-uitvoerparen. Bijgevolg kunnen modellen opgeblazen slaagpercentages behalen door aan deze schaarse tests te voldoen zonder het programmaproces echt te begrijpen of de geldigheid en volledigheid van hun gegenereerde specificaties te waarborgen. Dit leidt tot een overschatting van modelcapaciteiten, waarbij incorrecte implementaties of ongeldige specificaties de evaluatie doorstaan, simpelweg omdat de testsuite niet in staat is logische fouten of grensovertredingen bloot te leggen.

Methodologie: Het VeriScale-kader

Om deze beperkingen aan te pakken, stellen de auteurs VeriScale voor, een nieuw kader dat wordt gedreven door adversariale implementaties om test suites voor verifieerbare codegeneratie systematisch te schalen en te verfijnen. Het kader werkt in twee hoofdfasen: Test-Suite Uitbreiding en Test-Suite Reductie.

1. Test-Suite Uitbreiding

Het doel van deze fase is het opbouwen van een diverse en uitdagende pool van testgevallen, inclusief verwachte invoer-uitvoerparen, onverwachte invoer en onverwachte uitvoer.

• Zaadgeneratie en Type-bewuste Mutatie: Geïnspireerd door EvalPlus, gebruikt VeriScale LLM's om initiële zaadinvoer te synthetiseren. Deze zaden worden vervolgens uitgebreid via een iteratieve, type-bewuste mutatiestrategie. Het kader formaliseert mutatie als een vijf-tuple-proces ($M = (T, D, O, p, q)$) dat invoertypes behoudt terwijl structurele verstoringen worden geïntroduceerd. Dit omvat het hergebruiken van contextuele waarden uit een "ingrediëntenpool" of het toepassen van type-specifieke heuristieken om complexe randgevallen te genereren.
• Preconditie-gestuurde Invoerclassificatie: Kandidaat-invoer wordt strikt geclassificeerd tegen grondwaarheid-precondities met behulp van een tweestapsverificatiepijplijn in Lean.
  • Syntaxisfilter: Zorgt ervoor dat kandidaten syntactisch geldige Lean-expressies zijn.
  • Bidirectionele Verificatie: Gebruikt #guard decide en plausibele bewijszoektochten om invoer te classificeren als "verwacht" (voldoet aan de preconditie) of "onverwacht" (schendt deze).
• Adversariale Synthese van Onverwachte Uitvoer: Dit is de kerninnovatie. In plaats van te vertrouwen op LLM's om willekeurige onjuiste uitvoer te hallucineren, synthetiseert VeriScale adversariale implementaties.
  • Een capabel model fungeert als "red team" en genereert formele specificaties voor een probleem.
  • Een ander model (of hetzelfde model in een andere rol) probeert adversariale implementaties te ontwerpen die zwakke plekken in deze specificaties uitbuiten.
  • Deze implementaties worden uitgevoerd op verwachte invoer. Als een adversariale implementatie een uitvoer produceert die afwijkt van de grondwaarheid maar vals wordt geaccepteerd door de gegenereerde postcondities, wordt deze uitvoer behouden als een hoogwaardige "onverwachte uitvoer". Dit proces zorgt ervoor dat de testgevallen echt informatief zijn voor het blootleggen van specificatieongeldigheid.

2. Test-Suite Reductie

Om de rekenkosten van de uitgebreide suites te beheersen, hanteert VeriScale reductiestrategieën om de grote pool te destilleren tot compacte maar discriminerende suites.

• Grenzenbehoudende Reductie (voor Onverwachte Invoer): In plaats van willekeurige steekproeven, prioriteert deze strategie invoer die overeenkomt met veelvoorkomende grensovertredingen (bijvoorbeeld lege containers, nulwaarden, niet-overeenkomende lengtes). Het behoudt representatieve voorbeelden uit kritieke grensbuckets om dekking van typische preconditie-overtredingen te waarborgen.
• Adversaris-dodende Reductie (voor Verwachte Invoer): Deze strategie hergebruikt de adversariale implementaties die in de uitbreidingsfase zijn gesynthetiseerd. Elk verwacht invoer-uitvoerpaar wordt beoordeeld op basis van hoeveel "mutante" (adversariale) implementaties het kan "doden" (d.w.z. een andere uitvoer produceren dan). De reductie wordt geformuleerd als een set-dekkingprobleem, waarbij paren die het maximale aantal eerder ongedode mutanten dekken, gretig worden geselecteerd. Dit zorgt ervoor dat de gereduceerde suite het vermogen behoudt om gebrekkige specificaties te onderscheiden.

Belangrijkste Bijdragen

1. VeriScale-kader: De auteurs stellen een algemeen kader voor dat adversariale implementaties benut om zowel de systematische uitbreiding als reductie van test suites voor verifieerbare codegeneratie aan te sturen.
2. VERINAPLUS en VERINALITE: Het kader wordt geïnstancierd op de VERINA-benchmark om twee nieuwe datasets te creëren:
   • VERINAPLUS: Een uitgebreide benchmark met test suites die met meer dan 83× zijn geschaald (specifiek 62,83× voor verwachte invoer, 87,79× voor onverwachte uitvoer en 183,08× voor onverwachte invoer).
   • VERINALITE: Een lichtgewicht variant die met 14× is geschaald, geoptimaliseerd via reductiestrategieën om discriminerend vermogen te behouden met lagere evaluatiekosten.
3. Empirische Validatie: Het artikel toont aan dat de originele benchmarks modelcapaciteiten aanzienlijk overschatten. De verbeterde benchmarks onthullen aanzienlijke zwaktes in state-of-the-art LLM's die eerder verborgen waren.

Experimentele Resultaten

De auteurs evalueerden acht state-of-the-art LLM's (waaronder GPT-5.5, Claude-Sonnet-4.6 en DeepSeek-V4-Pro) over VERINA, VERINAPLUS en VERINALITE.

• Blootlegging van Modelzwaktes: De aangevulde benchmarks veroorzaakten scherpe prestatiedalingen. Zo daalde de SpecGen-score van GPT-5.5 bijvoorbeeld van 68,78% op VERINA naar 44,44% op VERINAPLUS, en daalde de CodeGen-score van 96,83% naar 86,24%. Dit geeft aan dat de schaarse testgevallen van de originele benchmark modellen in staat stelden te slagen zonder echt begrip.
• Vermindering van Evaluatieonzekerheid: De uitgebreide test suites verkleinden de foutmarges in SpecGen-evaluatie aanzienlijk. In de originele benchmark creëerden onbepaalde verificatie-uitkomsten brede gaten tussen boven- en ondergrenzen (bijvoorbeeld een gat van 13,23% voor Claude-Opus-4.7). Op VERINAPLUS werd deze ambiguïteit opgelost, waarbij het gat werd verkleind tot 4,76%, wat een statistisch betrouwbaardere beoordeling biedt.
• Robuustheidsgat: De resultaten benadrukken een fundamenteel verschil: modellen zijn aanzienlijk bekwaamer in CodeGen dan in SpecGen. Terwijl CodeGen-scores matige dalingen zagen, leden SpecGen-scores aan zware dalingen, wat suggereert dat het synthetiseren van geldige en volledige formele specificaties nog steeds een grote bottleneck is voor huidige LLM's.
• Efficiëntie van Reductie: VERINALITE behaalde prestatiedegradatieprofielen die bijna identiek waren aan die van VERINAPLUS, maar met aanzienlijk lagere rekenkosten. De evaluatietijd voor VERINALITE was slechts 1,38× (SpecGen) en 1,05× (CodeGen) de baseline, vergeleken met 1,80× en 1,50× voor de volledige VERINAPLUS-suite.

Betekenis en Claims

Het artikel stelt dat VeriScale een cruciale, uiterst betrouwbare standaard biedt voor de vooruitgang van op LLM's gebaseerde verifieerbare codegeneratie. Door verder te gaan dan schaarse positieve tests en adversariaal gesynthetiseerde negatieve gevallen op te nemen, biedt het kader een strengere evaluatie die een overschatting van modelcapaciteiten voorkomt.

De auteurs positioneren VeriScale als complementair aan bestaande inspanningen; in plaats van nieuwe taken in te voeren, versterkt het bestaande benchmarks door de kwaliteit en kwantiteit van testsignalen te schalen. Het werk onderstreept de noodzaak van adversariale testschaling om de fragiliteit van huidige modellen in formele redeneertaken bloot te leggen.

Erkende Beperkingen:
De auteurs merken op dat VeriScale afhankelijk is van de beschikbaarheid van grondwaarheid-precondities en referentie-implementaties. Bovendien wordt de kwaliteit van de gesynthetiseerde onverwachte uitvoer begrensd door de redeneercapaciteiten van de LLM die fungeert als "red team". Tot slot blijft de constructiefase rekenintensief, waarbij enorme LLM-steekproeven en Lean-uitvoeringen nodig zijn.

Toekomstig Werk:
De auteurs stellen voor VeriScale te laten evolueren tot een gesloten-lus reparatiesysteem om modellen te begeleiden bij het patchen van gebrekkige specificaties. Ze plannen ook om VeriScale te gebruiken als een adversariale data-engine om trainingscorpora te synthetiseren voor specifieke autoformalisatiemodellen en het kader te generaliseren naar andere verificatiebackends zoals Dafny.