Математический ИИ добился почти безошибочного результата на стандартном тесте благодаря неожиданному приёму: сокращению собственной истории рассуждений. В работе daVinci-Prover модель Qwen3.5 с 9 млрд параметров решила 97,1% задач MiniF2F при машинной проверке доказательств. Авторы также сообщили о среднем приросте на 13,7 процентного пункта после специального этапа обучения.
В отличие от систем, выдающих готовое доказательство целиком, daVinci-Prover работает пошагово. Агент ищет нужные теоремы, записывает фрагменты решения, отправляет код в Lean 4 и исправляет ошибки по замечаниям проверяющей программы. В распоряжении агента семь инструментов. Успех засчитывается лишь после строгой проверки исходного утверждения, а не по убедительности ответа нейросети.
Для обучения команда собрала корпус из 33,7 млрд токенов. В примерах показаны поиск промежуточных утверждений, разбор ошибок, проверка гипотез и настоящие обращения к инструментам. Затем разработчики подготовили около 36 тысяч успешных цепочек действий для дополнительной настройки модели. За счёт такой подготовки ИИ изучал не только правильные ответы, но и путь к ним.
На Qwen3-8B новая методика подняла долю решённых задач с 73,4 до 85,3% на MiniF2F, с 68 до 85,3% на FATE-M и с 28,4 до 40,4% на ProofNet. Средняя прибавка составила 13,7 пункта по трём наборам при одинаковом протоколе испытаний. При этом более крупный учебный корпус не гарантировал преимущества: система обошла OProver-8B, обученную на 65 млрд токенов.
Ещё сильнее повлияла работа с памятью агента. Когда диалог достигал 200 тысяч токенов, система сворачивала старые действия, сохраняя задачу, текущий код и результаты проверок. В режиме с таким сжатием Qwen3.5-9B поднялась с 90,1 до 97,1% на MiniF2F. На значительно более трудном FATE-H та же модель получила 28%, а версия с 35 млрд параметров достигла 42%.
Разработчики отдельно выложили код среды daVinci-Prover с доступом к библиотекам Lean и проверкой результатов. В репозитории приведены другие испытания, уже с DeepSeek-V4.1-Flash и лимитом 200 взаимодействий на задачу: 93% на FATE-H и 47% на FATE-X. Использовали и новую версию Lean. Эти цифры нельзя приписывать обучению Qwen, поскольку модель и условия эксперимента отличаются.
Показатель 97,1% не означает, что ИИ способен самостоятельно решить почти любую олимпиадную задачу. MiniF2F содержит заранее формализованные условия известных задач. Независимый аудит 2025 года нашёл расхождения между текстом и формальными записями более чем в половине заданий старой версии. Чтение условия, его перевод в Lean и последующее доказательство остаются разными испытаниями.
Работу представили 12 ноября как предварительную научную публикацию, а результаты обучения пока не получили независимого воспроизведения. Авторы пообещали открыть обучающие данные и веса моделей после завершения анонимного рецензирования. Подобная формальная проверка уже применяется не только в математике, но и для анализа программного кода и цифровых схем.
