Anthropic научила Claude доказывать безопасность кода в 123 библиотеках
Anthropic научила Claude доказывать безопасность кода в 123 библиотеках Anthropic совместно с Theorem показала, что языковые модели могут проводить формальную верификацию программного обеспечения в промышленном масштабе, а не только в единичных проектах уровня авиации. 🌍 Claude доказал безопасность 123 открытых библиотек на уровне ассемблера С помощью Claude в более чем 100 реальных открытых программных библиотеках доказаны свойства безопасности на уровне ассемблерного кода RISC-V. Для 123 библиотек Claude формально доказал, что исполняемые программы всегда завершаются штатно и не вызывают ошибок работы с памятью и нарушений проверок — при входных данных до 64 МБ и определённых допущениях об однопоточном исполнении и операционной системе Linux. Попутно, в процессе работы над доказательствами, Claude нашёл ошибки, которые не обнаруживались годами, несмотря на триллионы тестовых прогонов. Раньше формальная верификация требовала огромных трудозатрат: авторы приводят пример операционной системы seL4, реализация которой заняла два человеко-года, а формальное доказательство её корректности — двадцать человеко-лет. Из-за такой стоимости метод применялся только в критически важных системах, например в авиационном софте Airbus. Снижение стоимости доказательств благодаря LLM открывает этот подход разработчикам массового ПО, а партнёр Anthropic — компания Theorem — готова прогонять ту же методику для других open-source проектов и публикует инструмент (skill) для Claude, чтобы разработчики могли верифицировать свой код самостоятельно. Выигрывают разработчики критичного и инфраструктурного ПО — банков, госсистем, встроенных устройств, — для которых формальные гарантии раньше были недоступны по цене. Проигрывают поставщики традиционных средств тестирования и аудита безопасности, чья ценность снижается, если доказательства можно получать автоматически и дешевле. Для России прямое применение ограничено: доступ к Claude и западным инструментам верификации под вопросом из-за санкций, но сам факт удешевления формальной верификации — сигнал для разработчиков GigaChat, YandexGPT и других моделей, что стоит двигаться в ту же сторону. 💡 На пальцах: Программы, написанные с помощью таких инструментов, теоретически могут содержать меньше критичных ошибок памяти, что со временем снизит число взломов и сбоев в привычных сервисах. 🔗 anthropic.com Если удешевление формальной верификации подтвердится на практике, это станет куда более значимым сдвигом в безопасности софта, чем очередной рост баллов моделей в бенчмарках. #НейроНовости #Anthropic #безопасность #Claude