Claude на Anthropic вече пише код и автоматично доказва безопасността му

Anthropic използва Claude, за да докаже математически, че съществуващият код е коректен. Подходът решава основен проблем при софтуера, генериран от изкуствен интелект, но има строги практически ограничения.

Доказването, че софтуерът работи без грешки при всякакви обстоятелства, винаги е било непосилно скъпо. Екип от специалисти е имал нужда от 20 човекогодини, за да провери формално малкото ядро на операционната система seL4, затова методът е бил запазен за изключителни случаи като авионичния софтуер на Airbus.

Frontier Red Team на Anthropic, работейки с партньора Theorem, вместо това възложи работата по доказателствата на Claude. Моделът създаде приблизително 180 милиона реда математически доказателствен код само за няколко седмици, използвайки тестови програми от 123 библиотеки с отворен код в проекта за сигурност OSS-Fuzz на Google.

Вместо да пише нов код, Claude провери съществуващия софтуер, като преведе тестовете за сривове в математически задачи, анализира компилирания машинен код и създаде обширни доказателства. Независима програма за верификация, наречена Rocq, автоматично проверява тези доказателства и според Anthropic процесът почти не се нуждае от човешки проверяващи. Изследователите го наричат „напълно автономно“ генериране на доказателства, макар че инструментите и формалните основи са създадени от хората в Theorem.

Claude открива грешки, пропускани от години тестване

Докато генерира доказателства, Claude се натъкна на стотици грешки и му беше позволено сам да ги поправи. Според изследователите много от тях биха останали незабелязани при конвенционално тестване, защото се проявяват само при много специфични условия, като необичайно големи входни файлове или определена последователност от достъпи.

По време на опит да провери широко използван PDF четец, например, екипът откри за една седмица толкова уязвимости в сигурността, колкото обикновено се съобщават за този софтуер за цяла година. В друго приложение Claude откри логическа грешка, останала незабелязана повече от десетилетие. Дори когато пълното доказателство в крайна сметка се провали, опитът все пак разкрива реални грешки, казва Anthropic.

Какво може и какво не може да направи формалната верификация

Anthropic признава, че „формално проверен“ не означава „без грешки“. Доказателствата са валидни само при строги условия: конкретна архитектура на процесора, еднонишкови програми и входове с размер под 64 MB. На практика тези библиотеки работят на различен хардуер и в различни конфигурации.

Изчислителната цена е висока, като отделните доказателства използват до стотици милиони токени. Anthropic не посочва общите разходи по проекта. Но ако изкуственият интелект може да проверява собствения си код, разработчиците могат да се доверяват повече на софтуера, генериран от изкуствен интелект, и да отделят по-малко време за прегледа му. Това спестява разходи не само за верификацията, но и за целия процес на програмиране. По-малък тестов цикъл също показа, че доказателствата могат да се използват повторно, а по-новите модели стават по-ефективни: Opus 5.5 решава половината от доказателствата с около 40 процента по-малко токени от Opus 5.

Проектът засилва аргументите в полза на автоматизацията на софтуера. Ако изкуственият интелект може да пише код и да гарантира неговата коректност при определени условия, въпросът се измества от „Може ли изкуственият интелект да програмира?“ към „Може ли изкуственият интелект да докаже, че кодът, който пише, е безопасен?“ Ако отговорът е „да“, последиците могат да надхвърлят значително днешните инструменти за програмиране.

Показателен пример: Anthropic очаква формалната верификация с изкуствен интелект скоро да стане толкова практична, колкото стандартното тестване, а пътната карта на Theorem вече е насочена към критична инфраструктура като glibc, OpenSSL и cURL.

Новини за изкуствения интелект без преувеличения – подбрани от хора

Абонирайте се за THE DECODER и получете четене без реклами, седмичен бюлетин за изкуствения интелект, нашия ексклузивен шест пъти годишно доклад за водещите разработки „AI Radar“, пълен достъп до архива и достъп до секцията за коментари.