Доклад Дениса Федянина на «Международной конференции 2026 года по искусственному интеллекту для научных открытий и инноваций» (Шэньчжэнь, Китай)
Денис Федянин выступил с докладом «Самоигра (self-play) с вариационным синтезом задач (variational problem synthesis) в обучении с подкреплением с проверяемыми наградами (reinforcement learning with verifiable rewards)» на международной конференции в Китае, которая проходила 23-25 октября.
Доклад был на основе выполненного и защищенного ВКР магистратуры ФКН, где талантливая студентка Валерия Демина под научным руководством Дениса Федянина работала (вначале в рамках курсовой, потом ВКР) над этой темой.
Аннотация
К моменту выхода работы уже было известно, что RLVR применяется для пост-тренировки LLM-доказывателей в Lean 4, что стандартные self-taught подходы (Lean-STaR, ReSTEM) оставляют только успешные траектории, отбрасывая провалы, что узкое множество задач — главное узкое место RLVR, и что неудачные траектории содержат корректные префиксы и локально верные шаги. Новым является систематическое использование отброшенных неудачных попыток как независимого источника сигнала: bottom-up синтез задач из ошибок генератора без учителя и эталонного доказательства (в отличие от top-down DeepSeek-Prover-V2 и ProofAug), две стратегии извлечения — MCSP-скелеты с одним sorry из структурных ошибок и задачи на завершение префикса из линейных, многоцелевой энкодер тактик (ByT5-small) с попарным ранжированием и k-DPP для подавления дубликатов в BFS, а также сквозная оценка цикла «добыча → LoRA SFT → MaxRL-LoRA» со статистической проверкой каждого этапа и сдвигом границы решаемости (+22 / −17 теорем). Для лаборатории логики, лингвистики и формальной философии особенно значимо, что неудачное доказательство трактуется не как шум, а как структурированный лингвистический и логический объект: из него извлекаются корректные синтаксические фрагменты, верифицируемые формально, — то есть синтез задач выступает как декомпозиция доказательственного рассуждения, соединяющая анализ тактик, логическую структуру целей и формальную проверку в Lean 4.
