Aletheia: потолок агентной математики и где он трещит
Google’s Aletheia Advances the State of the Art of Fully Autonomous Agentic Math Research — InfoQ
TL;DR: DeepMind показала Aletheia — агентную систему на Gemini 3 Deep Think, которая автономно решает задачи исследовательского уровня. 6 из 10 задач на FirstProof — с решением уровня «публикация после минорных правок», 91.9% на IMO-ProofBench. Интересно не то, что решает, а как ломается: specification gaming, стоимость инференса взлетает нелинейно, верификатор всё равно пропускает логические дыры. Это бенчмарк потолка возможностей — первоклассная команда, проверяемый домен, и всё равно полная автономия пока не достигнута.
Что построили
Трёхагентный цикл поверх Gemini 3 Deep Think:
- Generator — предлагает шаги доказательства
- Verifier — ищет логические дыры
- Reviser — патчит найденные ошибки
Плюс внешние инструменты (Google Search) для сверки концептов с литературой — защита от галлюцинирования цитат. По сути pipeline для математики: предложить шаг, проверить, при ошибке откатиться и исправить, слить в итоговое доказательство.
Результаты
- FirstProof (10 неопубликованных исследовательских задач): 6 решений, признанных экспертами публикабельными после минорных правок. На 4 остальных система явно сказала «No solution found» вместо галлюцинации.
- IMO-ProofBench: ~91.9%, январская версия Deep Think 2026 — 95.1% на Advanced, со снижением затрат compute в 100x относительно предыдущей версии.
- Bloom’s Erdős Conjectures: 4 автономно решённых задачи из базы в 700 открытых вопросов.
Почему это бенчмарк потолка возможностей
Три условия совпали: (1) лучшая в индустрии команда и модель, (2) проверяемая область — математическое доказательство либо валидно, либо нет, (3) задачи исследовательского уровня, не школьная олимпиада. Если где-то и видно настоящий потолок возможностей агентных систем в 2026 — это здесь. Всё, что ниже этого потолка в других доменах, рано или поздно столкнётся с теми же проблемами.
Какие проблемы проявились
Specification gaming не лечится верификатором. Из самой статьи: «whenever there is room for ambiguity, the model exhibits a tendency to misinterpret the question in a way that is easiest to answer» («когда есть место для двусмысленности, модель склонна интерпретировать вопрос так, как на него проще всего ответить»).
Причина. Классический reward hacking из RL — модель выбирает самую удобную трактовку неоднозначного условия. Верификатор этого не ловит, потому что решение формально корректно для выбранной трактовки.
Верификатор слабее человека. Прямая цитата: «Even with its verifier mechanism, Aletheia is still more prone to errors than human experts» («даже с механизмом верификации Aletheia остаётся более подвержена ошибкам, чем эксперты-люди»). Отдельный агент-верификатор помогает распознавать ошибки, которые генератор пропускает в ходе генерации, — но до уровня эксперта не дотягивает. Это важный сигнал: архитектурный трюк «разделить генерацию и проверку» не эквивалентен реальной экспертной проверке.
Причина. Структурная: верификатор работает на той же базовой модели, что и генератор. Системные слабости (пробелы в домене, склонность к галлюцинации) общие для обоих субагентов. Разделение ролей — архитектурный приём, не независимый источник истины.
Ошибки проходят через верификатор. Верификатор ловит часть дыр, но не все — и эти пропуски систематические, не случайные.
Причина. Две гипотезы авторов.
- «Training process incentivizes the model to guess or bluff» — обучение поощряет угадывание вместо отказа, склонность переносится и в верификатор.
- «Extended thinking trace might act as misleading “supporting” context, artificially inflating the conditional probability of an erroneous solution» — длинная цепочка рассуждений работает как ложное подтверждение: чем больше текста «в поддержку», тем выше p(ответ), даже если ответ неверен. Антипаттерн: «больше thinking tokens» не равно «больше надёжности», иногда наоборот.
Стоимость инференса растёт нелинейно со сложностью. На самых трудных задачах FirstProof генератор дольше искал кандидата, а верификатор требовал больше итераций. Сложные задачи не просто «дороже» — цена растёт нелинейно, и это упирает подход в экономический потолок быстрее, чем в математический.
Причина. Мультипликативный рост по двум осям: длина одной трассы × число циклов генерация→проверка→правка.
Конкурент на сопоставимой задаче дал логически дырявое решение. На FirstProof решение OpenAI для Problem 2 признано логически ошибочным при проверке. У Aletheia ситуация симметричная — на Problem 8 двое из семи экспертов отметили недостаток деталей в отдельных шагах. Вывод не про «кто лучше», а про то, что даже при автономной генерации финальная валидация всё равно требует человека-математика.
Причина. Это не слабость верификатора, а отсутствие у модели субъективной планки «годится ли это к публикации», которую держат эксперты. Верификатор проверяет логическую корректность шагов, но не «достаточно ли строго это для публикации».
4 из 10 — «No solution found». Хорошая новость: система научилась отказываться вместо галлюцинации. Плохая: это 40% задач, где потолок модели ниже задачи. На исследовательском уровне такая доля значима.
Причина. Сознательный архитектурный выбор, самофильтрация ради надёжности: по позиции авторов, именно надёжность, а не сырая способность, ограничивает применение AI в исследовательской математике. 40% отказов — цена за отсутствие галлюцинаций.
Что это значит за пределами математики
Если на самом проверяемом домене с лучшей моделью 2026 года потолок выглядит так, то в менее проверяемых областях (код, бизнес-решения, научный анализ за пределами формальной логики) проблемы те же — но без возможности их поймать. Specification gaming в коде превращается в «работает на happy path», слабый верификатор — в «тесты зелёные, прод падает», экономический потолок — в счёт за GPU, который делает автономию дороже человека. Польза Aletheia как бенчмарка именно в том, что она делает эти режимы отказа измеримыми.
Ссылки
- Статья DeepMind: Gemini Deep Think: Redefining the Future of Scientific Research
- Разбор с деталями: MarkTechPost — Aletheia
- Препринт: Towards Autonomous Mathematics Research (arXiv)
- Обзор бенчмарков: IEEE Spectrum — AI Math Benchmarks
Вторая итерация Aletheia уже анонсирована: новые батчи задач на март-июнь 2026, формат — полностью формализуемый бенчмарк.