Ложное «опровержение» гипотезы Коллатца обнажило баг в ядре Lean

Леонардо де Моура, сооснователь и главный архитектор Lean FRO, опубликовал постмортем по ошибке корректности (soundness bug) в ядре системы интерактивных доказательств Lean. История получилась поучительной: слабое место обнаружили не вручную, а с помощью искусственного интеллекта.

Что произошло

25 июля Рамана Кумар выложил репозиторий с формально «чистым» (без sorry) опровержением гипотезы Коллатца, построенным при участии ИИ. Разумеется, гипотезу никто не опроверг: «доказательство» эксплуатировало баг в обработке вложенных индуктивных типов. Через несколько дней Киран Гопинатан свёл его к короткому выводу False и завёл issue #14576. Исправление выкатили спустя час после сообщения об ошибке.

Суть дефекта: когда параметры вложенного индуктивного типа оказываются «фантомными» (не упоминаются в полях конструкторов), они исчезают из вспомогательного типа и выпадают из проверки. Подсунув в эту позицию некорректный по типам аргумент, можно было заставить ядро принять доказательство False.

Тонкость с независимым проверяющим

Самое любопытное — почему подделку не поймал nanoda, независимая реализация ядра Lean на Rust. Оказалось, что задействованы сразу два несвязанных бага в двух разных проверяющих. Официальное ядро не проверяло одно место, а nanoda — другое (имя типа в узле проекции). «Доказательство» было устроено так, что выражение, которое ядро вообще не смотрит, как раз проходило старую версию nanoda. Баг nanoda, что показательно, починили за неделю до этого. Кумар считает совпадение случайным, но не исключает, что модель видела отчёт об ошибке nanoda.

Практический вывод де Моуры: перекрёстная проверка независимым ядром по-прежнему работает — для обмана потребовались две отдельные ошибки в двух реализациях, — но пользоваться нужно свежими версиями обоих.

Про метапрограммирование

В обсуждении звучало предложение убрать или ограничить метапрограммирование, чтобы такую атаку нельзя было выразить. Де Моура называет это заблуждением: элаборатор по определению не является доверенным компонентом. Корректность не может держаться на том, что недоверенная часть откажется собрать плохой терм — злоумышленник и без того способен писать .olean-файлы напрямую или править память. Отвергать некорректные объявления обязано само ядро, в своём процессе.

Что дальше

Добавлены регрессионные тесты, а отдельный PR теперь проверяет, что параметры вложенного вхождения действительно ведут себя как параметры. Дэниел Селсам из OpenAI помог Lean FRO специализированным на кибербезопасности ИИ и нашёл в ядре ещё несколько программных ошибок — все исправлены, и все, к слову, ловились nanoda. Инструмент comparator.live теперь по умолчанию запускает nanoda и отслеживает его ежедневно.

Источник: Hacker News