AI Radar
Anthropic применила Claude для проверки кода 123 open-source библиотек
Anthropic с помощью Claude сгенерировала около 180 млн строк доказательств для 123 open-source библиотек. При проверке существующего кода модель нашла ошибки, которые пропустили тесты.
Anthropic использовала Claude для генерации доказательств корректности существующего кода в 123 open-source библиотеках. В результате получилось около 180 млн строк кода доказательств. Формальная верификация проверяет, выполняются ли заданные свойства программы, с помощью математических доказательств; для этого свойства сначала нужно точно сформулировать.
В ходе работы модель обнаружила ошибки, которые раньше не выявили тесты. Anthropic хочет сделать формальную проверку с помощью AI столь же привычной частью разработки, как тестирование. Доступные сведения описывают масштаб эксперимента и найденные ошибки, но не уточняют, сколько доказательств прошло независимую проверку или сколько работы потребовалось для их сопровождения.
Почему это важно
Автоматическая генерация доказательств может расширить применение формальной верификации в open-source проектах. Найденные ошибки показывают, что такая проверка способна дополнить обычные тесты.
Мнение редакции
Мнение редакцииФормальные доказательства обычно требуют много ручной работы, поэтому такой масштаб эксперимента любопытен сам по себе. Следующий вопрос для практического применения – сколько усилий понадобится людям, чтобы проверять и поддерживать сгенерированные доказательства.
Первоисточники и подтверждения
Подборку проверяет редакция DSML. AI помогает дедуплицировать сигналы и готовить текст, но опубликованный выпуск остаётся редакционным продуктом, а не лентой отдельных каналов.