Авторы SymCE представили набор из 4707 ложных математических гипотез и исполняемые Python-верификаторы, которые проверяют предложенные к ним контрпримеры. На этой основе они сравнили два способа обучения языковых моделей: обычную донастройку на примерах и обучение с подкреплением по результату проверки.
Работа важна не только как новый бенчмарк. В экспериментах авторов обучение на одних контрпримерах привело к тому, что модель стала хуже распознавать истинные теоремы. Обучение с подкреплением помогло устранить этот эффект.
Как устроен SymCE
Авторы собрали задачи из алгебры и вещественного анализа на уровне бакалавриата. Для каждой ложной гипотезы приложен верификатор: программа проверяет, действительно ли предложенный объект опровергает утверждение. Таким образом, система оценивает не сходство ответа с образцом, а выполнение математического условия.
Этот же верификатор используется как источник награды при обучении. Авторы называют такой подход RLVR — обучение с подкреплением, где сигнал для модели даёт проверяемый результат. В опубликованном описании сказано, что набор, код, модули верификаторов и аннотации доступны в репозитории проекта.
Что показали эксперименты
На Qwen3-4B дообучение только на контрпримерах снизило показатель распознавания истинных теорем с 0,27 до 0,00. Затем обучение с подкреплением со скудной наградой за итог проверки подняло его до 0,66 — выше исходного уровня. Авторы сообщают, что эффект ухудшения воспроизвёлся на четырёх случайных начальных состояниях и на Gemma-3-4B.
В работе также сравниваются редкая и более плотная награды. На основных задачах их результаты статистически не различались, но на отдельной проверке калибровки возник разрыв в 33 процентных пункта. Авторы связывают его с компонентом частичной награды. Это напоминание: одинаковая оценка на целевом наборе не гарантирует одинакового поведения на других проверках.
Ограничения и практический смысл
Авторы сообщают, что их модель на 4 млрд параметров превзошла все проверенные открытые математические модели на 7 млрд параметров, оставалась конкурентоспособной с шестью коммерческими API и переносила результаты на GSM8K, MATH-500 и MMLU-college-math без изменения промпта. Эти выводы относятся к конкретным моделям, задачам и протоколу исследования; сами по себе они не доказывают общего превосходства на математических задачах.
Подход зависит от качества и корректности верификаторов: если проверка ошибается или покрывает лишь часть условий задачи, сигнал обучения тоже будет ограниченным. Человеческая проверка 177 решений верификаторов показала 97,7% точности, но это оценка небольшой выборки, а не гарантия безошибочности всего корпуса.
Для разработчиков главный вывод — при обучении генерации опровержений стоит отдельно проверять, не теряет ли модель способность отличать ложные утверждения от истинных. Исполняемый оракул позволяет измерять результат напрямую, однако перенос выводов на другие области потребует собственных проверяемых задач и оценок.
Источники
