Языковые модели учатся доказывать теоремы: где предел

Идея скормить трансформеру формальный язык доказательств выглядела спорно ещё в 2020 году, когда OpenAI выпустила GPT-f для системы Metamath. С тех пор направление превратилось в отдельную ветку исследований: DeepMind обучил AlphaProof решать задачи IMO на уровне серебряного медалиста, Meta выпустила HyperTree Proof Search, а Lean-сообщество получило десятки моделей-помощников. Но реальная картина сложнее победных пресс-релизов.

Почему математика — не программирование

Языковая модель, генерирующая код на Python, ошибается сплошь и рядом: тесты падают, программист правит. С доказательством так не выйдет. Формальная система вроде Lean 4 или Coq либо принимает доказательство целиком, либо отвергает. Промежуточных состояний нет: ошибка в одной тактике обнуляет весь вывод.

Отсюда две ключевые особенности задачи:

• обратная связь бинарная и мгновенная — компилятор проверяет шаг за миллисекунды;
• пространство поиска взрывается экспоненциально — на каждом шаге доступны сотни тактик^*.

* Тактика — команда системы доказательств, преобразующая цель. Например, intro вводит переменную, rw переписывает выражение по равенству.

Как устроен современный пайплайн

Типичная схема состоит из трёх компонентов, работающих в цикле:

1. Policy-модель — трансформер, предсказывающий следующую тактику по текущему состоянию цели.
2. Value-модель — оценивает перспективность промежуточного узла в дереве доказательства.
3. Поиск — вариант MCTS или best-first, обходящий дерево гипотез.

Пример входа для policy-модели на Lean 4:

-- Goal:
-- n : ℕ
-- ⊢ n + 0 = n

-- Predicted tactic:
exact Nat.add_zero n

Модель обучают на парах «состояние — тактика», извлечённых из библиотек mathlib (Lean) и stdlib (Coq). Mathlib на сегодня содержит около 1,7 млн строк формальных доказательств — этого хватает для претрейна, но недостаточно для покрытия всей математики.

Что показывают бенчмарки

Стандартные наборы — miniF2F (школьные и олимпиадные задачи) и ProofNet (университетский уровень). Цифры по открытым публикациям:

AlphaProof решил 4 из 6 задач IMO 2024, но на каждую задачу ушло до трёх дней вычислений на TPU-кластере. Точную стоимость DeepMind не раскрывает; по оценкам сторонних наблюдателей, речь идёт о десятках тысяч долларов на задачу.

Разрыв между «модель нашла доказательство» и «модель нашла его за разумное время и деньги» — главный, о чём стоит помнить, читая новости про ИИ-математиков.

Сколько это стоит на практике

Если вы хотите попробовать Lean-копилот на своей задаче, порядок цифр такой:

• инференс DeepSeek-Prover 7B локально — около 15 ГБ VRAM, одна RTX 4090 (≈180 тыс. руб.);
• облачный запуск на A100 — от 1,5 до 3 долларов в час, одна нетривиальная лемма может потребовать 100–1000 попыток;
• файнтюн под свою библиотеку — от 500 долларов на GPU-время плюс сбор данных.

Для сравнения: коммерческие API общего назначения (Claude, GPT-4o) справляются с задачами miniF2F хуже специализированных моделей, потому что не видели достаточного объёма формальных доказательств. Использовать их как proof assistant можно, но эффективность заметно ниже.

Подводные камни

Разрыв между уровнями

Модель, решающая олимпиадные неравенства, беспомощна перед доказательством из алгебраической геометрии. Причина не в «уме», а в данных: формализованных доказательств продвинутой математики почти нет. Проект формализации доказательства Ферма-Уайлса в Lean, запущенный Кевином Баззардом, рассчитан на годы работы десятков математиков.

Галлюцинации в формальном мире

Модель охотно ссылается на несуществующие леммы mathlib с правдоподобными именами вроде Nat.add_comm_mul. Компилятор их отвергает, но каждый такой промах — потраченный бюджет поиска. Retrieval-augmented подходы (LeanDojo, ReProver) частично решают проблему, подтягивая релевантные леммы из библиотеки.

Автоформализация

Отдельная задача — перевод теоремы с естественного языка на Lean. Здесь модели ошибаются в 30–50% случаев даже на простых утверждениях, часто меняя смысл. Пока автоформализация остаётся полуручной работой.

Куда движется область

Ближайшие годы задают три вектора:

• Синтетические данные. DeepSeek-Prover генерирует миллионы задач вариацией существующих — это дешевле, чем ждать новых человеческих доказательств.
• Гибридные системы. AlphaProof комбинирует нейросеть с классическим solver AlphaZero-стиля. Чистый end-to-end LLM пока проигрывает.
• Интеграция в IDE. Lean Copilot и Coq-LSP-плагины превращают модель в помощника, а не автономного доказывателя — и это, судя по опросам сообщества, самый востребованный сценарий.

Стоит ли ждать ИИ, самостоятельно доказывающего гипотезу Римана? Не в ближайшее десятилетие. Стоит ли встраивать модель в свой workflow, если вы работаете с формальными методами уже сегодня? Да, экономия времени на рутинных леммах достигает 40–60% по отзывам пользователей Lean Copilot.