Google DeepMind представила результати дослідження, в якому її дослідницький агент AlphaProof Nexus продемонстрував здатність розв'язувати не олімпіадні приклади, а відкриті математичні проблеми дослідницького рівня. Система розв'язала 9 із 353 відкритих задач, пов'язаних з ім'ям угорського математика Пала Ердеша, причому дві з них залишалися без рішення 56 років. Крім цього, агент довів 44 з 492 відкритих гіпотез з Онлайн-енциклопедії цілочислових послідовностей (OEIS). За оцінкою авторів, обчислення для кожної розв'язаної задачі Ердеша обійшлися в кілька сотень доларів.

Дев'ять задач Ердеша та 44 гіпотези OEIS

Робота присвячена застосуванню великих мовних моделей для пошуку формальних доведень. Автори свідомо вийшли за межі стандартних олімпіадних завдань і перевірили підхід на дійсно відкритих проблемах, над якими математика б'ється роками. Успіх у 9 задачах Ердеша та 44 гіпотезах OEIS показує, що підхід придатний для дослідницької математики, а не лише для навчальних та змагальних прикладів. При цьому важливо, що більшість відкритих задач Ердеша агент розв'язати не зміг: нинішні успіхи зосереджені в областях, для яких уже існує розвинена бібліотека формалізованих результатів і складні міркування вдається розбити на окремі підзадачі.

Формальна перевірка замість переконливого пояснення

Ключова відмінність AlphaProof Nexus від звичайного чат-бота — використання Lean, мови та середовища для формалізації математичних доведень. ШІ пропонує доведення у формальному вигляді, після чого Lean перевіряє кожен логічний крок. Якщо перевірка виявляє помилку, агент отримує зворотний зв'язок і продовжує пошук. Переконливо написаного пояснення недостатньо: результат має пройти машинну перевірку за суворими логічними правилами. Саме ця петля «генерація — перевірка — корекція» робить процес придатним для реальної математики, а не для генерації правдоподібного тексту.

Архітектура: кілька агентів та еволюційний алгоритм

В AlphaProof Nexus кілька ШІ-агентів паралельно шукають рішення, перевіряють підходи та уточнюють доведення. У найскладнішій конфігурації їхню роботу координує еволюційний алгоритм, а для окремих етапів пошуку використовується AlphaProof — система автоматичного доведення теорем, розроблена Google DeepMind і заснована на навчанні з підкріпленням. Така багатоагентна архітектура дозволяє розподіляти пошук за різними стратегіями та відбирати найбільш перспективні гілки доведень.

Простий агент теж упорався — але дорожче

Автори окремо порівняли складну архітектуру з простішим агентом, який просто чергує генерацію доведень мовною моделлю та перевірку в Lean. При повторному аналізі дев'яти розв'язаних задач Ердеша простий агент теж упоровся з усіма дев'ятьма. Однак на найважчих завданнях його використання обходилося дорожче. Це вказує на те, що результат залежить не лише від можливостей самої мовної моделі, а й від організації пошуку доведення: складна архітектура економить обчислення на складних випадках.

Горизонти та межі

Можливості системи не обмежуються задачами Ердеша та гіпотезами OEIS. AlphaProof Nexus допомогла розв'язати відкриту задачу в алгебричній геометрії, покращити оцінку у випуклій оптимізації та виявити помилки у формалізації математичних тверджень, що траплялися в науковій літературі. Її також використовують у дослідженнях з теорії графів та квантової оптики. Водночас система успадковує обмеження мовних моделей: результати пошуку можуть сильно відрізнятися від спроби до спроби, а завдання, що вимагають розробки обширної нової теорії, залишаються за межами її можливостей. Автори вважають, що формальні доведення можуть стати способом залучити ШІ до справжньої математичної роботи, а не просто отримувати від нього відповіді.