Мы используем AlphaEvolve, агент кодирования на основе LLM, для поиска и проверки комбинаторных структур, улучшающих результаты по сложности приближенного решения определенных задач оптимизации.
Быстрые ссылки
- Бумага
- AlphaEvolve
- Делиться
В последнее время большие языковые модели (LLM) продемонстрировали удивительные возможности в соревновательной математике и соревновательном программировании, показав лучшие в мире результаты в обеих этих областях. Однако их успехи в математических открытиях — доказательстве новых теорем или обнаружении новых комбинаторных структур — были относительно немногочисленны (с некоторыми заметными исключениями [1, 2, 3]). Поскольку математика и теоретическая информатика требуют абсолютной корректности[94fb54], любой метод на основе ИИ, совершающий математические открытия, должен либо иметь доказательство корректности, которое может быть подтверждено вычислительными методами (без участия человека), либо иметь в процессе эксперта в предметной области, который подтвердит корректность.
В нашей недавней статье «Усиленное генерирование комбинаторных структур: приложения к теории сложности» мы демонстрируем, как агент кодирования на основе LLM может помочь обнаружить новые математические структуры, расширяющие границы нашего понимания теории сложности (подраздела теоретической информатики). В нашей работе используется AlphaEvolve, система, разработанная в Google DeepMind, которая использует LLM для итеративного развития кода. Используя петлю обратной связи, AlphaEvolve начинала с популяций фрагментов кода, оценивала структуры, создаваемые этими фрагментами, и использовала LLM для преобразования наиболее успешных фрагментов в лучшие решения. Этот подход привел к новым результатам в двух различных областях теории сложности: 1) улучшению современного состояния дел в отношении ограничения на нашу способность аппроксимировать результат (т.е. «неаппроксимируемость») задачи максимального разреза для 4 срезов (которую мы определяем как задачу MAX-4-CUT) и 2) ужесточению границ средней сложности подтверждающих свойств случайных графов.
Математические исследования с использованием искусственного интеллекта могут проводиться в следующих режимах:
- Человек прибегает к методу LLM для обобщения литературы, составления плана исследований, направленных на открытие новых теорем, или для непосредственного создания фрагментов (или целых) доказательств.
- Человек использует инструменты, созданные на основе искусственного интеллекта, такие как AlphaEvolve, для генерации более качественных элементов доказательства.
Наша работа относится ко второй категории, где мы получаем более качественные элементы доказательства с помощью AlphaEvolve, которые могут быть автоматически проверены компьютерной программой.
Сила подъема: от конечных конструкций к универсальным утверждениям
Основная проблема использования ИИ в теоретических исследованиях в области информатики заключается в универсальном характере изучаемых задач. Система ИИ может найти решение для конкретного случая проблемы — например, оптимальный маршрут для коммивояжера, посещающего 50 конкретных городов. Однако специалисты по информатике часто ищут теоремы, которые верны для всех случаев и размеров задач (обозначаемых как ∀n).
Как можно использовать AlphaEvolve для доказательства универсального утверждения? Ответ кроется в методе, известном как «подъем» (см. изображение ниже). Если рассматривать доказательство как длинную строку, то можно взять фрагмент доказательства (соответствующий определенной конечной структуре) и развить его для поддержки более сильного универсального утверждения, сохраняя при этом неизменным интерфейс с остальной частью доказательства. Преимущество этого подхода заключается в том, что для подтверждения общей корректности достаточно подтвердить корректность только той конечной структуры, которая была преобразована.
Поднятие иерархии структур: Преобразование конечных структур с использованием ИИ при сохранении неизменного интерфейса с более широким доказательством.
В теории сложности исследователи часто используют устоявшиеся доказательные системы, основанные на существовании конкретных, высокооптимизированных конечных структур. Если удается найти лучшую структуру, вся доказательная система «поднимает» это улучшение до лучшего универсального результата.
Ключевым примером этого является «упрощение с помощью гаджетов». Чтобы доказать, что целевая задача является вычислительно сложной (неразрешимой), исследователи пытаются сопоставить с ней известную неразрешимую исходную задачу, тем самым демонстрируя, что целевая задача как минимум так же сложна, как и исходная. Гаджет — это рецепт локального преобразования небольшого фрагмента исходной задачи в фрагмент целевой задачи. Эти гаджеты представляют собой конечные структуры, и поиск оптимального гаджета — это кропотливый процесс, часто выполняемый вручную.
Поручив AlphaEvolve задачу поиска более совершенных устройств, мы смогли обнаружить структуры, гораздо более сложные, чем те, которые были известны ранее. Эти конечные открытия, будучи вписанными в существующие математические модели, немедленно приводят к новым универсальным теоремам в теории сложности.
Новые теоремы в теории сложности
Мы применили эту методологию к задаче MAX-k-CUT. Дана графовая структура (сеть узлов и ребер), цель состоит в том, чтобы разбить узлы на k различных множеств таким образом, чтобы количество ребер, пересекающих разные множества, было максимальным. Это классическая неразрешимая (NP-трудная) задача, то есть мы не ожидаем найти эффективные алгоритмы, которые решают ее точно. Поэтому мы сосредоточились на алгоритмах аппроксимации — тех, которые эффективно находят решения, гарантированно близкие к оптимуму.
Ключевой вопрос: каков предел приближения?
MAX-4-CUT: Новый уровень технологий
Для задачи MAX-4-CUT (разбиение на четыре множества) предыдущий лучший известный результат показал, что аппроксимация решения с точностью до коэффициента 0,9883 является NP-трудной задачей. Для поиска нового способа уменьшения размерности задачи MAX-4-CUT был использован AlphaEvolve.
Система обнаружила сложную схему, включающую 19 переменных (узлов) со сложной системой взвешивания (некоторые связи имеют вес, в 1429 раз превышающий вес других). Это открытие установило новый предел неаппроксимируемости, равный 0,987.
Это улучшение может показаться незначительным, но в зрелой области теории сложности приближения подобные достижения часто требуют значительных новых методов или комбинаторных идей.
Устройство, найденное AlphaEvolve для уменьшения размера до MAX-4-CUT.
Графики средней твердости и Рамануджана
Мы также исследовали сложность задач в среднем , а не в худшем случае. В частности, мы изучали сложность подтверждения границ MAX-2-CUT (а также максимального независимого множества) разреженных случайных графов[3d54ef]. Недавние работы связали эту проблему с существованием специфических графов Рамануджана — детерминированных графов, которые «выглядят» как разреженные случайные графы. Они предположили, что существование графов Рамануджана с неестественно большими разрезами подразумевает, что подтверждение MAX-2-CUT случайного графа является вычислительно сложной задачей.
В предыдущих работах для поиска таких графов с количеством узлов до 10 использовалась компьютерная помощь. Для улучшения результатов требовалось найти более экстремальные графы Рамануджана с гораздо большим количеством узлов, что чрезвычайно сложно обнаружить и проверить. AlphaEvolve успешно преодолела это обширное пространство поиска, обнаружив графы Рамануджана с еще большими разрезами на целых 163 узлах.
Граф Рамануджана с четырьмя регулярными степенями свободы и большим 2-разрезом, найденный программой AlphaEvolve.
Эти открытия значительно улучшили нижние границы сложности для среднего случая. Кроме того, в сочетании с новыми алгоритмическими разработками (не основанными на ИИ) нам удалось практически решить задачу определения вычислительной сложности этих вопросов, совместив верхние и нижние границы с точностью до третьего знака после запятой.
Ключевая роль проверенной корректности
Ключевым отличием этой работы является то, что результаты сопровождаются доказательствами их корректности.
Когда от студента, обучающегося по программе LLM, требуется напрямую сгенерировать математическое доказательство, он часто создает набросок доказательства или аргумент, для проверки и завершения которого требуется существенное вмешательство человека. Галлюцинации или незначительные ошибки могут сделать результат бесполезным. Как уже упоминалось, стандарт правильности в математике является абсолютным.
В отличие от этого, используемый здесь подход применяет ИИ для обнаружения структуры внутри доказательства, а не самого доказательства. Достоверность окончательной теоремы зависит от двух компонентов: корректности структуры подъема и проверки обнаруженной структуры. Хотя структуры являются надежными, проверка структур, обнаруженных AlphaEvolve, требует больших вычислительных затрат.
Примечательно, что AlphaEvolve добилась 10 000-кратного ускорения процесса верификации за счет внедрения сложных стратегий ветвей и границ, а также оптимизации на системном уровне. Это колоссальное ускорение стало ключевым фактором в исследовании, позволив системе исследовать гораздо более крупные и сложные устройства.
Что особенно важно, окончательно обнаруженные устройства были проверены с использованием исходного алгоритма полного перебора, что гарантировало абсолютную корректность теорем.
Будущее теории с использованием искусственного интеллекта
Хотя эти предварительные результаты исследований далеки от окончательных выводов, они предполагают, что ИИ готов стать полезным помощником в математических открытиях. Мы наблюдали, как модели в AlphaEvolve генерируют сложные математические объекты, которые порой демонстрируют зачатки способности к рассуждению. Однако по мере перехода в эпоху, когда доказательства все чаще будут приписываться ИИ, важнейшая задача проверки станет серьезным узким местом.
Благодарности
Мы хотели бы поблагодарить Адама Жолта Вагнера, Сварата Чаудхури, Пасина Манурангси и Сушанта Сачдеву за помощь на различных этапах проекта.
В математике утверждение однозначно истинно или ложно, без возможности промежуточных состояний. Это контрастирует с рядом других применений ИИ, таких как написание эссе или создание произведений искусства, где существуют субъективные критерии правильности, и нет необходимости в абсолютной правильности.
Разреженный случайный граф генерируется путем случайного добавления ребер между парой узлов, причем каждому узлу гарантировано ровно d соседей для некоторого малого d .
Источник: research.google
