Claude automatycznie dowodzi poprawności kodu

Anthropic przeprowadził eksperyment, który może zmienić sposób, w jaki podchodzimy do bezpieczeństwa oprogramowania. Zespół Frontier Red Team we współpracy z firmą Theorem wykorzystał model Claude do matematycznego udowodnienia poprawności istniejącego kodu źródłowego. To odpowiedź na fundamentalny problem generowanego przez AI softwaru – jak upewnić się, że działa bezbłędnie w każdych warunkach?

Formalna weryfikacja od dekad pozostawała domeną najbardziej krytycznych systemów. Weryfikacja jądra systemu operacyjnego seL4 wymagała około 20 osobokat pracy specjalistów. Nic dziwnego, że metodę stosowano wyłącznie w ekstremalnych przypadkach – choćby w awionice Airbusa. Anthropic postanowił sprawdzić, czy Claude może przejąć tę żmudną pracę.

Jak Claude weryfikuje kod bez pisania nowego

Podejście badaczy różni się od typowego generowania kodu. Model nie tworzył nowych programów, lecz analizował istniejące oprogramowanie. Proces przebiegał w kilku etapach: Claude tłumaczył testy awaryjne na problemy matematyczne, analizował skompilowany kod maszynowy, a następnie generował obszerne dowody poprawności. Całość opierała się na programach testowych pochodzących ze 123 bibliotek open source w ramach projektu Google OSS-Fuzz.

Skala robi wrażenie – model wyprodukował około 180 milionów linii kodu dowodowego w ciągu zaledwie kilku tygodni. Niezależny program weryfikujący Rocq automatycznie sprawdza te dowody, a według Anthropic cały proces wymaga niemal zerowego udziału ludzkich recenzentów. Badacze określają to mianem „w pełni autonomicznego” generowania dowodów, choć narzędzia i podstawy formalne przygotowali ludzie z Theorem.

Błędy, które umknęły latom testów

Podczas generowania dowodów Claude natrafił na setki błędów i otrzymał zgodę na samodzielne ich naprawianie. Wiele z tych usterek przeszłoby przez konwencjonalne testy niezauważenie, ponieważ ujawniają się tylko w bardzo specyficznych warunkach – przy nietypowo dużych plikach wejściowych lub określonej sekwencji operacji.

Szczególnie wymowny jest przykład popularnego czytnika PDF. W ciągu tygodnia pracy nad jego weryfikacją zespół znalazł tyle błędów bezpieczeństwa, ile zwykle zgłasza się dla tego oprogramowania przez cały rok. W innym przypadku Claude wychwycił błąd logiczny, który pozostawał niezauważony przez ponad dekadę. Co istotne, nawet gdy kompletny dowód ostatecznie się nie udaje, sama próba i tak ujawnia rzeczywiste problemy.

Ograniczenia formalnej weryfikacji z pomocą AI

Anthropic uczciwie przyznaje, że „formalnie zweryfikowany” nie oznacza „wolny od błędów”. Dowody zachowują ważność tylko w ściśle określonych warunkach: konkretnej architekturze procesora, programach jednowątkowych i danych wejściowych poniżej 64 MB. W praktyce biblioteki działają na różnym sprzęcie i w odmiennych konfiguracjach, co wykracza poza zakres dowodu.

Koszty obliczeniowe również są wysokie – pojedyncze dowody zużywają setki milionów tokenów. Anthropic nie ujawnia łącznych kosztów projektu. Mniejszy test pokazał jednak, że dowody można wykorzystywać ponownie, a nowsze modele stają się efektywniejsze: Opus 5.5 rozwiązuje połowę dowodów zużywając około 40 procent mniej tokenów niż Opus 5.

Co to oznacza dla przyszłości automatyzacji programowania

Jeśli AI potrafi zweryfikować własny kod, programiści mogą bardziej ufać generowanemu oprogramowaniu i poświęcać mniej czasu na jego przegląd. Oszczędności dotyczą nie tylko samej weryfikacji, ale całego procesu tworzenia. Projekt wzmacnia argumenty za automatyzacją software’u – pytanie przesuwa się z „czy AI umie programować?” na „czy AI potrafi udowodnić, że napisany przez nią kod jest bezpieczny?”.

Anthropic przewiduje, że formalna weryfikacja z udziałem AI wkrótce stanie się równie praktyczna jak standardowe testowanie. Plan rozwoju Theorem obejmuje już krytyczną infrastrukturę – glibc, OpenSSL i cURL. Jeśli te zapowiedzi się potwierdzą, konsekwencje mogą wykroczyć daleko poza dzisiejsze narzędzia do kodowania.