Претензия к языковым моделям годами не менялась: складно болтают, а за слова не в ответе. Теперь у ИИ есть экзамен, на котором не спишешь, — формальное доказательство. DeepMind, если верить сообщениям, добилась результата, где модель сама вывела и машинно проверила математические закономерности для машин Тьюринга. На слух — нишевая новость. На деле планка сдвинулась именно тут. Почему «доказать» оказалось и сложнее, и ценнее, чем «угадать», и что из этого выйдет для науки — попытаемся разобраться.
Обычный ответ нейросети — текст, за которым никто не стоит. Правдоподобно? До неприличия. Проверяемо? Вот с этим беда. Формальное доказательство устроено с точностью до наоборот: модель излагает рассуждение не прозой, а на языке интерактивного прувера — скажем, Lean, — и компилятор собирает из него объект, который проверяющее ядро либо принимает, либо отвергает. Серединки тут нет. Пропущенный шаг, выдуманная лемма, ссылка не туда — это не «особая точка зрения», а просто ошибка сборки.
Поэтому олимпиадные результаты машин здесь не пустой звук. В 2024 году связка AlphaProof и AlphaGeometry от DeepMind показала уровень серебряной медали Международной математической олимпиады, решая задачи в формальной среде. Медаль, по большому счёту, вторична. Ценно другое: удачей такое не спишешь. Модель не «угадала» число — она выдала цепочку шагов, которую любой желающий прогоняет через проверяльщик и убеждается сам.
Крошечная машина Тьюринга — праздник примитивизма: лента, головка, таблица на несколько правил. При этом пространство её поведений бездонно. Одни машины зацикливаются мгновенно, другие выводят правильные узоры, третьи трудятся дольше, чем существует вселенная, — не зря вокруг функции занятого бобра идёт отдельная гонка. А между «тривиально» и «безнадёжно» лежит царство закономерностей, которые никто толком не каталогизировал.
Здесь, по сообщениям, и отличилась модель DeepMind. Её обучали на небольших машинах, а она сделала то, чего от неё мало кто ждал: обобщила. Система сама вывела математические закономерности, управляющие поведением увиденных программ, — и доказала их. Самое вкусное тут в механике: галлюцинация гибнет на первом же шаге проверки. Выведенное «правило» неверно? Доказательство не соберётся, и системе придётся искать настоящее. Мало данных плюс жёсткий верификатор — режим, в котором не обманешь ни себя, ни других.
Формальные доказательства старше нейросетей. Компьютер подтвердил теорему о четырёх красках ещё в семидесятых, а формализация доказательства гипотезы Кеплера отняла у команды Томаса Хейлса годы ручной работы. ИИ перевернул экономику процесса. Сообщество Lean накопило библиотеку Mathlib с сотнями тысяч готовых формализованных лемм, а Теренс Тао показал темп на личном примере: его Liquid Tensor Experiment превратил свежую теорему в машинно проверяемый текст за месяцы, а не десятилетия.
А рядом — AlphaEvolve, связка эволюционного поиска с языковой моделью, которая не придумывает, а отбирает: выживает лишь то, что прошло беспощадный тест. Система улучшила классические алгоритмы умножения матриц, оптимизировала расписание задач в дата-центрах и ядра для TPU. Формула всюду одна: генерация гипотез плюс независимая машинная проверка. Перед нами, в сущности, научный метод, пересобранный в кремнии, — с той разницей, что перебирать варианты машина способна в масштабах, которые ни одному факультету не снились.
У формальных методов здесь родословная глубокая. Андрей Марков-младший построил теорию нормальных алгорифмов и строго доказал алгоритмическую неразрешимость ряда задач; Андрей Колмогоров заложил основы алгоритмической сложности; Юрий Матиясевич в 1970 году закрыл десятую проблему Гильберта. Олимпиадная школа до сих пор поставляет людей, одинаково свободно чувствующих себя в математике и в коде.
Прикладная ставка — на верификацию там, где иначе никак. «Лаборатория Касперского» годами развивает KasperskyOS, микроядро которой прошло формальную верификацию: по строгости гарантий это редкость даже на мировом фоне. А вот генеративный фланг проседает. GigaChat от «Сбера» и YandexGPT с математическими задачами, судя по всему, справляются, но моста от их рассуждений к пруверам вроде Lean пока не видно — как не видно и крупного локального сообщества формализаторов. Отдельные курсы по интерактивным доказательствам, по имеющимся данным, появляются в российских вузах, а спрос на верифицированный софт в критической инфраструктуре, как ожидают, будет расти. Ниша «нейросеть плюс формальная проверка» пустует — что одновременно и ограничение, и окно возможностей.
Автоматизация доказательств математиков не отменяет — она меняет их роль. Генерацию гипотез и рутинную дедукцию можно спихнуть на машину, если рядом стоит строгий верификатор, превращающий правдоподобие в проверяемость. Результат с машинами Тьюринга, если он подтвердится, — победа небольшая, но траекторию обнажает: ИИ перестаёт быть оракулом, вещающим ответы, и становится соавтором с прозрачной бухгалтерией, где каждый шаг можно перепроверить. Прорывы теперь случатся там, где наука научится спрашивать машины не «как думаешь?», а «докажи».