Lean используют как процессный оракул в обучении моделей для автоматического доказательства теорем
Исследователи предложили способ обучать системы автоматического доказательства теорем, используя proof assistant Lean как источник детализированной обратной связи. В классическом подходе reinforcement learning from verifiable rewards (RLVR) модель обычно получает лишь один бинарный сигнал, проверку итогового результата. Авторы работы обращают внимание, что формальные системы доказательства дают куда более богатую структурированную информацию. Благодаря этому можно извлекать плотные и корректные сигналы обратной связи прямо в процессе доказательства.
В новой схеме Lean работает как символический процессный оракул. Во время обучения он не только подтверждает конечный результат, но и даёт проверенную обратную связь по отдельным тактикам. Попытка доказательства представляется как последовательность тактик. Затем механизм elaboration в Lean отмечает локально корректные шаги и указывает первый шаг, где появляется ошибка. Такая разметка позволяет формировать плотные сигналы credit assignment, опирающиеся на проверку в рамках типовой теории.
Структурированные награды включаются в objective обучения reinforcement learning в стиле GRPO. Используются методы first-error propagation и first-token credit, они помогают совместить преимущества сигналов уровня результата и уровня процесса. Эксперименты с STP-Lean и DeepSeek-Prover-V1.5 показывают, что supervision на уровне тактик в большинстве конфигураций работает лучше, чем обучение только по итоговому сигналу. Улучшения наблюдаются и на бенчмарках, включая MiniF2F.
Ключевые факты
Препринт arXiv:2606.20068v1 описывает метод Process-Verified Reinforcement Learning для доказательства теорем с использованием proof assistant Lean.
Lean используется как «символьный процессный оракул», который во время обучения выдает проверенную обратную связь как на уровне результата, так и на уровне отдельных тактик.
Попытки доказательства разбиваются на последовательности тактик, а механизм elaboration в Lean помечает локально корректные шаги и указывает на самый ранний ошибочный шаг.
В экспериментах с STP-Lean и DeepSeek-Prover-V1.5 обучение с тактическим уровнем обратной связи превосходит базовые подходы только с итоговым сигналом на бенчмарках, включая MiniF2F.