Technische Samenvatting: Verus-SpecGym

Probleemstelling

Hoewel AI-coderingsagenten steeds bekwaamer worden in het genereren van geverifieerde code (code vergezeld van machine-gecontroleerde bewijzen), blijft een fundamentele knelpunt bestaan: de trouw van de formele specificatie zelf. Geverifieerde codegeneratie garandeert dat code voldoet aan een gegeven formele specificatie, maar het garandeert niet dat de specificatie de informele intentie van de gebruiker accuraat vastlegt. Als een agent een specificatie genereert die te zwak is, kan het incorrecte code certificeren; als deze te sterk is, kan het correcte code afwijzen.

Het artikel behandelt specificatie-autoformalisatie: de taak om informele programmeerproblemen (beschrijvingen in natuurlijke taal) te vertalen naar trouwe formele specificaties. De kernuitdaging is evaluatie. Bestaande methoden vertrouwen op dure, door experts geschreven referentiespecificaties of benaderende LLM-rechters, die beiden moeite hebben om subtiele semantische fouten te detecteren of effectief te schalen. Er is behoefte aan een schaalbaar, deterministisch evaluatiemechanisme dat kan verifiëren of een gegenereerde specificatie precies de geldige invoer en correcte uitvoer accepteert die door het informele probleem zijn gedefinieerd.

Methodologie

1. De Benchmark: VERUS-SPECBENCH

De auteurs introduceren VERUS-SPECBENCH, een benchmark bestaande uit 581 specificatie-schrijftaken die zijn afgeleid van Codeforces-programmeerproblemen. Deze problemen zijn geselecteerd om gericht te zijn op Verus, een verificatiekader voor Rust.

• Taakstructuur: Elke taak voorziet een agent van een informele probleemstelling, een formele Verus-skelet (dat invoer-/uitvoertypen en lege pre_spec- en post_spec-functies definieert), voorbeeldtestgevallen en documentatie.
• Gegevensbronnen: De benchmark maakt gebruik van twee verschillende bronnen voor testgevallen:
  • Officiële Codeforces-tests: Voornamelijk gebruikt voor volledigheidstests (geldige invoer en correcte uitvoer).
  • Codeforces "Hacks": Adversariële invoer geschreven door menselijke concurrenten om incorrecte oplossingen te breken die de officiële tests hadden doorstaan. Deze zijn cruciaal voor soundness-tests (het identificeren van ongeldige invoer of incorrecte uitvoer die modellen ten onrechte zouden kunnen accepteren).

2. De Omgeving: VERUS-SPECGYM

De evaluatie vindt plaats in VERUS-SPECGYM, een agentieke omgeving waarin modellen interageren met Verus, een bash-shell en een bestandssysteem.

• Iteratieve verfijning: Agenten lezen het probleem, schrijven specificaties en verfijnen deze iteratief op basis van feedback van een aangepast evaluatiecommando (verus_gym_specgen_check).
• Uitvoerbare specificaties: Een belangrijke technische innovatie is de uitbreiding van Verus's exec_spec-mechanisme. Verus-specificaties zijn doorgaans logische predikaten voor een stellingbewijzer en kunnen niet worden uitgevoerd op concrete invoer. De auteurs hebben exec_spec uitgebreid (met name door exec_spec_unverified! in te voeren) om gegenereerde specificaties te compileren naar uitvoerbare Rust-code. Dit stelt het systeem in staat om de specificatie uit te voeren tegen concrete testgevallen om op deterministische wijze acceptatie of afwijzing te bepalen.

3. Evaluatiekader

De evaluatie decomposeert trouw in vier categorieën van testgevallen:

1. Pre-volledigheid: Geldige invoer moet worden geaccepteerd door pre_spec.
2. Pre-soundness: Ongeldige invoer moet worden afgewezen door pre_spec.
3. Post-volledigheid: Correcte (invoer, uitvoer)-paren moeten worden geaccepteerd door post_spec.
4. Post-soundness: Incorrecte (invoer, uitvoer)-paren moeten worden afgewezen door post_spec.

De evaluator maakt gebruik van een tweeledige resolutiestrategie:

• Symbolische check: Poging om het gedrag van de specificatie te bewijzen met de SMT-oplosser van Verus.
• Uitvoerbare fallback: Als het symbolische bewijs inconclusief is, wordt de specificatie gecompileerd naar uitvoerbare Rust en uitgevoerd op het concrete testgeval. Dit zorgt ervoor dat zelfs complexe specificaties op deterministische wijze kunnen worden geëvalueerd.

Belangrijkste Bijdragen

1. VERUS-SPECGYM & VERUS-SPECBENCH: De eerste agentieke omgeving en benchmark die specifiek is ontworpen om specificatie-autoformalisatie te evalueren met behulp van uitvoerbare specificaties en adversariële "hack"-testgevallen.
2. Evaluatie voor uitvoerbare specificaties: Een nieuwe uitbreiding van Verus's exec_spec-mechanisme die deterministische tests van specificatietrouw mogelijk maakt zonder dat er door experts geschreven referentiespecificaties nodig zijn of dat uitsluitend wordt vertrouwd op LLM-rechters.
3. Adversariële evaluatiesuite: De constructie van een uitgebreide evaluatiesuite met behulp van door mensen geschreven Codeforces-hacks, wat aantoont dat deze adversariële invoer specificatiefouten blootlegt die officiële tests missen.
4. Empirische analyse van faalmodi: Een gedetailleerde analyse die aantoont dat zelfs frontiermodellen die in staat zijn tot het genereren van correcte code vaak falen in het schrijven van trouwe specificaties, waarbij fouten clusteren rond weggelaten invoeraannames, geaccepteerde incorrecte uitvoer en afgewezen geldige uitvoer.

Resultaten

De auteurs evalueerden zes frontier- en open-source-taalmodellen (waaronder gemini-3.1pro, gpt5.3-codex, opus4.6 en enkele open-source modellen) onder een vast reken- en tijdsbudget.

• Prestatiekloof: Het sterkste model, gemini-3.1pro, loste 77,8% van de taken op. Andere frontiermodellen losten tussen 51,1% en 57,8% op, terwijl open-source modellen slechts 21,5%–25,5% behaalden.
• Code versus specificatie: Op een subset van problemen waarbij gpt5.3-codex correcte uitvoerbare code kon genereren (81,8% succes), faalde het in veel gevallen om een trouwe specificatie voor hetzelfde probleem te schrijven. Dit geeft aan dat specificatie-autoformalisatie een apart knelpunt is dat losstaat van codegeneratie.
• Belang van soundness-tests: Evaluatie uitsluitend op volledigheidstests overschat de prestaties aanzienlijk. Het toevoegen van soundness-tests (afgeleid van hacks) zorgde ervoor dat de Pass@1 voor gpt5.3-codex daalde van 77,8% naar 58% en voor gemini-3.1pro van 82% naar 78%.
• Beperkingen van LLM als rechter: Bij het gebruik van een LLM als rechter om specificaties te evalueren, werden 26% van de fouten die door de uitvoerbare evaluator werden gedetecteerd, gemist. Dit suggereert dat uitvoerbare tests een betrouwbaarder signaal zijn voor de subtiele fouten die inherent zijn aan deze taak.
• Faalmodi: Kwalitatieve analyse onthulde drie terugkerende faalpatronen:
  1. Weggelaten invoeraannames: Ontbrekende globale structurele beloften (bijvoorbeeld het aannemen dat een oplossing bestaat wanneer dat niet het geval is).
  2. Geaccepteerde incorrecte uitvoer: Het niet afdwingen van optimaliteits- of correctheidsrestricties (bijvoorbeeld het accepteren van niet-mutueel ondeelbare paren).
  3. Afgewezen geldige uitvoer: Het schrijven van te complexe of restrictieve specificaties die correcte antwoorden afwijzen.

Betekenis en Claims

Het artikel beweert dat specificatie-autoformalisatie binnen bereik is voor frontieragenten maar breekbaar blijft, zelfs bij problemen waar ze succesvol correcte code kunnen genereren. Het werk toont aan dat:

• Het genereren van trouwe specificaties een apart vermogen is ten opzichte van codegeneratie.
• Uitvoerbare tests met behulp van adversariële invoer (hacks) essentieel zijn voor betrouwbare evaluatie, omdat ze randgevallen blootleggen die standaardtests en LLM-rechters missen.
• Huidige modellen moeite hebben met de nuance van het vertalen van informele intentie naar precieze logische predikaten, waarbij ze vaak falen in het vastleggen van impliciete restricties of optimaliteitscriteria.

De auteurs positioneren dit werk als een stap richting robuustere geverifieerde codegeneratie, met de nadruk dat het "knelpunt" is verschoven van het schrijven van code naar het schrijven van de juiste specificatie. Ze benadrukken dat hun aanpak een schaalbaar, deterministisch signaal voor trouw biedt zonder de prohibitieve kosten van door experts geschreven referentiespecificaties.