Представлен LeanPRM: Lean размечает шаги доказательств без людей
Нейросети уже пишут длинные и сложные математические доказательства, и проверка их пошаговой корректности становится узким местом. Обучаемый верификатор (проверяющая модель) мог бы делать это дёшево, но для его обучения нужна метка правильности на каждом шаге, а для открытых доказательств такие метки получить трудно. Существующие подходы берут их у людей-разметчиков (дорого) или выводят из итогового ответа (которого у доказательств нет); к тому же формализация каждого доказательства в Lean требует усилий экспертов.
Авторы предлагают LeanPRM, каркас (фреймворк), в котором система проверки доказательств Lean создаёт пошаговые метки для доказательств на естественном языке. Одна модель пишет доказательство на естественном языке вместе с парным формальным доказательством, причём без обратной связи от Lean. Затем Lean размечает каждый шаг, а вторая модель отбрасывает случаи, когда сбой вызван только формальным синтаксисом, чтобы отрицательные метки отмечали именно математические ошибки.
Получившийся набор данных, тоже называемый LeanPRM, содержит 10 634 доказательства и 152 тысячи размеченных шагов без ручной разметки. Верификатор на основе Qwen3-4B, обученный на LeanPRM, повышает точность точного совпадения пошаговых меток на отложенной выборке из 200 доказательств (LeanPRM-Bench) с 48,2 до 74,7. Та же базовая модель, обученная на PRM800K, достигает 60,3. Кроме того, такой верификатор лучше отбирает доказательства при выборе лучшего из N вариантов (best-of-N) на задачах уровня олимпиады IMO и превосходит верификатор, обученный на PRM800K, на трёх из четырёх внешних бенчмарков проверки. Обучение на LeanPRM улучшает верификаторы любого размера от 0,6 до 8 млрд параметров на LeanPRM-Bench, Hard2Verify и IMO-GradingBench.
По мысли авторов, поскольку метки не требуют ручной разметки, LeanPRM может расти вместе с числом доступных формальных утверждений. Это открывает путь к пошаговой обратной связи для доказательств, созданных ИИ, которые людям трудно проверять.
Ключевые факты
- LeanPRM, каркас, в котором Lean автоматически размечает каждый шаг доказательства на естественном языке; вторая модель отсеивает сбои, вызванные только формальным синтаксисом.
- Набор данных: 10 634 доказательства и 152 тысячи размеченных шагов, без ручной разметки.
- Верификатор на Qwen3-4B: точность точного совпадения пошаговых меток на LeanPRM-Bench (200 доказательств) выросла с 48,2 до 74,7; при обучении на PRM800K, 60,3.
- Лучше, чем PRM800K, на трёх из четырёх внешних бенчмарков проверки; улучшение отмечено для моделей от 0,6 до 8 млрд параметров на LeanPRM-Bench, Hard2Verify и IMO-GradingBench.
Почему это важно
Когда ИИ пишет всё более длинные доказательства, проверять их вручную становится всё труднее. Обучить проверяющую модель мешает нехватка пошаговых меток правильности. Работа предлагает способ получать такие метки автоматически через Lean, без людей-разметчиков и без ручной формализации каждого доказательства.
Кому это важно
Исследователям, которые обучают модели математических рассуждений и верификаторы доказательств, а также тем, кто работает с формальной верификацией и системой Lean. Тем, кто использует выбор лучшего из N вариантов при генерации доказательств, тоже есть что взять: авторы сообщают об улучшении такого отбора на задачах уровня IMO.
Как это применить
Из текста источника видно подход: модель пишет доказательство на естественном языке и парное формальное доказательство, Lean размечает шаги, а вторая модель убирает сбои из-за синтаксиса. Сведений о публикации кода, набора данных или лицензии в источнике нет, поэтому практическое применение пока ограничено пониманием метода.
Можно ли доверять
Это препринт: приведены результаты самих авторов. Основное сравнение сделано на LeanPRM-Bench, отложенной выборке из 200 доказательств, способ построения которой в источнике не указан, поэтому выигрыш над PRM800K на ней нужно читать с поправкой. Более независимо выглядит результат на внешних бенчмарках, но там преимущество только на трёх из четырёх. Для результата best-of-N на задачах уровня IMO числа не приведены.
Риски и подводные камни
Метки зависят от того, насколько точно формальное доказательство соответствует доказательству на естественном языке; отбраковку синтаксических сбоев выполняет вторая модель, и её ошибки могут влиять на качество меток. Выигрыш на одном внешнем бенчмарке из четырёх не подтверждён. Заявление о том, что набор данных сможет расти вместе с числом формальных утверждений, пока остаётся предположением авторов.