dxdt.blog: занимательный интернет-журнал

Могут ли в программных системах проверки математических, формализованных доказательств быть ошибки? Конечно. Они там даже есть. И эти ошибки могут проявляться в том, что какие-то неверные цепочки “доказательств”, будут отмечены как верные.

Вероятность ошибки тем выше, чем больше формальных конструкций в доказательстве. Если код доказательства генерирует LLM, а в коде миллионы строк, то вероятность “эксплуатации ошибки” – выше. Почему “эксплуатации”? Потому что никто не сказал, что мощная LLM-система, использующая тот тамый программный парсер для проверки своих сегенерированных “формализаций”, не подберёт ошибку специально так, чтобы формальное доказательство сошлось к нужному результату. Вполне может и подобрать.

Должна ли такая ошибка в парсере вообще воспроизводиться системно? Не должна, но может. То есть, естественно, если у вас дефектный программный “парсер теорем”, но проявление дефекта в нём зависит, скажем, от схемы исчерпания свободного ОЗУ того компьютера, на котором запущен парсер, то выводы системы проверки будут плавающими и это все сразу заметят. Ну как – “все”: не то чтобы прямо “все”, но те, у кого есть вычислительные ресурсы для запуска проверки миллионов строк на гигабайтах ОЗУ. Но это другое дело. Главное, что дефект может быть системным, а это означает, что он строго воспроизводится, раз за разом выдавая одинаковый, но неверный вывод. Как проверить миллионы строк формализации вручную? Никак.

Понятно, что можно взять и написать другой парсер, который либо подтвердит вывод, либо обнаружит ошибку. На вход нового парсера подаётся тот же самый поток доказательств. В конце концов, формализация – это лишь набор текстовых файлов, можно попробовать проверить на компьютере, но разным проверяющим кодом. Такая схема тоже используется, пусть и с ограничениями. Для Lean, например, есть Nanoda. Код парсера даже может быть обозримым. Но только тут необходимо учитывать компилятор. А чтобы доказать, что компилятор выводит тот машинный код, который ожидается, опять нужна формальная проверка на компьютере, в том или ином виде. Читай: нужен тот же парсер с формализацией.

Получается не просто “диагонализация”, а вообще-то некоторый замкнутый круг.

Адрес записки: https://dxdt.blog/2026/09/10/19169/