Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Модель научили быстро предсказывать, примет ли Lean 4 кандидат на формальное доказательство. В препринте EPFL, который не прошёл рецензирование и содержит числа, полученные самими авторами, гибридная проверка сократила длительность шага обучения на 31%. Точный Lean остаётся в контуре, но больше не задерживает всю пачку доказательств.
Каскад сначала отсеивает кандидатов, затем восстанавливает обратную связь Lean
При обучении прувер генерирует пачку доказательств, а Lean проверяет каждое на процессоре. Если отдельные проверки идут долго, GPU с моделью ждут сигнал вознаграждения для всей пачки. Простой короткий тайм-аут ускоряет процесс, но помечает часть корректных доказательств как неуспешные.
Для обучения оценщика собрали 4,84 млн программ с вердиктами компилятора. Перед обучением на этих примерах модели дополнительно учили на исходном коде и документации Lean, чтобы они знали синтаксис, тактики и структуру доказательств.
Оценщик состоит из двух ступеней. Qwen3-8B быстро выдаёт вероятность того, что программа корректна, и отклоняет слабых кандидатов. Только положительные ответы переходят к Qwen3-4B, которая воспроизводит трассу обратной связи: текущее состояние цели, сообщения об ошибках и место, где Lean остановил бы проверку.
Кандидат получает положительный вердикт, только если обе модели считают его корректным. Такая схема снижает число ошибочных принятий и не тратит генерацию длинной трассы на программы, которые первая ступень уже отклонила. Для дополнительного ускорения трассы выводят с упреждающим декодированием, при котором основная модель проверяет сразу предложенные последовательности токенов.
Во время групповой относительной оптимизации политики (GRPO) Lean и нейронный оценщик работают параллельно. Когда GPU заканчивает обработку пачки, система сохраняет уже готовые точные вердикты Lean, подставляет прогнозы для остальных кандидатов и отменяет незавершённые проверки.
Приближённый вердикт оказался быстрее параллельного Lean
Каскад предсказал принятие кандидата с точностью 87,8%. С ускоренным декодированием он обрабатывал 3,5 кандидата в секунду на одной H100 — в 4,2 раза производительнее использованного авторами параллельного контура Lean с повторным использованием загруженного окружения.
Это сравнение двух разных результатов работы. Lean возвращает точный вердикт компилятора, а каскад — вероятностный прогноз. Выигрыш появляется не потому, что нейронная модель заменяет формальную проверку без потерь, а потому, что она ограничивает время ожидания при расчёте сигнала вознаграждения.
Гибридная схема сократила полный шаг обучения на 31%. В него входили генерация доказательств, проверка, расчёт вознаграждений и обновление прувера, поэтому ускорение относится ко всему циклу, а не только к отдельному вызову оценщика.
Точность проверяли на результатах Pythagoras-Prover, Goedel-Prover и DeepSeek-Prover для наборов miniF2F и ProofNet. В эталон вошли кандидаты, для которых Lean успел вернуть пригодный вердикт в отведённое время. Само обучение прувера проверяли после одного цикла GRPO на miniF2F, поэтому работа показывает эффект в конкретном стеке Lean и не устанавливает такой же выигрыш для других языков или проверяющих систем.
Планы меняются в обучающем контуре, но не на границе доверия
После обучения с гибридным сигналом pass@1 составил 62,2% против 62,4% при использовании только Lean. Эта метрика показывает долю задач, которые прувер решает одной попыткой. При том же времени на проверку вариант с укороченным тайм-аутом Lean достиг 59,8%, то есть простое прекращение медленных проверок не сохранило качество.
К моменту остановки гибридной проверки точные ответы Lean покрывали около 43% кандидатов. Остальная часть сигнала зависела от каскада, поэтому такая архитектура требует сохранять формальный проверяющий модуль и регулярно сравнивать прогнозы с его вердиктами.
Это особенно заметно по ходу обучения: итоговая точность каскада на новых попытках прувера снизилась до 81,7%. Модель меняла распределение генерируемых доказательств и чаще находила ошибки оценщика. Более слабые классификаторы деградировали сильнее, что делает полную замену Lean рискованной.
Работа меняет планы команд, у которых проверка доказательств уже стала узким местом обучения. Вместо расширения процессорного пула можно добавить GPU-оценщик, запускать его одновременно с Lean и задать момент, после которого прогнозы закрывают незавершённую часть пачки. Для финальной оценки прувера, публикации доказательств и любых решений, где нужен гарантированный результат, остаётся точная проверка Lean.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
