Anthropic julkaisi torstaina tutkimuksen, jonka mukaan suuret kielimallit tekevät formaalista ohjelmistojen todentamisesta ensimmäistä kertaa käytännöllistä laajassa mittakaavassa. Yhteistyössä Theorem-yhtiön kanssa Claude todisti turvaominaisuuksia 123 avoimen lähdekoodin kirjastolle suoraan käännetyn konekoodin tasolla. Anthropicin mukaan kyseessä on ensimmäinen laaja hanke, jossa tekoäly soveltaa formaalia todentamista tuotantokoodiin konekielen tasolla.
Taustalla on kasvava huoli. Kielimallit löytävät ja hyödyntävät ohjelmistovirheitä yhä taitavammin, ja Linux-ytimestäkin julkaistiin hiljattain yli tuhat haavoittuvuutta. Perinteinen testaus näyttää vain, että virheitä on, mutta ei koskaan sitä, ettei niitä ole. Formaali todentaminen lupaa juuri jälkimmäisen.
Todistusten kirjoittaminen paljasti samalla satoja virheitä, joista osa oli säilynyt huomaamatta vuosia. Anthropic julkaisee osan todistuksista kaikkien tarkistettaviksi ja uudelleenkäytettäviksi.
Miksi formaali todentaminen on ollut harvinaista
Formaalissa todentamisessa ohjelma muunnetaan matemaattiseksi malliksi. Sen jälkeen todistetaan, että malli noudattaa aina ennalta määriteltyjä sääntöjä, esimerkiksi ettei muistia koskaan lueta varatun alueen ulkopuolelta. Jos todistus ei onnistu, epäonnistumisen kohta osoittaa yleensä, missä vika piilee.
Menetelmä on vanha, mutta se on ollut äärimmäisen kallis. Todistukset ovat usein moninkertaisesti alkuperäistä koodia pidempiä, ja niiden laatiminen vaatii harvinaista erikoisosaamista. Anthropic muistuttaa, että seL4-käyttöjärjestelmäytimen toteuttaminen vei kaksi henkilötyövuotta mutta sen todentaminen kaksikymmentä.
Siksi menetelmää on käytetty lähinnä aidosti kriittisissä kohteissa, kuten lentokoneiden ohjausjärjestelmissä. Tavallisen avoimen lähdekoodin kirjaston todentamiseen ei ole löytynyt aikaa eikä rahaa. Anthropicin mukaan tämä yhtälö on nyt muuttumassa, koska kielimalli jaksaa käydä läpi miljoonia rivejä selkeästi määritellyn tavoitteen perässä.
Fuzz-testeistä matemaattisiksi väitteiksi
Suurin käytännön ongelma on määritellä, mitä "oikein toimiva" ohjelma edes tarkoittaa. Anthropic kiersi ongelman hyödyntämällä Googlen OSS-Fuzz-ohjelman valmiita sumutestejä eli fuzz-testejä. Niissä testityökalu syöttää ohjelmalle valtavan määrän satunnaisia ja muunneltuja syötteitä ja etsii kaatumisia.
Jokaisesta testistä tehtiin väite: ohjelma ei kaadu millään alle 64 megatavun syötteellä. Muistivirheet saatiin kiinni AddressSanitizer-työkalulla, joka kaataa ohjelman heti virheellisen muistiviittauksen kohdalla. Jos Claude todistaa väitteen, saman testin sumuttaminen ei voi enää koskaan löytää uutta kaatumista.
Muutaman viikon aikana Claude todisti 239 testin sisääntulopisteen kaatumattomuuden 123 kirjastossa. Todistuksia kertyi noin 180 miljoonaa riviä Rocq-todistuskieltä, ja tyypillinen todistus oli noin 600 000 riviä pitkä. Ne koskevat RISC-V-arkkitehtuurille käännettyjä binäärejä, joiden mediaanipituus on noin 18 000 konekäskyä.
Valtavaa todistusmäärää ei tarvitse lukea ihmisvoimin. Rocqin todistustarkistin varmistaa koneellisesti, että jokainen todistus pitää. Luotettavaksi jäävät vain RISC-V:n ja Linux-prosessien mallit, todistettujen väitteiden muotoilu sekä itse tarkistin.
Todistustyö paljasti vuosia piilossa olleita virheitä
Kun todistus ei mennyt läpi, syynä oli usein todellinen virhe. Claude sai korjata löytämänsä bugit itse, minkä jälkeen väite muodostettiin uudelleen korjatusta koodista ja todistus jatkui. Näin prosessi löysi satoja virheitä, joista monet olisivat jääneet sumutestaukselta todennäköisesti kokonaan huomaamatta.
Yhdessä purkukirjastossa laskurin alivuoto johti kirjoittamiseen muistialueen ulkopuolelle, mutta vain noin 20 megatavun syötteellä, jolla oli harvinainen rakenne. Kuvadekooderin virhe vaati 64 megatavun syötteen ja yli kaksi gigatavua muistia. Sumutestit käyttävät yleensä enintään megatavun syötteitä, joten tällaiset viat jäävät niiltä helposti löytymättä.
Lisäksi Claude löysi uudelleen libexpat-kirjaston tunnetun haavoittuvuuden ja havaitsi logiikkavirheitä, jotka eivät kaada ohjelmaa lainkaan. Yhdessä kirjastossa ominaisuus, jonka piti rajata ladattavia tiedostoja, ei aina toiminut. Anthropicin mukaan pelkkä todistusyritys tuottaa siis korjattavia löydöksiä, vaikka lopullinen todistus jäisi saavuttamatta.
Riskinä oli niin sanottu palkkiohuijaus: malli voisi muuttaa ohjelman sellaiseksi, ettei se kaadu koskaan, vaikka se ei enää tekisi mitään hyödyllistä. Anthropic rankaisi jokaisesta korjauksesta, antoi lisäpisteitä muutosten rajaamisesta ja tarkasti korjaukset jälkikäteen.
Zlib, Python-tulkki ja PDF-lukija
Sumutestit olivat vain yksi kokeiluista. Toisessa Claude kirjoitti zlib-pakkausformaatin määrittelevästä RFC 1950 -standardista muodollisen määritelmän ja todisti, että Linux-ytimen zlib-toteutus noudattaa sitä. Tällä kertaa todistus tehtiin x86-binäärille, jonka semantiikan Claude oli itse mallintanut.
Saman kokeen yhteydessä todennettiin puolen tusinaa muuta laajasti käytettyä kirjastoa. Niistä löytyi vain pieniä, ei hyödynnettäviä reunatapausvirheitä. Anthropicin johtopäätös on kaksijakoinen: hyvin testattu koodi on jo lähes täysin oikein, ja koko toteutuksen oikeellisuus on mahdollista todistaa olemassa olevasta koodista.
Kolmannessa kokeessa Claude kirjoitti Rustilla tulkin suurelle osalle Python-kieltä ja todisti Verus-työkalulla sen noudattavan CPythonin semantiikkaa. Kun tulkkia ajettiin 1,7 miljoonalla satunnaisella Python-ohjelmalla, se käyttäytyi 99,95 prosentissa tapauksista täsmälleen kuten CPython.
Laajasti käytetyn PDF-lukijan todentamisyritys tuotti viikossa yhtä monta tietoturvavirhettä kuin sovelluksesta tavallisesti raportoidaan vuodessa. Toisesta kriittisestä sovelluksesta löytyi yli kymmenen vuotta piilossa ollut logiikkavirhe.
Rajoitukset ja kustannukset
Anthropic korostaa, ettei todennettu tarkoita virheetöntä. Todistus osoittaa vain, että ohjelma täyttää määritelmän. Jos määritelmä tai koneen malli poikkeaa todellisuudesta, virheitä voi yhä olla. Tämän tutkimuksen todistukset koskevat yksisäikeisiä, staattisesti linkitettyjä RISC-V-binäärejä, kun taas useimmat ajavat samoja kirjastoja x86- tai ARM-koneilla glibc-kirjaston kanssa.
Myös kattavuus on rajattu. AddressSanitizer ei havaitse kaikkia muistivirheitä, kaikkia sisääntulopisteitä ei todennettu, eikä todistus estä kutsuvaa ohjelmaa käyttämästä kirjastoa väärin. Tutkijat pitävät näitä aukkoja kuitenkin tunnettuina ja rajattuina, mikä helpottaa jäljellä olevien virheiden etsimistä.
Suurin käytännön este on hinta, sillä yksittäinen todistus voi kuluttaa satoja miljoonia tokeneita. Anthropicin mittauksissa Claude Opus 5.5 ratkaisi puolet 36 testitehtävästä noin 40 prosenttia pienemmällä tokenimäärällä kuin Opus 5. Kun agentit saivat kopioida toistensa todistuksia yhteisestä työtilasta, tokeneita kului vielä 17 prosenttia vähemmän.
Todistusten uudelleenkäyttö on myös strateginen ajatus. Koska ohjelmistoriippuvuudet keskittyvät harvoihin kirjastoihin, kunkin kirjaston riittää todentaa kerran. Theorem on julkaissut tiekartan koko Nix-ekosysteemin todentamiseksi, glibc, OpenSSL ja cURL mukaan lukien, ja tarjoaa samaa työketjua muille avoimen lähdekoodin hankkeille.
Yhteenveto
Anthropicin ja Theoremin tutkimus siirtää formaalin todentamisen asiantuntijoiden erikoisalalta kohti tavallista ohjelmistokehitystä. Claude todisti muistiturvallisuuteen liittyviä ominaisuuksia 123 kirjastolle konekoodin tasolla ja löysi samalla virheitä, joita biljoonat testiajot eivät olleet paljastaneet.
Menetelmä on vielä kallis, ja sen oletukset ovat kapeat. Kehittäjille tutkimus antaa silti konkreettisen työkalun: Theorem julkaisi Claude-taidon, jolla omaa koodia voi alkaa todentaa, ja Anthropic kehottaa kokeilemaan uudelleen erityisesti niitä, joille menetelmä ei aiemmin toiminut heikommilla malleilla.