Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Дообучение только на контрпримерах может научить модель выдумывать опровержения даже для истинных теорем. В препринте команды National School of Artificial Intelligence и University of Birmingham, который не прошёл рецензирование и приводит замеры самих авторов, разреженная награда вернула распознавание истинных утверждений выше исходного уровня. Для команд это рабочая схема: сначала закрепить формат ответа, затем оценивать не сходство с образцом, а корректность результата.
Как контрпример превратили в проверяемый результат
Контрпример должен удовлетворять всем оставшимся условиям теоремы и одновременно опровергать её вывод. Обычная модель-оценщик проверяет это вероятностно и сама может ошибиться, поэтому в SymCE для каждой теоремы создали отдельный детерминированный верификатор на Python.
Модель выдаёт объект заданной формы: например, число, матрицу или набор значений. Верификатор проверяет каждую гипотезу и отдельно устанавливает, нарушен ли вывод. Такая схема превращает ответ в исполняемое свидетельство: его можно принять или отклонить без сравнения с эталонным текстом.
Корпус содержит 4 707 ложных утверждений из алгебры и вещественного анализа. Их получили из учебных теорем, удаляя отдельную гипотезу, а затем отбрасывая случаи без рабочего проверяющего модуля и подтверждённого контрпримера.
Вручную проверенная выборка показала 97,7% точности решений верификатора. Медианное время одной проверки составило 132 мс, поэтому тот же код удалось использовать и для оценки, и как источник награды во время обучения.
Перед обучением модель также получает краткую схему допустимого объекта. Это не подсказка к математическому решению, а контракт интерфейса: без него часть попыток тратилась бы на неподходящий синтаксис вместо поиска контрпримера.
Почему имитация сломала распознавание истинных теорем
Первый этап использовал обучение с учителем, SFT: модель показывали только ложные утверждения и готовые контрпримеры. Она лучше соблюдала формат, но усвоила побочный шаблон — на любой вход нужно выдать свидетельство, даже когда теорема верна.
На проверке истинных теорем доля правильных ответов упала с 0,27 у базовой модели до 0,00 после SFT. Эффект повторился в разных запусках и на Gemma-3-4B, поэтому его трудно объяснить случайной инициализацией или особенностью Qwen3-4B.
Затем модель обучали с проверяемой наградой, RLVR. Разреженный вариант давал положительный сигнал только за полностью корректный контрпример: все условия выполнены, а вывод опровергнут. Он поднял распознавание истинных теорем до 0,66.
На основной задаче доля контрпримеров, принятых с первой попытки, выросла с 0,30 у базовой модели до 0,50 после обучения с верификатором. Обученная модель также обошла проверенные в работе более крупные открытые математические модели и осталась в диапазоне коммерческих API.
Плотная награда давала частичный балл за отдельные выполненные гипотезы. На тесте с ложными утверждениями она работала не хуже разреженной в пределах погрешности, но заметно слабее восстанавливала способность признать теорему истинной. Частичный балл оставлял выгодной стратегию «выдать что-нибудь похожее на контрпример».
Что меняется в плане обучения математической модели
Работа не предлагает отказаться от SFT. Этот этап быстро учит модель формату ответа и снижает число синтаксических ошибок, но его стоит считать подготовкой к обучению по результату, а не самостоятельным способом поставить рассуждение.
Если для задачи можно написать детерминированную проверку, план стоит строить вокруг неё. Сначала задаётся строгий контракт ответа, затем SFT закрепляет этот контракт, после чего RLVR награждает только за конечное корректное состояние. Отдельный тест должен содержать случаи, где правильное действие — отказаться от генерации свидетельства.
Плотную награду не следует добавлять автоматически. Частичные баллы полезны, только если каждый промежуточный признак действительно приближает к требуемому результату. Здесь выполненные гипотезы без опровергнутого вывода выглядели как прогресс, хотя модель всё ещё не решила задачу.
Порог для эксперимента сравнительно низкий: обучение запускали на RTX 5090 с 32 ГБ памяти, а один этап RLVR занимал около девяти часов. Это позволяет проверить схему до перехода к более крупной модели, если сама предметная область допускает быстрый исполняемый верификатор.
Границы результата заданы устройством SymCE. Проверяли Qwen3-4B и Gemma-3-4B с адаптерами LoRA и алгоритмом GRPO; задачи охватывали учебную алгебру и вещественный анализ, а ложные утверждения строили удалением гипотезы. Для областей, где ответ нельзя надёжно проверить Python, SymPy или Z3, эта архитектура не переносится напрямую.
Главный практический вывод касается не только математики. Когда продукт генерирует конфигурации, планы или структурированные решения, сходство с примерами может закрепить формат и одновременно ухудшить способность распознавать невозможный запрос. Исполняемый критерий результата и отдельная проверка на корректный отказ защищают от этой ловушки лучше, чем дополнительные положительные примеры.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
