Goedel-Prover v2: ИИ-доказчик теорем с формальной верификацией на Lean

Проблема верификации в ИИ-доказательствах теорем

В последние годы ИИ-модели научились решать всё более сложные математические задачи — вплоть до уровня Международной математической олимпиады (IMO). Однако оставалась проблема: проверить правильность таких решений мог только человек.

Эта проблема связана с тем, что крупные языковые модели — «чёрные ящики». Они могут выдать разумное на вид доказательство, но нет способа гарантировать его корректность.

Goedel-Prover v2: ИИ-доказчик теорем на языке Lean

В июле 2025 года исследователи из Принстона представили Goedel-Prover v2 — обновлённую версию открытого ИИ-доказчика, построенного на языке Lean. Lean — это язык формальной верификации, позволяющий строго доказывать математические утверждения и проверять корректность каждого шага.

Goedel-Prover v2 умеет:
– генерировать математические доказательства,
– проверять их строгость в Lean,
– автоматически исправлять ошибки в собственных рассуждениях (режим самокоррекции).

Результаты ИИ-доказчика теорем на математических бенчмарках

Модель успешно прошла три бенчмарка:
– PutnamBench — задачи университетского уровня,
– miniF2F — задачи уровня школьной математики,
– MathOlympiadBench — задачи уровня IMO.

Точность модели на miniF2F выросла с 60% (в первой версии) до 90%. При этом Goedel-Prover использует модель с 32 млрд параметров и работает на вычислительных ресурсах, доступных в академической среде — в 20 раз меньших, чем у конкурентов.

Самообучение и гарантия корректности доказательств

Отдельная особенность: модель обучается в режиме scaffolded learning. Если она не может решить задачу, она генерирует более простые варианты, решает их и добавляет в собственную тренировку. Это позволяет модели накапливать полезные примеры и улучшаться без внешнего вмешательства.

Ключевая гарантия корректности — использование Lean: каждое доказательство формализуется и строго проверяется по математическим правилам.

Перспективы ИИ в математических открытиях

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

По мнению авторов, это один из ключевых шагов к созданию полноценного ИИ-соавтора в математике.