В начале июня 2026 вышли результаты First Proof Second Batch — первого бенчмарка, который одновременно: (1) состоит из исследовательских задач, (2) заведомо не встречавшихся в обучающих данных, и (3) проверяется живыми математиками вслепую по правилам журналов.
Заголовки привычно написали: «ИИ провалил тест по математике». Но самое интересное в отчёте — не счёт, а то, что ни один тип ошибок не нов. Каждую можно было предсказать заранее из классических работ о математическом мышлении и надёжности проверок. Если сложить эти источники, результаты First Proof перестают удивлять.
Ниже — разбор по первоисточникам (отчёт First Proof на 35 страниц [1] и заметка в Nature [2]), а не по пересказу пресс-релиза. И тревога тут не только академическая: более 150 математиков уже публично призвали не доверять слишком убедительным на вид «доказательствам» ИИ [8] — именно потому, что строгий текст легко маскирует подмену одного трудного шага.
TL;DR
Если читать некогда, суть в нескольких тезисах.
Что произошло. First Proof Second Batch — первый бенчмарк на исследовательских задачах вне обучающих данных, со слепой проверкой ~30 математиков. Лучшая система решила 6 задач из 10; ИИ уступил людям.
Что важнее счёта. Ни один тип ошибок не нов — каждый заранее описан в классике: Пуанкаре (инсайт ≠ доказательство), Оакли (диффузный режим), Бернштейн (верхний смысловой уровень), ТРИЗ (противоречие vs интерполяция), работы о коррелированных ИИ-судьях.
Профиль провала. Модели дотошны на рутине и «размахивают руками» на трудном шаге («следует из стандартных рассуждений»), галлюцинируют ссылки, копируют без атрибуции и местами доказывают ложь.
Оговорка по потолку. В тесте участвовали только публичные модели. Специализированная Aletheia от Google и полная (невыпущенная) Claude Mythos не допускались — бенчмарк меряет потолок доступного, а не существующего. При этом одна система дала новое безупречное доказательство.
Экономика. «Совет судей» за 4 799 долларов не пробил потолок голой модели за 117 долларов — он лишь дороже подтвердил общий слепой угол.
Главный вывод. Разрыв с человеком — не «нехватка интеллекта», а конкретные дефициты (нет фазы открытия, нет локализации трудности, иллюзия независимости проверок), описанные задолго до First Proof. Вывод LLM — гипотеза, а не доказательство; для критичных задач нужен внешний детерминированный контур (формальные верификаторы, тесты, человек).
Что это был за тест
Большинство «математических» бенчмарков меряют не то, что обещают: задачи либо валяются в открытом доступе (могли попасть в обучение), либо проверяются по короткому ответу, когда само доказательство никто не читает. First Proof закрывает обе эти дыры.
Задачи новые. Десять исследователей дали по одной задаче из собственных неопубликованных работ. У автора уже было решение (до 8 страниц), но в интернете оно нигде не светилось.
Полная автономность. Система получала задачу в формате
.texи работала в один заход: без диалога, без человека в петле, без итеративной «натаски».Слепое судейство. Около 30 математиков-предметников рецензировали обезличенные решения по журнальной шкале: «безупречно / мелкие правки / крупные правки / отклонить».
Важная деталь, которую упомянули далеко не все пересказы: тестировались только публично доступные модели. Поэтому в бенчмарк не попали две, вероятно, сильнейшие системы — специализированная Aletheia от Google и невыпущенная Claude Mythos. Это принципиально: тест показывает потолок того, что можно купить «с полки» прямо сейчас, а не абсолютный предел возможного.
Какие модели участвовали
Система | Команда | Базовая модель | Что сверху |
|---|---|---|---|
A — ProofCouncil | ETH Zürich / Aarhus | gpt-5.5 pro | «Совет» из gpt-5.5, gemini-3.1-pro, claude-opus-4-7 |
B — Moonshot | UCLA (в т.ч. Т. Тао) | gpt-5.5 pro | harness с перепроверкой |
C — ChatGPT 5.5 Pro | OpenAI | gpt-5.5 pro | без обвязки, голая модель (режим xhigh) |
D — Momus | Princeton | gemini-3.1-pro | harness |
Всех прогоняли в одном режиме one-shot: задача → один заход → проверка людьми.
Результаты: не ноль, но и не «прорыв»
Если объединить все четыре системы, 7 задач из 10 получили хотя бы одну проходную оценку, ещё по двум задачам хотя бы одно решение дотянуло до уровня «крупные правки». Планка при этом довольно низкая: «мелкие правки» означают «математика верна, поправить оформление и ссылки».
Лучший индивидуальный результат показала команда ETH: их система закрыла 6 задач из 10. Два полюса полезно назвать поимённо.
Задача 5 (стохастические УрЧП). Система A выдала решение, признанное безупречным и при этом новым: ход отличался от человеческого, а промежуточный результат оказался даже сильнее исходного. Это уже настоящая математическая публикация.
Задача 4 (метрическая геометрия, Л. Гут). Полный провал. Система C сгенерировала теорему, дословно совпадавшую с тем, что её просили доказать, приписала её несуществующему «Предложению 9.1» Гута — и «тривиально вывела» требуемый результат из собственной выдумки.
Рецензентские отчёты здесь особенно ценны: они дают не только итоговый вердикт, но и «анатомию» ошибок. И все эти паттерны заранее описаны в классике — от философии математики до работ по надёжности проверок.
Пять заранее известных ошибок
Рис. 1. Пять типов ошибок моделей и классические работы, которые их предсказали.
1. Дотошность на лёгком, «размахивание рук» на трудном (Пуанкаре)
Сквозная претензия рецензентов: модель педантично расписывает рутину и перескакивает самый трудный шаг, объявляя его «следствием стандартных рассуждений». Анри Пуанкаре в «Науке и методе» [3] разводил две фазы: логика доказывает, но открывает интуиция; ключевая идея приходит после неосознанной инкубации, а не простого перебора.
First Proof в принципе измеряет только фазу доказательства. Модель без фазы открытия закономерно не умеет локализовать, где именно «болит» задача, и пролистывает критический шаг. Этот же тезис прямо вынесен во вводную главу отчёта First Proof [1].
2. Только фокусный режим (Оакли)
Барбара Оакли в «A Mind for Numbers» и курсе Learning How to Learn [4] описывает, что сложные задачи решаются не только в фокусном, но и в «диффузном» режиме — фоновой, рассеянной обработкой, где мозг примеряет разные конфигурации идеи.
LLM в one-shot-режиме работают практически только в фокусном режиме: одна траектория вывода, никаких пауз на «переспать с задачей». Отсюда дотошность на простом и пустота на действительно сложном шаге. Важно не перетягивать аналогию: «диффузный режим» — это всего лишь нейробиологическая метафора, а не конкретный алгоритм. Chain-of-Thought, Tree-of-Thought и многопроходная выборка частично эмулируют перебор вариантов, но в First Proof такие техники не применялись. Глубинный дефицит не в отсутствии режима как такового, а в отсутствии надёжной валидации промежуточного инсайта — модель не умеет отделять перспективную ветку рассуждения от тупиковой.
3. Проседает верхний смысловой уровень (Бернштейн)
Н. А. Бернштейн в работе «О построении движений» [5] описал иерархию уровней управления: верхний смысловой задаёт цель, нижние реализуют её в виде конкретных движений. У современных моделей нижние уровни — локальные шаги, рутинные выкладки — отрабатываются почти идеально, а вот верхний уровень, где нужно понять, в чём основной труд, даёт сбой.
По рецензиям это хорошо видно: там, где нужно изобрести или распознать ключевой приём, модель либо не замечает сложность, либо объявляет её «стандартной». В результате «гладкость» текста растёт, а решённость задачи — нет.
4. Интерполяция вместо разрешения противоречия (ТРИЗ)
В ТРИЗ Генриха Альтшуллера [6] новизна — это разрешение противоречия, а не интерполяция между известными решениями. Модели сильны там, где есть похожий образец в литературе. Вторая задача бенчмарка как раз попадает в эту область: три системы её закрыли, по сути «переведя» уже опубликованную задачу в нужную категорию.
Проблема не в самой стандартной терминологии — это нормальный перенос знаний, — а в нулевой атрибуции. Модели построчно заимствовали терминологию и даже буквенные обозначения автора (B, T, D, H) без единой ссылки; рецензенты справедливо отметили, что человеку такое засчитали бы за плагиат.
Там, где похожего образца нет (задача 4), наблюдаем противоположный экстремум — галлюцинацию теоремы и самоподтверждающуюся проверку: модель порождает посылку, равную выводу, и своим же контекстом её «подтверждает». Это уже не просто «обычная» галлюцинация, а самореферентная странная петля в духе Хофштадтера.
5. Иллюзия независимости проверок (коррелированные судьи)
Работа Kim, Garg, Peng, Garg (ICML 2025, arXiv:2506.07962) [7] показывает: два ИИ-судьи из одного семейства делают коррелированные ошибки, и «второе мнение» часто оказывается эхом первого.
В First Proof это всплывает в экономике ансамблей: самый дорогой harness (Moonshot, ~4 799 долларов) так и не вырвался вперёд — лучший результат по бенчмарку, 6 из 10, остался за более дешёвым «советом» ETH. «Совет судей» не пробивает общий слепой угол базовой модели, он просто дороже его подтверждает.
История с проверкой цитат — та же: и проверяемое, и проверяющее порождены одними и теми же семействами моделей, обученными на пересекающихся веб-данных с общей архитектурой. Прогнать одну и ту же информацию через большее число почти одинаковых моделей нельзя превратить в знание, которого нет ни у одной из них — это информационный потолок, а не вопрос числа судей. Корреляция здесь симптом, общий источник данных и архитектуры — причина.
Экономика: за что вы платите
Суммарная стоимость прогона всех десяти задач хорошо показывает цену «качества через обвязку».
Система | Стоимость | Что это |
|---|---|---|
C (голый ChatGPT 5.5 Pro) | $117 | базовая модель, один промпт на задачу |
D (Princeton, Gemini) | ~$1 014 | оценка по листинговым ценам |
A (ETH, ProofCouncil) | $3 186 | «совет» из трёх моделей |
B (UCLA, Moonshot) | $4 799 | самая дорогая обвязка |
Рис. 2. Стоимость растёт на два порядка, а потолок качества (6 из 10) — нет.
Голая модель оказывается в 27–41 раз дешевле самых богатых обвязок. Прирост качества реален, но покупается двумя порядками по деньгам и всё равно упирается в потолок «6 из 10 с оговорками» — трезвый сигнал для всех, кто строит сложные агентные пайплайны «модель проверяет модель».
Почему обвязки так дороги: задача гоняется по множеству проходов (генерация → критика → переписывание), а выходные токены у рассуждающих моделей — самые дорогие. «Совет» из трёх моделей просто умножает эти расходы на число участников. Деньги в такой конфигурации покупают подтверждение в пределах общего слепого угла, а не новое знание.
Что с этим делать инженеру
Диагноз без рецепта — красивая эпитафия. Здесь дефициты довольно конкретны, значит, под них можно подложить инженерные решения. Базовая идея: компенсировать отсутствие интуиции и независимой проверки внешним детерминированным контуром, который живёт вне весов модели.
Рис. 3. Корреляция проверок внутри одного семейства vs ортогональная внешняя верификация.
Считать вывод LLM гипотезой. Любой формальный результат модели — это кандидат, который требует внешней верификации.
Не упираться в «модель проверяет модель» внутри близких семейств. Нужны ортогональные механизмы ошибки: в математике — формальные верификаторы (Lean, Coq, Isabelle), где каждое логическое действие проверяет машина; в коде — компиляторы, типы, тесты, статический анализ.
Триангуляция вместо размножения. Если строите ансамбль, берите источники с разными механизмами ошибки: формальный верификатор + человек + LLM. Цель — чтобы проверяющий был структурно ортогонален генератору, а не его слегка модифицированной копией.
Скепсис к авторитету оформления. Модели отлично имитируют строгий LaTeX-стиль и журнальные шаблоны. Аккуратная вёрстка не является аргументом. Формула «следует из стандартных рассуждений» — повод вручную пройти этот шаг, а не расслабиться.
Практически удобно держать три уровня доверия:
Что используем | Можно ли доверять |
|---|---|
Идеи и черновики | Годится — но с обязательной человеческой фильтрацией |
Формальные результаты | Приемлемо только в связке «LLM + proof assistant / тесты / сверка с известными результатами» |
Safety-критичное, инфраструктура, публикация теорем | Неприемлемо, если единственный источник истины — модель |
Как применить выводы First Proof к ML-сервису с LLM
Рассмотрим типичный сценарий: у вас есть ML-сервис (рекомендательная система, скоринг, internal-инструмент), в который вы добавляете LLM как «мозг» для генерации правил, фичей, SQL, конфигов, текстов. First Proof подсказывает, где именно нельзя доверять модели и как это обойти.
LLM как генератор гипотез, а не прод-логики
LLM генерирует кусок логики: SQL-запрос, фичу, правило скоринга, конфигурацию пайплайна.
Этот артефакт никогда не идёт прямо в прод — он попадает в стадию «sandbox + тесты»: SQL гоняется на тест-базе и проходит статический анализ (нет DROP/TRUNCATE, full-scan на больших таблицах, доступ только к whitelisted-схемам); фичи проверяются офлайн (распределения, корреляции, data leakage, PSI/KS на train vs prod); конфиги валидируются схемой (JSON Schema / Pydantic) и dry-run пайплайна.
В прод перетекает только то, что прошло валидаторы и ревью.
Псевдокод CI-конвейера:
stages:
- generate
- validate
- offline_eval
generate_llm_candidates:
stage: generate
script:
- python tools/gen_rules_with_llm.py
--backend internal-llm-proxy
--out artifacts/llm_rules.yaml
artifacts:
paths: [artifacts/llm_rules.yaml]
validate_rules:
stage: validate
needs: ["generate_llm_candidates"]
script:
- python tools/validate_rules_schema.py artifacts/llm_rules.yaml
- python tools/security_lint_rules.py artifacts/llm_rules.yaml
- python tools/dryrun_rules_sql.py
--rules artifacts/llm_rules.yaml
--dsn $TEST_DB_DSN
artifacts:
paths: [artifacts/valid_rules.yaml]
offline_eval:
stage: offline_eval
needs: ["validate_rules"]
script:
- python training/train_with_rules.py
--rules artifacts/valid_rules.yaml
--baseline recsys_v1
--out recsys_v1_llm_rules
- python eval/offline_eval.py
--baseline recsys_v1
--candidate recsys_v1_llm_rules
--metrics-out artifacts/metrics.json
- python tools/check_metrics_thresholds.py artifacts/metrics.json
Здесь LLM участвует только на шаге generate_llm_candidates: он генерирует гипотезы (правила/SQL), но не решает, что уйдёт в прод. Решение принимают схема, security-lint, dry-run на тестовой базе и офлайн-оценка модели — ровно то, чего не хватало First Proof, где «следует из стандартных рассуждений» часто проходило без реальной проверки.
Прогноз на третий батч (чтобы не было «задним числом»)
Чтобы избежать ретроспективной подгонки «мы же говорили», полезно зафиксировать проверяемые ожидания на третий батч (анонсирован на август–октябрь 2026).
Успехи будут кластеризоваться в областях с плотным покрытием литературой.
Провалы останутся там, где нужен новый ключевой приём без близкого аналога.
Галлюцинированные и пропущенные ссылки сохранятся как массовый паттерн.
«Советы» из близких семейств дадут небольшой прирост качества при кратном росте цены и не пробьют потолок голой модели.
Условие фальсификации: если публичная модель в режиме one-shot решит задачу, специально сконструированную так, чтобы требовать нового кросс-доменного приёма без ближайших аналогов в литературе, придётся существенно смягчить тезис «у моделей нет фазы открытия». Это и будет отличать проверяемую теорию от красивой ретроспективной рамки.
Чего этот тест не доказывает
Важно проговорить не только то, что First Proof показывает, но и то, чего он не показывает.
Одна из систем уже дала новое безупречное доказательство (задача 5). В узких областях с хорошо покрытой литературой модели способны делать публикабельную работу.
В тест не пустили сильнейшие системы (Aletheia, полная Claude Mythos). Потолок доступного не равен потолку существующего.
Это срез одного момента времени. Третий batch запланирован на август–октябрь 2026, и только там станет видно динамику.
Бенчмарк меряет автономный one-shot. В диалоге с живым математиком результат может быть другим — но тогда модель выступает как инструмент, а не как автономный решатель.
Вместо финала
Фраза «ИИ уступает человеку в сложных задачах» ничего не объясняет. Более точное описание: на хорошо спроектированном бенчмарке современные публичные модели в автономном режиме аккуратно делают лёгкое, перескакивают трудное, галлюцинируют ссылки, копируют без атрибуции и иногда уверенно доказывают ложь — и всё это на той половине математики (доказательство), где у них формальная фора.
Разрыв с человеком — не туманная «недостаточная общая интеллектуальность», а набор вполне конкретных дефицитов: нет фазы открытия, нет локализации трудности, нет границы между «вспомнил похожее» и «доказал новое», плюс иллюзия независимости проверок в ансамблях. Каждый из этих пунктов описан задолго до First Proof — Пуанкаре, Оакли, Бернштейном, ТРИЗ и работами о коррелированных ошибках.
Поэтому главный артефакт бенчмарка — не таблица очков, а рецензентские разборы и ссылки на источники: они показывают не «на сколько» ИИ отстаёт, а «где и как» он ошибается. И ни одно из этих «где» не оказалось новым.
Источники
Отчёт First Proof Second Batch, 1stproof.org, 10 июня 2026.
D. Castelvecchi, «Humans outperform AI at this highly rigorous mathematics test», Nature, 12 июня 2026.
А. Пуанкаре, «Наука и метод» (очерк «Математическое творчество»).
Б. Оакли, «A Mind for Numbers»; курс Learning How to Learn.
Н. А. Бернштейн, «О построении движений» (1947).
Г. С. Альтшуллер, основы ТРИЗ.
Kim, Garg, Peng, Garg, «Correlated Errors in Large Language Models», arXiv:2506.07962 (ICML 2025). Прим.: работу часто ошибочно приписывают «Goel et al.» — это разные статьи.
«Более 150 математиков призвали не верить в научные доказательства ИИ», SecurityLab, 2026.
Если хотите быть в курсе современных технологий и индустриальных решений (Best Practices) по DevOps, AI и AI-агентам — подписывайтесь на мои Telegram-каналы:
Русскоязычный — DevOps-Best-Practices: t.me/devops_best_practices (@devops_best_practices)
Англоязычный — DevOps Hot News Global: t.me/devops_world_news (@devops_world_news)