Hoe goed gebruiken agents test- en verificatietechnieken?

Methodologie

We maken gebruik van de Zstd-implementatie-evaluatie uit een eerdere vergelijking van de effectiviteit van agentic programmeertalen. In plaats van talen vergelijken we nu verschillende testtechnieken en testbibliotheken. De agents kregen de opdracht om Zstd te implementeren, aangevuld met specifieke instructies zoals "Gebruik test-driven development", "Gebruik Lean 4", "Gebruik QuickCheck" of "Gebruik property-based testing".

Alle implementaties werden uitgevoerd in Rust. De 26 geteste prompt-condities waren:

• ACL2, Alloy, "Audit and fuzz risky areas", "Audit first", Creusot.
• Default (geen aanvullende instructies).
• Differential testing, Fuzzing, Hegel, Insta, Judgement (agents gevraagd de beste techniek te kiezen).
• Kani, Lean 4, "Make no mistakes", Metamorphic testing, Mutation testing.
• Property-based testing, Proptest, QuickCheck, rstest.
• Rust built-in test framework, SMT solvers (met Z3, cvc5 en Yices), Spin, TDD, TLA+, en Verus.

Daarnaast werden vier 'skills' getest: de officiële Hegel-skill, de ECC Rust test skill, de Trail of Bits property test skill, en een eigen geschreven test-skill. De skills werden gekozen op basis van suggesties van Codex.

Voorspellingen

Vooraf aan het onderzoek zijn de volgende voorspellingen gedaan:

• TDD zal ondermaats presteren (55% vertrouwen): Specifiek toegevoegd omdat ik verwachtte dat het slecht zou werken.
• Formele methoden zullen niet overperformeren (52% vertrouwen): Formele methoden zijn effectief, maar bij eenvoudige problemen zouden ze niet significant beter moeten presteren dan goede testmethoden bij een gelijkwaardig competentieniveau.
• "Make no mistakes" zal niet beter presteren dan geen instructies (95% vertrouwen): Een bekende grap; als dit zou werken, zou het inmiddels opgemerkt zijn.
• De ECC test skill zal niet overperformeren (65% vertrouwen): Deze skill instrueert agents om TDD te gebruiken, wat naar verwachting resultaten verslechtert.
• De Hegel skill zal niet overperformeren (65% vertrouwen): De skill is erg groot en leest meer als een tutorial dan als instructies voor een agent.
• De Trail of Bits test skill zal niet overperformeren (55% vertrouwen): Bevat potentieel nuttige informatie, maar is ook vrij omvangrijk.

Algemene resultaten

Uit de resultaten (gebaseerd op GPT-5.6 Sol met 'medium' en 'xhigh' effort) blijkt dat niets extreem overperformeert. Opvallend is dat de Default-conditie (geen aanvullende instructies) ruim boven het gemiddelde scoort.

Bij de 'xhigh' instelling presteerden fuzzing en PBT (property-based testing) gemiddeld iets beter dan formele methoden. De door Codex aanbevolen skills presteerden ondermaats, terwijl een eenvoudige custom skill redelijk scoorde. TDD presteerde, zoals voorspeld, slecht.

Wanneer we kijken naar wat de agents daadwerkelijk deden, wordt duidelijk dat ze deze tools en technieken over het algemeen niet goed kunnen gebruiken. Agents zijn standaard slecht in testen. Wanneer ze worden gevraagd een specifieke techniek te gebruiken, gebeurt vaak het volgende:

1. Ze schrijven de tests die ze normaal zouden schrijven, maar plaatsen deze binnen het framework van de gevraagde techniek.
2. Ze passen een techniek oppervlakkig toe zonder de werkelijke waarde ervan te benutten.

Bij formele methoden bewezen ze vaak irrelevante eigenschappen; bij property-based testing vertrouwden ze op volledig willekeurige inputs die vaak leidden tot ongeldige gevallen of triviale checks. Dit patroon was consistent over verschillende problemen (Zstd, IMAP RFC, etc.).

Op 'xhigh' effort konden agents hun eigen tests meestal laten slagen, maar de tests zelf waren van slechte kwaliteit (bijvoorbeeld door vier identieke bitstreams te gebruiken voor een feature die vier verschillende streams vereist).

Reflectie op RL-omgevingen

Het is interessant waarom AI-labs geen RL-omgevingen (Reinforcement Learning) hebben gecreëerd om agents te leren hoe ze goed moeten testen. Aangezien agents al goed zijn geworden in runtime-optimalisatie, zou effectief testen in dezelfde klasse van problemen moeten vallen. Wellicht is de kennis over effectieve testtechnieken simpelweg niet wijdverspreid genoeg om dit te implementeren.

Analyse per conditie

De volgende secties beschrijven de resultaten per techniek, gesorteerd van slechtste naar beste correctheid (hoewel de exacte volgorde met voorzichtigheid moet worden geïnterpreteerd).

Verus

Verus gebruikt een SMT-solver om te bewijzen dat code overeenkomt met specificaties. Agents gebruikten Verus echter niet voor de eigenlijke code, maar voor abstracte redeneringen over Zstd. De bewijzen waren vaak oninteressant of vacuéus (bijv. $A \implies A$).

• Voorbeeld van een vacuëus bewijs:

``rust requires 0 < a <= window, 0 < b <= window, 0 < c <= window, ensures 0 < c <= window, 0 < a <= window, 0 < b <= window, `` De correctheid op 'xhigh' was acceptabel, maar dit kwam door traditionele Rust-tests, niet door Verus.

Alloy

Alloy is een bounded model checker. Agents vertrouwden hier ook op standaard Rust-tests en gebruikten Alloy oppervlakkig. In één geval vond Alloy een tegenvoorbeeld, maar dit was gebaseerd op een 8-bit overflow die in de praktijk niet mogelijk was (omdat er 64-bit usize werd gebruikt), waardoor de code onnodig complex werd zonder een echte bug te voorkomen.

Differential Testing

Hierbij worden dezelfde inputs aan meerdere implementaties gegeven om verschillen te vinden. Dit leverde zeer slechte resultaten op. Geen enkele agent maakte twee volledige, onafhankelijke implementaties. In plaats daarvan schreven ze vaak twee keer dezelfde (foutieve) code, waardoor de bug in beide versies aanwezig was en niet werd gedetecteerd.

Lean 4

Lean 4 is een interactieve theorem prover. Net als bij Verus beperkten agents zich tot eenvoudige rekenkundige bewijzen die de risicovolle delen van de code niet raakten.

QuickCheck

Agents gebruikten QuickCheck vooral voor eenvoudige "smoke tests". Ze gebruikten volledig willekeurige inputs, wat voor Zstd inefficiënt is omdat dit vaak direct leidt tot foutmeldingen/afwijzingen in plaats van diepere logische bugs.

TDD (Test-Driven Development)

TDD presteerde ondermaats. De prompt zorgde wel voor een verandering in gedrag: agents schreven meer tests vooraf en werkten iteratiever. Echter, ze schreven vaker tests die geen rekening hielden met complexe gevallen (bijv. identieke streams gebruiken in plaats van verschillende).

Yossi Kreinin suggereert dat TDD agents richting "black box testing" stuurt, wat minder effectief is voor complexe machinery dan "white box testing" (waarbij je de code kent en gericht test op zwakke punten).

Spin

Spin is een model checker. Het gebruik was oppervlakkig en had geen correlatie met het slagen van de verborgen tests.

Hegel

Hegel is een PBT-bibliotheek. Agents gebruikten het na het schrijven van normale tests en schreven slechts enkele simpele property-tests. De Hegel-skill verslechterde de correctheid en verhoogde de kosten aanzienlijk, omdat de skill-tekst erg groot is (20k+ tokens) en vaak opnieuw werd ingelezen.

ToB Skill

Slechts een deel van de agents opende de skill. Omdat de skill suggereerde dat er goedkeuring nodig was voor nieuwe dependencies (en dit autonome runs waren), werd de aanbevolen bibliotheek proptest vaak niet toegevoegd.

Rstest

Agents gebruikten Rstest technisch gezien wel, maar schreven er gewoon standaard unit tests in zonder de fixture-functionaliteiten van Rstest te benutten.

Rust Built-in Framework

Het expliciet vragen om het standaard framework te gebruiken leidde tot meer tests, maar niet tot een betere correctheid. Meer tests betekenden niet noodzakelijkerwijs een betere dekking van risicovolle scenario's.

Creusot

Net als bij Verus werd Creusot niet effectief gebruikt.

Mutation Testing

Agents deden in de praktijk geen mutation testing, maar voerden normale tests uit met enkele kleine wijzigingen die niet aan de definitie van mutation testing voldeden.

Judgement

Wanneer agents zelf mochten kiezen, kozen ze bijna altijd voor standaard Rust unit tests.

Fuzzing

Agents stuurden voornamelijk willekeurige bytes, wat leidde tot ongeldige inputs. In zeldzame gevallen (10/160) genereerden ze gestructureerde inputs, wat in de helft van die gevallen echte bugs vond. Dit suggereert dat agents het kunnen, maar niet doen zonder sterke sturing.

Insta

Snapshot testing werd nauwelijks gebruikt; agents schreven normale unit tests binnen het Insta-framework.

SMT Solvers

Agents gebruikten SMT-solvers (Z3, cvc5, Yices) vooral als een soort kladblok voor berekeningen, maar implementeerden daarna vaak alsnog de verkeerde code.

TLA+

TLA+ scoorde iets boven gemiddeld. Bijna alle agents maakten een state-machine model van Zstd, maar dit gebeurde vaak pas laat in het proces. Er is geen bewijs dat TLA+-modellering direct leidde tot correctere Rust-code.

Metamorphic Testing

Agents controleerden enkele redelijke eigenschappen, maar deze raakten niet de gebieden waar de meeste fouten zaten. Ze testten wat makkelijk was, niet wat risicovol was.

ECC Skill

De resultaten waren inconsistent. De skill instrueerde agents om red-green TDD te gebruiken, wat leidde tot veel kleine, niet-betekenisvolle tests en uiteindelijk tot een ondergemiddelde score wanneer de skill daadwerkelijk werd gebruikt.

Default

De Default-conditie scoorde boven gemiddeld. Het niet geven van instructies voorkwam dat agents tijd verspilden aan ineffectieve implementaties van complexe technieken.

Audit

Audit-instructies zorgden ervoor dat agents de code hercontroleerden. Hoewel ze vaak dezelfde fouten herhaalden in de audit, scoorde deze conditie op 'xhigh' het beste qua correctheid, maar tegen zeer hoge kosten.

Audit and Fuzz Risky Areas

Agents identificeerden de risicovolle gebieden (FSE, Huffman) correct, maar de uitvoering van de fuzzing was zwak (te willekeurig, focus op crashes in plaats van eigenschappen).

Make No Mistakes

Presteerde vergelijkbaar met Default; resultaten lijken toe te schrijven aan willekeurige variatie.

Kani

Kani had de beste dekking wat betreft daadwerkelijk gebruik op de code. In één geval vond Kani een non-triviale bug. De kosten waren echter hoog door het herhaaldelijk lezen van Kani-output.

ACL2

Veel runs liepen vast door geheugengebruik (OOM). De bewijzen die werden geleverd hadden weinig impact op de uiteindelijke correctheid.

Proptest & Property-based Testing

Beide condities scoorden boven gemiddeld. Hoewel de tests vaak niet optimaal waren, bood de 'shrinking' functionaliteit van Proptest (het vinden van de kleinste input die een fout veroorzaakt) echte waarde.

Custom Skill

De door de auteur geschreven skill behaalde de hoogste score. De skill bevatten instructies om:

1. Risicovolle gebieden te identificeren en checks te bedenken waar resultaten verschillen.
2. Onafhankelijke herberekeningen uit te voeren in een nieuwe context.
3. Gestructureerde random inputs te gebruiken in plaats van naïeve randomisatie.

Hoewel de score hoog was, werd de skill niet perfect uitgevoerd (bijv. de nieuwe context werd zelden gebruikt). Toch hielp het sturen weg van standaard-foutmodi.

Algemene conclusies

Ongeacht de bibliotheek of techniek, agents slagen er over het algemeen niet in om deze tools effectief in te zetten. Het simpelweg benoemen van een techniek leidt tot oppervlakkig gebruik. Wel is vastgesteld dat agents goed in staat zijn om te identificeren welke delen van de code risicovol zijn, maar ze weten niet hoe ze die risico's effectief moeten testen.

Hoe krijg je agents om goede tests te schrijven?

De ervaring is dat het opzetten van een redelijke teststructuur en het geven van lichte, iteratieve instructies werkt. Wanneer men "praat" met een agent en corrigeert op basis van output, kan de kwaliteit snel verbeteren. Het lijkt erop dat de kennis aanwezig is in het model, maar niet wordt geactiveerd door simpele prompts; er is specifieke priming of sturing nodig.

Nauwkeurigheid van de voorspellingen

Voorspelling	Resultaat
TDD zal ondermaats presteren	Correct
Formele methoden zullen niet overperformeren	Correct (omdat ze ineffectief werden gebruikt)
"Make no mistakes" presteert niet beter dan Default	Correct
ECC skill zal niet overperformeren	Correct
Hegel skill zal niet overperformeren	Correct
ToB skill zal niet overperformeren	Correct

Over 'Skills'

De geteste skills leken vaak geschreven als menselijke tutorials (uitleggen hoe iets werkt). Voor een model dat de kennis al bezit, is dit niet optimaal. Effectievere skills zouden zich moeten richten op het aanpassen van het gedrag van het model, in plaats van het aanleren van de techniek zelf.

Bijlagen

Agent-dwazigheden

Tijdens het onderzoek vertoonden agents grillig gedrag. In één geval startte een agent een Perl-proces voor een regex-zoekopdracht in een klein bestand (44kB), maar door een degenerate expressie liep dit proces meer dan twee uur door voordat het handmatig werd beëindigd.

Experimentele details (IMAP RFC)

Tests op de IMAP RFC bevestigden de resultaten van Zstd: agents gebruikten tools zoals TLA+ oppervlakkig. Ze modelleerden eenvoudige aspecten (zoals mailbox-mutaties) waar de Default-conditie al bijna 100% scoorde, maar negeerden complexe aspecten (zoals event queues) waar de meeste fouten ontstonden.