A Claude 180 millió sornyi bizonyítással ellenőrzött nyílt forráskódú programokat
Az Anthropic Claude modellje a Theorem szakértőivel együttműködve mintegy 180 millió sornyi matematikai bizonyítást készített 123, nyílt forráskódú könyvtárhoz. A projekt a Google OSS-Fuzz biztonsági programjának tesztjeire épült, és nem új szoftver írására irányult: Claude a meglévő programokat vizsgálta, a hibákat jelző összeomlási teszteket matematikai feladatokká alakította, majd a lefordított gépi kód helyességét próbálta igazolni. A bizonyításokat a Rocq nevű, független ellenőrzőprogram vizsgálta meg.
A folyamat során a modell több száz olyan hibát talált, amelyeket a hagyományos tesztelés évek alatt sem feltétlenül fedezett volna fel. Ezek csak különleges körülmények között jelentkeztek, például szokatlanul nagy bemeneteknél vagy bizonyos memória-hozzáférési sorrendekben, és Claude több hibát maga is kijavított. Egy széles körben használt PDF-olvasó ellenőrzésekor egy hét alatt annyi biztonsági problémára derült fény, amennyit abból a programból általában egy év alatt jelentenek. Egy másik alkalmazásban több mint tíz évig rejtve maradt logikai hibát azonosítottak.
A „formálisan ellenőrzött” azonban nem jelent feltétel nélküli hibamentességet. A bizonyítások egy meghatározott processzorarchitektúrára, egyszálú működésre és legfeljebb 64 megabájtos bemenetekre vonatkoztak. A számításigény is jelentős: egyes bizonyítások több százmillió tokent igényeltek. Anthropic szerint az irány mégis elvezethet oda, hogy az AI-val támogatott formális ellenőrzés a szokásos teszteléshez hasonlóan mindennapossá váljon, a következő célpontok között pedig a glibc, az OpenSSL és a cURL szerepel.
Folytasd az appban — szavazz és szólj hozzá ➔