AI-model Claude bewijst wiskundig dat bestaande software klopt

Bewijzen dat software onder alle omstandigheden foutloos draait, was tot nu toe extreem duur en tijdrovend. Voor het kleine besturingssysteem seL4 hadden specialisten twintig persoonsjaren nodig om dat soort formele verificatie uit te voeren. Daardoor bleef de techniek voorbehouden aan uitzonderlijke gevallen, zoals de besturingssoftware van vliegtuigbouwer Airbus. Het Frontier Red Team van Anthropic liet deze klus nu grotendeels overnemen door het AI-model Claude, in samenwerking met het bedrijf Theorem.

Van twintig persoonsjaren naar enkele weken

Claude kreeg geen nieuwe code te schrijven, maar ging aan de slag met bestaande software uit OSS-Fuzz, een beveiligingsproject van Google met testprogramma's voor 123 open-source bibliotheken. Het model vertaalde crashtests naar wiskundige problemen, analyseerde de gecompileerde machinecode en stelde uitgebreide bewijzen op. Een onafhankelijk controleprogramma genaamd Rocq checkte die bewijzen automatisch. Volgens Anthropic was daarbij nauwelijks menselijke controle nodig, al zijn de onderliggende tools en wiskundige basis wel door mensen bij Theorem gebouwd. In enkele weken tijd leverde Claude zo ongeveer 180 miljoen regels bewijscode op.

Bugs die jarenlang over het hoofd werden gezien

Tijdens het bewijzen stuitte Claude op honderden fouten in de software, die het model vervolgens zelf mocht herstellen. Veel van die bugs waren met gewoon testen nooit gevonden, omdat ze alleen optreden onder zeer specifieke omstandigheden, zoals een ongewoon groot bestand of een bijzondere volgorde van bewerkingen. Bij de controle van een veelgebruikte pdf-lezer vond het team in één week evenveel beveiligingsproblemen als normaal in een heel jaar worden gerapporteerd. In een andere toepassing ontdekte Claude een logische fout die al meer dan tien jaar onopgemerkt was gebleven. Zelfs als een volledig bewijs uiteindelijk niet lukt, levert de poging volgens Anthropic nog waardevolle bugmeldingen op.

Strikte grenzen aan wat het bewijs waard is

Anthropic benadrukt dat 'formeel bewezen' niet betekent dat software foutloos is. De bewijzen gelden alleen onder strikte voorwaarden: een specifieke processorarchitectuur, programma's die niet meerdere taken tegelijk uitvoeren, en invoerbestanden kleiner dan 64 megabyte. In de praktijk draaien deze bibliotheken op uiteenlopende hardware en in andere configuraties, waardoor het bewijs niet overal automatisch opgaat. Ook de rekenkosten zijn hoog: losse bewijzen kosten honderden miljoenen tokens, de rekeneenheden waarmee AI-taalmodellen tekst verwerken. Toch wordt het efficiënter: het nieuwere model Opus 5.5 lost de helft van de bewijzen op met ongeveer 40 procent minder tokens dan voorganger Opus 5. Theorem wil de aanpak nu uitbreiden naar kritieke software zoals de systeembibliotheek glibc, de beveiligingslaag OpenSSL en het dataprogramma cURL.