ИИ поставили перед настоящей математикой — а он едва вытянул на тройку

Математики получили первые официальные результаты проекта First Proof - проверки, которая показывает, как ИИ справляется с задачами из реальных математических исследований. Впечатления у проверяющих смешанные: большие языковые модели уже помогают искать идеи для доказательств, но вместе с удачными ходами выдают ошибки, лишние рассуждения и плохо оформленные ссылки.

First Proof запустили математики, которым не хватало понятного теста для ИИ. Компании часто проверяют нейросети на сложных математических задачах, но такие проверки не всегда похожи на работу профессионального исследователя. Одно дело - решить олимпиадную задачу или найти численный ответ. Другое - написать доказательство для вопроса, который возник при подготовке научной статьи.

В феврале проект провел пробный раунд. Тогда результаты оказались неровными: внутренние системы компаний заметно обошли модели, доступные обычным пользователям. После этого организаторы решили проверять только инструменты, к которым исследователи могут получить доступ. Так тест стал ближе к реальной работе математиков, а не к закрытым демонстрациям ИИ-компаний.

В новом раунде участвовали OpenAI и три академические группы. Среди участников были команды из Швейцарской высшей технической школы Цюриха и Орхусского университета в Дании, Калифорнийского университета в Лос-Анджелесе и Принстонского университета. OpenAI представила ChatGPT-5.5 Pro, остальные команды показали исследовательские системы, собранные в университетах.

Задачи для проверки прислали математики из разных областей. Организаторы не брали учебные примеры и популярные головоломки. Моделям дали вопросы, похожие на настоящие рабочие задачи из математики: там нужен не короткий ответ, а последовательное доказательство.

Ответы проверяли оплачиваемые эксперты. Рецензенты собрались в Гарвардском центре математических наук и приложений и два дня разбирали решения ИИ. По смыслу это напоминало ускоренную проверку математической статьи: обычно такая работа может занимать полгода или больше.

Доказательство засчитывали, если основная идея была верной, а ошибки можно было исправить без полной переделки. В математических журналах похожий случай обычно отправляют на небольшие правки. Но часть ответов оказалась пограничной: решение вроде бы шло в правильную сторону, но не всегда дотягивало до убедительного доказательства. Поэтому некоторые результаты указали диапазоном.

Лучший результат показала IMProofBench, система исследователей из Цюриха и Орхуса. Эксперты сочли почти правильными шесть или семь ее решений из десяти. ChatGPT-5.5 Pro справился с четырьмя или пятью задачами. В целом хотя бы одна система дала почти верное решение для шести или семи задач из десяти.

Сильные стороны моделей уже знакомы математикам, которые пробуют ИИ в работе. Нейросети быстро ищут редкие ссылки в литературе, перебирают известные методы и могут долго развивать скучный, но технически нужный ход. В одном случае модель взяла подход, который авторы задачи сами видели, но не стали доводить из-за большого объема рутинных выкладок. ИИ продолжил этот путь и дошел дальше.

Но удачное решение не означает, что модель рассуждает как математик. За хорошим результатом часто стоит не один чат-бот, а целый рабочий процесс. Базовая языковая модель может отказаться от трудной задачи, придумать неверное доказательство или сослаться на несуществующую работу. Поэтому разработчики добавляют проверку: другие модели читают промежуточные шаги, ищут ошибки, предлагают исправления и отправляют систему на новую попытку.

В англоязычных материалах такую схему называют scaffolding. В русском тексте проще описать ее как набор подсказок и проверок вокруг основной модели. Она не решает задачу совсем одна: ее заставляют пробовать снова, сравнивать варианты и исправлять слабые места. Такая организация заметно повышает качество ответов.

IMProofBench работает именно так. В основе стоит тот же ChatGPT, но при затруднении система может обращаться к другим моделям, включая Claude от Anthropic и Gemini от Google. В итоге решение ищет не одна модель, а связка ИИ-инструментов, которые проверяют и дополняют друг друга.

Такой подход быстро становится дорогим. В отдельных случаях множество параллельных запросов к разным моделям стоило почти 1000 долларов за одну попытку, причем даже неверный ответ мог обойтись в такую сумму. Для науки это уже не мелкая техническая деталь. Если исследовательские группы начнут закладывать в гранты расходы на токены и доступ к коммерческим моделям, ИИ станет отдельной статьей бюджета в математике.

Еще одна проблема связана с научной аккуратностью. Модели часто пропускали нужные ссылки или оформляли их плохо. Для человека такая работа выглядела бы как нарушение академических норм: в математике нельзя использовать чужие идеи без понятного указания источника. Организаторы First Proof рассчитывают, что профессиональное сообщество сможет подтолкнуть разработчиков ИИ к более строгой работе со ссылками.

Раунд профинансировали благотворительные фонды и крупные ИИ-компании, которые сделали пожертвования без специальных условий. Среди доноров была Anthropic, хотя компания не отправляла свою модель на проверку. Организаторы подчеркивают, что First Proof должен стать независимым и прозрачным способом оценивать ИИ в исследовательской математике.

В ближайшие недели команда проекта планирует открыть дополнительные задачи для всех желающих. Их смогут попробовать профессиональные математики, любители и пользователи разных моделей. Следующий официальный раунд First Proof намечен на осень.

Главный вывод не сводится к счету в задачах. ИИ уже может брать на себя часть черновой работы: искать идеи, проверять длинные варианты, подбирать методы и разбирать литературу. Но эксперт все еще нужен на каждом важном шаге. Модель может уверенно написать ошибочное доказательство, поэтому человеку приходится проверять, где есть рабочая идея, а где только убедительно оформленный текст.