Anthropic застосувала Claude для автоматичної формальної верифікації відкритого коду
Головне за 30 секунд
- Claude згенерував приблизно 180 мільйонів рядків коду математичних доказів для 123 бібліотек відкритого коду проєкту Google OSS-Fuzz.
- Процес повністю автономно перевіряє програма Rocq, знаходячи дефекти, які не фіксувало традиційне тестування.
- Доведення безпеки має межі: діє для однопотокових програм, обмеження входу до 64 МБ та конкретної архітектури процесора.
- У майбутньому Theorem планує застосувати метод до важливих компонентів інфраструктури: glibc, OpenSSL і cURL.
Зміст
Що сталося
Команда Anthropic Frontier Red Team разом із партнером Theorem задіяла модель Claude для математичного підтвердження коректності наявного програмного забезпечення. За кілька тижнів система створила близько 180 мільйонів рядків математичних доказів для 123 відкритих бібліотек, використовуючи тестові програми з проєкту безпеки Google OSS-Fuzz.
Замість генерації нових програм Claude переводив тести на аварійне завершення у математичні задачі, аналізував скомпільований машинний код і формував доведення. Їх автоматично валідує незалежна програма Rocq, що майже усуває потребу в залученні інженерів до перевірки.
Під час роботи Claude виявив і самостійно виправив сотні багів. Зокрема, у популярному PDF-рідері за один тиждень було знайдено стільки вразливостей, скільки зазвичай документують за цілий рік, а в іншому продукті знайдено логічну помилку, яка залишалася непоміченою понад десятиліття.
Кого це стосується
Ця розробка стосується інженерів безпеки, мейнтейнерів відкритих бібліотек і компаній, що розробляють критичне програмне забезпечення. Досі математична верифікація вимагала значних ресурсів: наприклад, для перевірки ядра операційної системи seL4 знадобилося 20 людино-років спеціалістів, через що метод застосовували переважно для проєктів на зразок авіоніки Airbus.
У перспективі це торкнеться широкої цифрової екосистеми, оскільки команда Theorem уже додала до своїх планів аналіз базових системних бібліотек glibc, OpenSSL та cURL.
Що робити: практичний висновок
Наразі розробникам не потрібно терміново змінювати поточні пайплайни тестування чи відмовлятися від звичних методів забезпечення якості. Формальна верифікація за допомогою ШІ працює у жорстких межах: вона підтверджена лише для однопотокового коду, конкретної процесорної архітектури та розміру вхідних файлів до 64 МБ.
Командам розробки варто враховувати, що статус «математично верифіковано» за цієї технології ще не означає повної відсутності збоїв на іншому обладнанні чи за змінених конфігурацій. Стежте за розвитком таких рішень і зниженням витрат на обчислення: нова версія Opus 5.5 вже виконує половину доведень приблизно на 40 відсотків меншою кількістю токенів порівняно з Opus 5.
Чого поки не відомо
Компанія Anthropic не оприлюднила загальну вартість усього проєкту. Окремі доведення потребують сотень мільйонів токенів, тому точні комерційні розцінки та дата публічного релізу інструмента для сторонніх розробників залишаються невідомими.
