Hillel Wayne: KI gjør ikke formell verifikasjon til allemannseie

«KI som løfter formell verifikasjon fra kanskje 0,1 til 0,3 prosent på tvers av bransjen ville fortsatt vært enormt» — Hillel Wayne, konsulent og forfatter innen formelle metoder

Wayne sier dette i en samtale med The Pragmatic Engineer, og går rett imot en utbredt antakelse: at når maskiner skriver mesteparten av koden, må matematisk bevis for korrekthet overta jobben testing gjør i dag. Hans egen observasjon peker motsatt vei. De som faktisk lykkes med å få en språkmodell til å generere formelle spesifikasjoner, er som regel folk som allerede er eksperter på formell verifikasjon.

Flaskehalsen er ikke verktøyet, men spesifikasjonen. Wayne bruker et bevisst kjedelig eksempel: finn fila i en katalog som har flest linjer. Skal du modellere det formelt, må du svare på om linjeskift telles som ASCII eller UTF-8, hva som skjer med uleselige filer, og hvordan symlinker håndteres. Uten formelle metoder skriver du en enkel sjekk som er riktig i over 99 prosent av tilfellene. Med dem betaler du full pris for den siste prosenten.

Der metodene faktisk lønner seg, er i systemer med feil som er nær umulige å finne på andre måter. I AWS sin gjennomgang av egen TLA+-bruk var det korteste feilsporet som viste én bestemt bug 35 steg langt, og buggen hadde allerede passert både designgjennomgang, kodegjennomgang og testing. Kappløpsituasjoner hører til samme kategori: i vanlig kode oppdager du dem måneder senere, om noen gang, mens en TLA+-modell melder fra med det samme.

Waynes anbefaling til de fleste er derfor ikke TLA+, men property-based testing: definer egenskapene koden skal oppfylle, og la testverktøyet kaste tusenvis av input mot dem. Det er den lette varianten av formelle metoder, og den eneste han mener er verdt å innføre bredt. Produserer agenten din mer kode enn du rekker å lese, er det der gevinsten ligger, ikke i beviset.