---
title:

Aletheia: стеля агентної математики і де вона тріщить

date: 2026-04-20
tags: [#ai, #benchmark, #gemini, #reasoning, #llm ]
draft: false
---

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 залишається більш схильною до помилок, ніж експерти-люди»). Окремий агент-верифікатор допомагає розпізнавати помилки, які генератор пропускає під час генерації, — але до рівня експерта не дотягує. Це важливий сигнал: архітектурний трюк «розділити генерацію і перевірку» не еквівалентний реальній експертній перевірці.

Причина. Структурна: верифікатор працює на тій же базовій моделі, що й генератор. Системні слабкості (прогалини в домені, схильність до галюцинацій) спільні для обох субагентів. Розподіл ролей — архітектурний прийом, не незалежне джерело істини.

Помилки проходять через верифікатор. Верифікатор ловить частину дір, але не всі — і ці пропуски систематичні, не випадкові.

Причина. Дві гіпотези авторів. (1) «Training process incentivizes the model to guess or bluff» — навчання заохочує вгадування замість відмови, схильність переноситься і у верифікатор. (2) «Extended thinking trace might act as misleading “supporting” context, artificially inflating the conditional probability of an erroneous solution» — довгий ланцюг міркувань працює як хибне підтвердження: чим більше тексту «на підтримку», тим вище p(відповідь), навіть якщо відповідь невірна. Антипатерн: «більше thinking tokens» не дорівнює «більше надійності», іноді навпаки.

Вартість інференсу зростає нелінійно зі складністю. На найважчих задачах FirstProof генератор довше шукав кандидата, а верифікатор вимагав більше ітерацій. Складні задачі не просто «дорожчі» — ціна зростає нелінійно, і це впирає підхід в економічну стелю швидше, ніж у математичну.

Причина. Мультиплікативне зростання по двох осях: довжина однієї траси × кількість циклів генерація→перевірка→правка. Не адитивно.

Конкурент на співставній задачі дав логічно дірявe рішення. На FirstProof рішення OpenAI для Problem 2 визнано логічно помилковим при перевірці. У Aletheia ситуація симетрична — на Problem 8 двоє з семи експертів відзначили брак деталей в окремих кроках. Висновок не про «хто кращий», а про те, що навіть при автономній генерації фінальна валідація все одно вимагає людини-математика.

Причина. Це не слабкість верифікатора, а відсутність у моделі суб’єктивної планки «чи годиться це до публікації», яку тримають експерти. Верифікатор перевіряє логічну коректність кроків, але не «чи достатньо це суворо для публікації».

4 з 10 — «No solution found». Хороша новина: система навчилася відмовлятися замість галюцинації. Погана: це 40% задач, де стеля моделі нижча за задачу. На дослідницькому рівні така частка значуща.

Причина. Свідомий архітектурний вибір, самофільтрація заради надійності: за позицією авторів, саме надійність, а не сира здатність, обмежує застосування AI в дослідницькій математиці. 40% відмов — ціна за відсутність галюцинацій.

Що це означає за межами математики

Якщо на найперевірнішому домені з найкращою моделлю 2026 року стеля виглядає так, то в менш перевірних областях (код, бізнес-рішення, наукова аналітика поза формальною логікою) проблеми ті ж — але без можливості їх впіймати. Specification gaming у коді перетворюється на «працює на happy path», слабкий верифікатор — на «тести зелені, прод падає», економічна стеля — на рахунок за GPU, який робить автономію дорожчою за людину. Користь Aletheia як бенчмарка саме в тому, що вона робить ці режими відмови вимірюваними.

Посилання

Друга ітерація Aletheia вже анонсована: нові батчі задач на березень–червень 2026, формат — повністю формалізований бенчмарк.