Claude від Anthropic тепер пише код і автоматично доводить його безпеку

Anthropic використала Claude, щоб математично довести коректність наявного коду. Цей підхід розв’язує ключову проблему програмного забезпечення, створеного ШІ, але має суворі практичні обмеження.

Доведення того, що програмне забезпечення працює без помилок за будь-яких обставин, завжди було надто дорогим. Команді фахівців знадобилося 20 людино-років, щоб формально перевірити невелике ядро операційної системи seL4, тому цей метод застосовували лише в надзвичайно важливих випадках, як-от авіоніка Airbus.

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

Замість написання нового коду Claude перевіряв наявне програмне забезпечення, перетворюючи тести на випадки аварійного завершення на математичні задачі, аналізуючи скомпільований машинний код і створюючи розгорнуті докази. Незалежна програма верифікації під назвою Rocq автоматично перевіряє ці докази, і, за словами Anthropic, цей процес майже не потребує участі людей-рецензентів. Дослідники називають це «повністю автономною» генерацією доказів, хоча інструменти та формальні основи створили люди з Theorem.

Claude виявляє помилки, які роками не помічали тести

Під час створення доказів Claude натрапив на сотні помилок, і йому дозволили виправити їх самостійно. За словами дослідників, багато з них могли залишитися непоміченими під час традиційного тестування, оскільки проявляються лише за дуже специфічних умов, наприклад у разі незвично великих вхідних файлів або певної послідовності звернень.

Наприклад, під час перевірки широко використовуваної програми для читання PDF команда за один тиждень знайшла стільки ж помилок безпеки, скільки зазвичай виявляють у цьому програмному забезпеченні за цілий рік. В іншій програмі Claude виявив логічну помилку, яка залишалася непоміченою понад десятиліття. Навіть коли повний доказ зрештою не вдається створити, спроба все одно виявляє реальні помилки, зазначає Anthropic.

Що може і чого не може формальна верифікація

Anthropic визнає, що «формально перевірений» не означає «без помилок». Докази чинні лише за суворих умов: для конкретної архітектури процесора, однопотокових програм і вхідних даних обсягом до 64 МБ. На практиці ці бібліотеки працюють на різному обладнанні та в різних конфігураціях.

Обчислювальні витрати значні: на окремі докази витрачаються сотні мільйонів токенів. Anthropic не повідомляє загальну вартість проєкту. Але якщо ШІ може перевіряти власний код, розробники зможуть більше довіряти програмному забезпеченню, створеному ШІ, і витрачати менше часу на його перевірку. Це заощаджує кошти не лише на верифікації, а й на всьому процесі написання коду. Менший тестовий запуск також показав, що докази можна повторно використовувати, а нові моделі стають ефективнішими: Opus 5.5 розв’язує половину задач на доведення, використовуючи приблизно на 40 відсотків менше токенів, ніж Opus 5.

Проєкт посилює аргументи на користь автоматизації розробки програмного забезпечення. Якщо ШІ може писати код і гарантувати його коректність за визначених умов, питання зміщується від «Чи може ШІ програмувати?» до «Чи може ШІ довести, що написаний ним код безпечний?» Якщо відповідь ствердна, наслідки можуть вийти далеко за межі сучасних інструментів для написання коду.

Показовий приклад: Anthropic очікує, що формальна верифікація за допомогою ШІ незабаром стане такою ж практичною, як стандартне тестування, а дорожня карта Theorem вже передбачає критично важливу інфраструктуру, зокрема glibc, OpenSSL і cURL.

Новини про ШІ без зайвого галасу — відібрані людьми

Підпишіться на THE DECODER, щоб читати без реклами, отримувати щотижневу розсилку про ШІ, наш ексклюзивний звіт про передові технології «AI Radar» шість разів на рік, повний доступ до архіву та доступ до розділу коментарів.