Anthropic nechal Claude dokazovat, že vybrané testy knihoven nespadnou
Claude podle Anthropicu vytvořil matematické důkazy pro 239 vstupních bodů ve 123 knihovnách. Výsledek platí pro konkrétní sestavení a omezené vstupy, nikoli pro veškerý kód těchto knihoven.
Anthropic ve výzkumu zveřejněném 22. října popsal, jak nechal Claude vytvářet matematické důkazy o chování skutečného softwaru. Ve spolupráci s firmou Theorem podle svého oznámení ověřil 239 vstupních bodů ve 123 knihovnách z projektu OSS-Fuzz. Úspěšné důkazy mají dohromady přibližně 180 milionů řádků. Nejde o počet řádků opravených programů ani o potvrzení, že jsou celé knihovny bez chyb.
Zkoušení vstupů vystřídal důkaz
OSS-Fuzz od Googlu hledá chyby tak, že programům opakovaně předkládá generované vstupy. Sleduje přitom například přístupy mimo vyhrazenou paměť. Takzvaný fuzz test má vstupní bod: kus programu, který data převezme a zavolá zkoušenou knihovnu. Ani velké množství pokusů nezaručí, že se otestovaly všechny možné vstupy.
Anthropic vzal existující testy a jejich požadavky převedl na matematická tvrzení o přeloženém programu. Claude pak hledal důkaz, že požadavky platí pro každý vstup ve stanovených mezích. Hotový důkaz kontroluje program Rocq. Model tedy sám nerozhoduje, zda jeho odpověď obstála.
Kontrola se týká strojových instrukcí pro procesory RISC-V, tedy podoby programu, kterou vykonává procesor. Odpadají tím možné rozdíly mezi zdrojovým kódem a jeho překladem. Zůstává ovšem nutnost správně popsat samotný procesor i operační systém, jinak se matematický důkaz vztahuje k chybnému modelu počítače.
123 knihoven neznamená 123 úplných prověrek
Podmínky jsou úzké. Výzkum počítá s jednovláknovým programem pro Linux a RISC-V, s pevně stanoveným rozpočtem paměti a se statickým sestavením, které má potřebné knihovny připojené už při překladu. Vstupy mají být menší než 64 MiB, jak limit upřesňuje příloha výzkumu. Hlavní text používá označení 64 MB.
Rozhoduje také to, kterou cestou test do knihovny vstoupí. Anthropic neověřoval všechny vstupní body každé knihovny. Ani jejich úplné pokrytí by podle firmy samo nezaručilo bezpečnost veškerého kódu nebo správné použití knihovny jiným programem.
Při dokazování Claude podle výzkumníků objevil stovky chyb a mohl je rovnou opravovat. Poté vzniklo nové tvrzení o opraveném programu a dokazování pokračovalo. Právě tady je další podmínka: oprava nesmí pouze odstranit potřebnou funkci, aby test přestal padat. Anthropic uvádí, že úpravy kontroloval a model za každou změnu kódu penalizoval.
Veřejná sada obsahuje 60 vstupních bodů
V zveřejněném repozitáři Theoremu je k 23. říjnu uvedeno 60 vstupních bodů ve 25 knihovnách. Anthropic slíbil zveřejnit jen podmnožinu důkazů, a to u testů, které nevyžadovaly opravu. Rozsah veřejné sady se proto nesmí zaměnit s celkovým výsledkem uvedeným v oznámení.
Dokumentace repozitáře také výslovně varuje, že důkazy nevylučují všechny chyby. Nesprávný výsledek nebo únik paměti může zůstat mimo vlastnosti, které kontrolní nástroje zachytí. Zveřejněné důkazy navíc nevylučují běh, který nikdy neskončí. Bez pádu tedy neznamená dokončený úkol.
Zopakování samotné kontroly není zadarmo. Theorem pro kontrolu jednoho důkazu na 16 jádrech uvádí spotřebu až 20 GiB operační paměti. Důkazy jsme sami neověřovali; počty i výsledek experimentu jsou údaje jeho autorů.
Člověku zůstává zadání toho, co se dokazuje
Výzkumník Martin Kleppmann z Cambridgeské univerzity už v prosinci 2025 vysvětloval, proč se psaní důkazů hodí pro jazykové modely: chybný důkaz odmítne samostatný kontrolní program a agent musí pokračovat. Současně upozornil, že člověk stále musí poznat, zda dokázaná vlastnost odpovídá tomu, co od programu skutečně potřebuje. Jeho text předchází nynějšímu experimentu, není jeho nezávislým přeměřením.
Otevřená zůstává cena vytváření důkazů. Anthropic píše, že jednotlivé úlohy mohou spotřebovat stovky milionů tokenů, tedy jednotek textu zpracovaných modelem. Celkový účet projektu neuvádí. Bez něj zatím nelze spočítat, pro které běžné programy se taková kontrola vyplatí.