Google DeepMind доказала безопасность кода Signal с помощью ИИ-агентов

Отлично, какой прекрасный вариант использования ИИ. Мне кажется, Google был самым чистым из крупных игроков с точки зрения полезного вклада и контроля над своими ИИ-системами. Правда, этот новый агент для доказательств, похоже, не оспаривает спецификацию, а только реализацию, если я правильно понял.

Интересно, чем этот агент отличается от классического агента для кодинга; в итоге он, похоже, работает так же: итерируется по кодовой базе, попутно пишет код на Lean или Rocq и запускает его.

Я ожидаю, что очень скоро, возможно, в ближайшие два-три года, будет казаться безумием, что мы когда-либо запускали _хоть какой-то_ неверифицированный софт на наших системах, так же как сейчас кажется безумием, что мы использовали Telnet или HTTP в открытом виде.

В начале этого года я делал крупные рефакторинги старого проекта. В то время агенты для кодинга как раз набирали обороты, и им можно было всё больше доверять более автономную работу, так что я с воодушевлением решил попробовать.

Он выполнил рефакторинг, работая несколько часов, и в итоге сам предложил обширный набор тестов. Все тесты зелёные!

Я был очень впечатлён, пока не прищурился. Он реализовал всё наоборот, причём не только бессмысленно (не достиг ни одной из заявленных целей), но и фактически сделал хуже, чем было!

До этого момента я был довольно оптимистичен насчёт потенциала формальной верификации в эпоху ИИ. Но увидев этот бардак, я понял, что он с тем же успехом мог написать мне математическое доказательство для написанного им кода, и доказательство бы прошло, а код всё равно был бы неправильным!

Очень круто. Пару лет назад я размышлял о разработке специализированной модели для формальной верификации с использованием подхода вроде AlphaZero. Учитывая новости последних нескольких месяцев, я рад, что не стал этого делать: похоже, универсальные LLM действительно съедают всё.

Интересно, что в итоге у них получилось 26 тысяч строк спецификаций (включая семантику Arm). Это довольно большая доверенная вычислительная база. Полагаю, им пришлось разрабатывать символические/вычислительные модели с нуля. Будет интересно посмотреть, сможем ли мы создать переиспользуемые библиотеки таких моделей, в духе mathlib, и как там сложатся стимулы. Лабораториям ИИ это, вероятно, не особенно интересно, и, скорее всего, это неблагодарная работа для исследователей. Но, возможно, если появятся компании, занимающиеся верификацией или продажей верифицированных продуктов, у них может возникнуть стимул делиться работой и иметь стандартизированную TCB. Это, к лучшему или к худшему, может также положить практический конец «войнам интерактивных средств доказательства теорем».

Также интересно, как это отразится на коде в разработке. ChatGPT утверждает, что на следующий день после релиза libsignal существенно изменился :D Возможно, помогла бы промежуточная недоверенная модель на Rust (где большая часть доказательства связывает модель на Rust со спецификацией, а затем более механическое доказательство связывает модель на Rust с бинарником); seL4 сделал это давным-давно. Но я понятия не имею, практично ли это, я не слышал ни о чём […]

Я экспериментировал с тем, насколько легко ИИ пишет на Lean (https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...), и вот несколько уроков:

1. ИИ на Lean не идеален, и ИИ может легко схитрить, раз уж он пишет этот Lean. Всем, кто играется с кодом на Lean от ИИ, как минимум нужен ещё один состязательный промпт для проверки сгенерированного ИИ Lean.

2. Копаясь в статье, я вижу, что они действительно заново внедрили некоторые баги, чтобы проверить, что система их поймает, но, похоже, сами багов не нашли. Может, Signal просто потрясающий, раз его просматривает столько глаз, но настоящая история для остальных из нас в том, что если вы начнёте с помощью ИИ переводить код в Lean, ценность будет в том, какие допущения он обнаружит. Даже для вещей, которые я считал логически очень строгими, Lean нашёл несколько мелочей, которые мне пришлось исправить. По аналогии с фаззингом, где я ни разу не вносил фаззинг в кодовую базу и не находил багов, я ожидаю того же от перевода спецификаций в Lean.

3. Возможность (дёшево) генерировать Lean с помощью ИИ — это очень интересный ключ к кодингу. Потенциально возможность переходить от спецификации к Lean и к коду, используя Lean как логического привратника, может стать реальной возможностью, которая будет использоваться всё чаще и не только в исследованиях.

Вопрос новичка: помимо этих криптографических систем, было бы полезно строить такие доказательства для обычных кусков программного обеспечения? Конкретно:

1. Применял ли кто-нибудь это к программным системам, где ИИ-агент находится на критическом пути в продакшене, то есть где возможно недетерминированное действие (пусть и с восстановлением)?

2. В каких сценариях имеет смысл иметь доказательство на Lean с самого начала? Например, я представляю, что если вы хотите сделать систему баз данных с какими-то гарантиями вокруг ACID, то, возможно, лучше иметь это с самого начала. Но, вероятно, это не так полезно для создания сервиса с API.

Здорово. Помню, в прошлом году я думал, что софт вот-вот станет намного более багованным, раз люди всё больше перекладывают на ИИ, но такие инструменты дают мне надежду, что будущее программного обеспечения на самом деле выглядит гораздо более безопасным.