Claude доказал безопасность кода в 123 open-source библиотеках — и нашёл баги, которые не ловили триллионы тестов
LLMs are making formal software verification feasible at a much larger scale
Anthropic совместно с Theorem показала, что LLM способны автономно писать формальные доказательства корректности на уровне ассемблера RISC-V. Claude доказал отсутствие падений при любом вводе до 64 МБ для 239 точек входа в 123 библиотеках OSS-Fuzz, попутно обнаружив и исправив сотни давних багов, включая ошибки, которые фаззеры не могли найти из-за ограничений на размер входных данных. Это первый масштабный опыт применения ИИ для формальной верификации production-кода.
Claude успешно исправил найденные баги, а затем доказал, что падений не будет ни при каком вводе (до 64 МБ) для 239 точек входа в 123 различных библиотеках OSS-Fuzz.
- yazaddaruvala
Думаю, на самом деле произойдёт нечто противоположное. LLM не будут формально верифицировать императивный код, сгенерированный LLM. Мы (включая агентную разработку) уйдём от императивных языков, минуя функциональные, и перейдём к детерминированным декларативным языкам.
Вероятно, произойдёт всплеск экспериментальных языков, чем-то похожих на Typescript для SQL, но со значительно более нюансированными операторами, позволяющими лаконично выражать те же результаты, что и императивные языки.
Они будут компилироваться так, чтобы работать производительно для разработки игр или даже для ядра Linux (как будто Линус когда-нибудь согласится, лол), но также смогут выполняться на движках распределённого выполнения с фактически общим адресным пространством и т.д.
Это позволит создавать значительно более лаконичные артефакты. Меньше вероятность галлюцинаций, меньше выходных токенов, меньше итераций циклов рассуждения и достаточно кратко для проверки человеком (в тех областях, где это нужно).
Вдобавок ко всему, дополнительный синтаксис вроде теорем, чтобы резко ограничить возможности функций и т.п., вероятно, какая-то система эффектов более высокого уровня для верификации. Используется для многого, например, «компиляция с постоянным временем для криптографических функций», а также «обеспечение соответствия ACID» для записей и чтений в локальном контексте, и такое как «обеспечение доставки ровно один раз» для функций на движке распределённого выполнения.
В этот момент каждая программа будет формально верифицирована по умолчанию. Можно думать об этом как о AdaErlangSQL+++
- jaykru
Из приложения [0]: «Доказательства, написанные агентами, так же „хороши“, как и любое другое доказательство той же теоремы, в том смысле, что они доказывают теорему эквивалентности. Однако остаётся вопрос, смогут ли агенты масштабировать этот многословный стиль доказательств непосредственно на более сложные программы. Опыт других проектов агентной верификации, таких как MachCSL, позволяет предположить, что ответ может быть отрицательным: агенты упираются в стену сложности с многословным стилем доказательств, и для масштабирования требуется, чтобы доказательства были структурированы вокруг лучших модульных абстракций и принципов рассуждения. Если это так, как мы можем помочь агентам обнаруживать и вводить правильные абстракции, чтобы уменьшить эту сложность? Требуется ли для этого участие экспертов по инженерии доказательств, или мы можем извлечь общие принципы, которые будут направлять агентов к обнаружению хороших абстракций, позволяющих масштабировать доказательства?»
Некоторые математики заметили похожую закономерность в недавних прорывах LLM в доказательствах, что побудило их предположить, что LLM упрутся в стену в математических способностях чуть за пределами выпуклой оболочки человеческой математики. Доказательства, выполняемые в формальной верификации, являются довольно интересным лакмусовым тестом для рассуждений LLM, поскольку рассматриваемые системы не обязательно находятся в распределении (сравните с математикой, где «системы» и структуры, с которыми работают, и доказательства о них, появляются в тысячах отдельных книг), так что преимущества в широких предметных знаниях, которые предобученные LLM имеют перед людьми, на самом деле мало что дают. ИМХО, это наблюдение […]
- malisper
Для скептиков: у меня был приличный успех в использовании формальной верификации для моего переписывания Postgres на Rust. Я написал компилятор, который может переводить код как на Rust, так и на C в Lean. Как только эти две функции оказываются в Lean, я заставляю LLM написать доказательство на Lean о том, что они ведут себя одинаково.
На данный момент я доказал, что около 12% кода ведёт себя одинаково при однопоточном выполнении. Это примерно 70 тысяч строк кода на C. Это выявило очень незначительные различия в поведении, например, как операции с плавающей запятой на разных платформах могут давать разные результаты.
Я работаю над тем, как масштабировать это, но не вижу никаких фундаментальных ограничений, которые помешали бы масштабировать это дальше.
- fedupnow
Мне 35, и мне конец, если они добьются своего. Я не пойду в рабочие специальности, я ушёл из строительства в 27, потому что слишком любил программирование. Я хотел покончить с собой практически каждый день, работая в строительной отрасли. Я пропил свои двадцать лет, потому что это было настолько отстойно. Я уже несколько лет трезв исключительно благодаря программированию и тому, что мне действительно нравится то, что я делаю. Но эта компания крадёт это у меня, многими разными способами.
Я вложил кучу своей жизни и все свои сбережения в этот переход. Теперь мне каждый день орут, чтобы я шёл в электрики, потому что Anthropic заявляет, что они собираются решить проблему остановки каким-то окольным путём, им даже не нужно делать то, что они заявляют. Им достаточно убедить 20% отрасли, что они это сделают, и такие парни, как я, никогда не получат шанса проработать достаточно долго, чтобы выйти на пенсию.
Я действительно не думаю, что у них получится, но если получится, я буду бездомным, программируя из публичной библиотеки, потому что я не собираюсь начинать всё заново.
- sestep
Занимаюсь этим на работе последние пару недель. Чрезвычайно мощно иметь возможность заставить агента открыть PR с некоторыми экспериментами, показывающими, что он делает какую-то функцию быстрее с помощью SIMD или CUDA, и просто уверенно смержить его, потому что в PR есть доказательство на Rocq, что поведение эквивалентно исходной реализации.
- pinevale
Формальная верификация относительно чего?
Неуловимой формальной спецификации со 100% покрытием, которая охватывает каждый предполагаемый и непредполагаемый вход, интересы каждого заинтересованного лица и каждое возможное поведение пользователя? В эпоху вайбкодинга? Нет, страница имеет достоинство признать, что этого не существует.
В конце концов, они останавливаются на поиске падений с помощью обычного фаззера, исправлении падений и затем... написании формального доказательства, что падение исправлено? Это кажется... довольно бессмысленным? Я что-то упускаю?
- Olscore
Строительство дома имеет три слоя:
1. Видение: что мы хотим (наше намерение)
2. Чертёж: спецификация, которую мы написали (наш дизайн)
3. Инспекция: проверка того, что мы построили, на соответствие чертежу (доказательства)
Это исследование делает инспекцию почти идеальной. Но инспекция проверяет только чертёж, а не наше видение, поэтому дом, построенный по неправильному чертежу, всё равно может пройти идеальную инспекцию. Другая половина — это убедиться, что чертёж соответствует нашему намерению и остаётся таким, пока агенты строят. Я работаю над этим, так что думаю, это дополняет:
- passive
Это казалось весьма вероятным, но поскольку наше внедрение LLM в разработку программного обеспечения до сих пор в основном сводилось к отказу от лучших практик, я скептически отношусь к тому, что это приведёт нас к расширенной верификации.
Это как Безос, рассуждающий о том, как у нас будет трёхдневная рабочая неделя, в то время как он заставляет своих сотрудников писать в бутылку.