AI-агенты переписали CPython на Lean и нашли 418 багов в Python
Formalizing CPython
Агенты на основе Opus 5.5 построчно скопировали внутренности CPython на Lean, проверили каждую функцию на десятках тысяч входов против настоящего Python и доказали теоремы. Второй агент, не участвовавший в написании, проверял каждую работу. Итог: 613 318 строк Lean, 18 898 теорем и 4 071 принятая функция. Попутно доказательства вскрыли 418 багов, около 55 из которых могут уронить интерпретатор или повредить память обычным Python-кодом.
Самое сложное было не заставить AI-агентов писать доказательства, а получить доказательства, которые действительно что-то значат.
- debugnik
Не было бы продуктивнее потратить токены на добавление аннотаций ACSL для верификации CPython с помощью Frama-C? Вы бы верифицировали реальную среду выполнения, а не её ИИ-перевод, и исправления можно было бы напрямую отправлять в上游.
- anewhnaccount2
Тот же подход для стандартной библиотеки Julia: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- jakobnissen
Я считаю, что этот подход к поиску багов очень перспективен (очевидно — он находит кучу багов). Долгосрочная проблема в том, как такой поиск багов можно делать рутинно, например, как часть набора тестов. Подход, использованный этими людьми, тот же, что и у ребят из Julia, не очень-то автоматизируем, потому что требует много работы как людей, так и ИИ-агентов.
Полагаю, в долгосрочной перспективе это нужно встроить в язык, чтобы код и доказательства на Lean не расходились. То есть это могли бы быть опциональные свойства, записываемые вместе с кодом, которые затем проверяются в наборе тестов. Очень похоже на обычные проверки компилятора, только более выразительные и дорогие, и выполняемые только во время тестирования.
- tomtom1337
Я запутался в нескольких моментах, был бы признателен, если бы кто-нибудь помог разобраться!
- если переписывание на Lean происходит строка за строкой, как могут две реализации различаться в результате (Шаг 2)?
- как этот подход узнаёт «то, что всегда должно быть истинным» на Шаге 3 (это интеллект LLM «угадывает»?).
- erfgh
Кто-нибудь читает статьи, написанные ИИ? Это серьёзный вопрос.