Az Anthropic közzétette Claude szoftverbizonyításainak egy részét

Az Anthropic október 22-i közlése olyan folyamatot mutat be, amely egy könyvtárat és meglévő fuzztesztjét RISC-V gépi kódra fordítja. A fuzzteszt itt egy generált bemenetek vizsgálatára szolgáló belépési pont a programban. A futtatható állomány, az utasítások és a Linux formális modellje, valamint az elvárt összeomlásmentesség együtt határozza meg a matematikai specifikációt. Claude megírja a bizonyítást, majd a Rocq ellenőrzőmagja összeveti azt ezzel a specifikációval.

A nyilvános bizonyítástár pontosítja a határokat: a bizonyítások konkrét lefordított állományokra és egy teszt belépési pontjából elérhető kódra vonatkoznak, rögzített bemeneti és memóriafeltételekkel. Nem igazolják a teljes könyvtár helyességét, nem zárják ki az ellenőrzések által fel nem ismert hibás eredményeket vagy memóriaszivárgásokat, és nem érvényesek az x86-ra fordított változatokra. Ebben a kiadásban egyik bizonyítás sem zárja ki, hogy egy futás soha ne fejeződjön be. A dokumentált ellenőrzőprogram ellenőrzi az állományok hashét, előállítja az állításokat, lefordítja a bizonyításokat, és elutasítja az engedélyezett listán kívüli feltevéseket.

A mögöttes Linux-folyamatmodell azt is tisztázza, mit jelenthet a programok viselkedésének összehasonlítása. Megkülönbözteti a kimeneti bájtokat, azok sorrendjét, a kilépési állapotot és a fájlok végső tartalmát, de nem figyeli a futási időt vagy az utasítások számát. Az eredménynek meg kell neveznie a ténylegesen bizonyított állítást; a megfigyelhető viselkedés egyezése önmagában nem igazolja a futás befejeződését. A modell továbbra is hiányos, és nem ellenőrzött feltevésekre támaszkodik, ezért szerzői az érvényességi kört leíró dokumentum elolvasását kérik, mielőtt valaki egy bizonyítást valódi programra vonatkozó bizonyítékként használna.

A projektről és gyakorlati korlátairól Matthias Bastian számolt be október 23-án a The Decoderben.