10 июля, на следующий день после публичного запуска GPT-5.6 Sol Ultra, OpenAI заявила, что ее флагманская модель нашла доказательство гипотезы о двойном покрытии циклами — одной из самых известных открытых задач теории графов, стоявшей около полувека. По словам сотрудника OpenAI Итана Найта, модель справилась меньше чем за час, задействовав 64 параллельных сабагента. Сразу стоит отметить, что пока доказательство только проходит проверку математиками — и на данном этапе больше интересен подход, который OpenAI применила при решении задачи.
Но сначала о самой гипотезе. Возьмем граф без мостов — то есть без ребер, удаление которых разваливает его на части. Гипотеза утверждает: в любом таком графе найдется набор циклов, который покрывает каждое ребро ровно два раза. Ее независимо выдвигали Джордж Секереш в 1973 году и Пол Сеймур в 1979-м; в статье OpenAI среди авторов гипотезы называют также Татта и пару Итаи—Родех. Простота обманчива: сформулировать гипотезу можно за минуту, а полностью доказать не получалось ни у кого пятьдесят лет.
При этом математики закрыли множество частных случаев: гипотеза верна для планарных графов, для кубических графов с правильной раскраской ребер в три цвета, для графов без подразделения графа Петерсена. Но общий случай упирался в так называемые снарки — вредный класс графов, для которого не работают стандартные приемы. Попыток полного доказательства тоже хватало, — и все они рано или поздно разваливались при проверке.
Что предъявила OpenAI? Доказательство занимает три страницы и устроено на удивление классически. Сначала стандартное сведение задачи к кубическим графам — тем, где из каждой вершины выходит ровно три ребра, — известное из работ Франсуа Джагера. Затем — теорема о 8-потоке, классический результат Килпатрика и Джагера середины 1970-х, позволяющий согласованно разметить ребра любого графа без мостов. Ключевой ход — превратить эту разметку в другую: каждому ребру назначается пара элементов небольшого векторного пространства так, чтобы вокруг каждой вершины все сходилось, а финальное препятствие снимается элементарной линейной алгеброй. В документе отдельно оговорено: за доказательство отвечала версия модели Sol Ultra, а оформлением текста занимался Codex в связке с обычной GPT-5.6 Sol.
Интересно, что все инструменты доказательства существовали к середине 1980-х: никакой новой теории, никаких результатов последних десятилетий, только техника, которой владеет любой специалист по теории графов. Если доказательство верно, получается, что решение около сорока лет лежало на поверхности — и поколения специалистов, включая авторов самой гипотезы, просто прошли мимо короткой комбинации известных идей. Такое в истории математики случалось, но редко.
Не менее любопытен использованный промпт — он отличается от большинства приемов работы с ИИ. Модели прямо говорят: «считай, что полное доказательство существует», запрещают возвращаться с частичными результатами, с редукцией задачи к другим недоказанным гипотезам и объяснениями, почему задача трудна. Отдельно запрещено гуглить решение и отвечать, что проблема открыта. По сути, у модели отобрали все пути к отступлению, которыми часто заканчиваются такие сессии.
Вторая половина промпта — про управление роем из 64 агентов. На старте их проинструктировали работать независимо — это сделано, чтобы агенты не сосредоточились на одной красивой, но тупиковой идее. Для этого же ведется реестр семейств подходов; заблокированные направления открываются заново только при появлении принципиально нового механизма. Каждое доказательство-кандидат атакуют adversarial-агенты — их работа искать типичные лазейки: краевые случаи, на которых конструкция ломается, объекты, которые лишь притворяются циклами, и рассуждения, где гипотеза незаметно доказывается через саму себя.
Финальный штрих — инструкция «потрать минимум 8 часов, прежде чем даже думать о возврате». Ее модель, строго говоря, не выполнила: ответ был готов меньше чем через час. Но следить за временем модели толком не умеют, и такие указания работают не как таймер, а как прием, чтобы модель не сдалась слишком рано — в паре с «считай, что доказательство существует» из начала промпта.
Доказательство не проходило рецензирование, формальной верификации в Lean или другом пруф-ассистенте тоже не было — хотя часть изданий уже успела назвать его «machine-verified», это неточность. Обсуждение на Hacker News собрало больше 200 комментариев, где восторги перемешаны с напоминаниями, что верифицировал результат «пока никто».
В пользу компании играет свежий прецедент. В мае модель OpenAI опровергла в задаче Эрдеша №90 о единичных расстояниях — одной из самых знаменитых в комбинаторной геометрии — ответ, которого ждали почти 80 лет, и тот результат проверку выдержал: его верифицировал Томас Блум, дорабатывал принстонский математик Уилл Савин (Will Sawin), а филдсовский лауреат Тимоти Гауэрс назвал вехой. Против — вся история гипотезы, хоронившей доказательства и покрепче. Точнее всех пока формулирует Википедия: в статью о гипотезе добавили строчку, что OpenAI «заявила» о решении, — и это слово там несет основную смысловую нагрузку.
Впрочем, доказательство короткое, техника классическая, поэтому есть шанс увидеть проверку уже в ближайшие дни. Если доказательство устоит, это будет самый громкий математический результат языковой модели — громче даже майского: там модель опровергла ожидаемый ответ, но сама задача Эрдеша осталась открытой, а здесь именованная гипотеза с полувековой историей закрывается целиком. Если нет — гипотеза о двойном покрытии циклами просто пополнит свою коллекцию несостоявшихся доказательств, на этот раз впервые — машинным.
P.S. Поддержать меня можно подпиской на канал «сбежавшая нейросеть», где я рассказываю про ИИ с творческой стороны.
ссылка на оригинал статьи https://habr.com/ru/articles/1058194/