LeanPRM: Lean разметил 152 тысячи шагов доказательств без людей и поднял точность до 74,7%

Проверка длинных математических доказательств, которые пишут языковые модели, становится узким местом. Авторы LeanPRM предлагают получать пошаговую разметку от ассистента доказательств Lean, без аннотаторов. В итоге получился датасет из 10 634 доказательств и 152 тысяч размеченных шагов. Верификатор на Qwen3-4B, обученный на нём, поднял точность попадания в метку шага на отложенном наборе LeanPRM-Bench (200 доказательств) с 48,2 до 74,7. Та же базовая модель, обученная на PRM800K, показала 60,3.

Откуда берутся метки

Обучить процессный верификатор (PRM) можно только на данных, где у каждого шага есть оценка «верно» или «неверно». Для открытых доказательств такие метки получить трудно. Люди-разметчики стоят дорого. Метки из финального ответа не помогают, потому что у доказательства нет числа, с которым можно сверить результат. Формализация каждого доказательства в Lean требует работы экспертов.

LeanPRM обходит эти ограничения так. Модель пишет доказательство на естественном языке и параллельно формальное доказательство, причём без обратной связи от Lean. Затем Lean проверяет формальную версию и ставит метку каждому шагу. Вторая модель отфильтровывает случаи, где провал вызван только синтаксисом формального текста. После этого отрицательные метки отражают именно математические ошибки, а не огрехи записи.

Что показали цифры

Основные результаты из статьи:

• датасет: 10 634 доказательства, 152 тысячи шагов с метками, ручной разметки нет;
• LeanPRM-Bench (200 отложенных доказательств): Qwen3-4B вырос с 48,2 до 74,7 точного совпадения по шагам;
• базовая линия PRM800K на той же модели: 60,3;
• на трёх из четырёх внешних бенчмарков верификатор на LeanPRM обходит версию на PRM800K;
• в отборе best-of-N на задачах уровня IMO он выбирает более качественные доказательства;
• прирост подтверждён на моделях от 0,6B до 8B параметров на LeanPRM-Bench, Hard2Verify и IMO-GradingBench.

Устойчивость эффекта по размерам важна не меньше, чем рекордная цифра. Улучшение видно и у совсем маленькой модели, и у восьмимиллиардной. Значит, дело в качестве сигнала, а не в удачном подборе одной конфигурации.

Где стоит смотреть внимательнее

Главный разрыв, 48,2 против 74,7, измерен на бенчмарке, который собрали сами авторы и в котором те же процедуры генерации и разметки. Для такой выборки LeanPRM-обучение имеет естественное преимущество. Поэтому внешние тесты ценнее: там выигрыш есть на трёх бенчмарках из четырёх, то есть не везде. Вывод о четвёртом статья в приведённом описании не раскрывает, и его стоит проверить по полному тексту.

Есть и структурное ограничение. Метки верны настолько, насколько формальное доказательство соответствует естественному. Если модель написала формальную версию, которая расходится с текстом, Lean оценит не то, что читает человек. Фильтр второй модели снижает риск шума от синтаксиса, но не гарантирует полного соответствия двух версий. Охват тоже ограничен: разметить можно то, что получилось формализовать.

Практическая ценность в масштабировании. Объём данных растёт вместе с числом доступных формальных утверждений, а не с бюджетом на экспертов. Командам, которые обучают математические модели с best-of-N или RL по процессным наградам, это возможность получить плотный сигнал на шагах рассуждения без закупки разметки. Для оценки подхода стоит прогнать свой верификатор на Hard2Verify и IMO-GradingBench. Заодно полезно проверить, насколько выигрыш сохраняется на доказательствах, далёких от формализованных в Lean областей.