ИИ-агенты помогли доказать гипотезу KLS спустя 31 год
Исследователь Microsoft Research Синьчжи Чжан и независимый исследователь Чжао Сун представили доказательство гипотезы Каннана — Ловаса — Симоновица (KLS). Проблема была сформулирована в 1995 году и более трёх десятилетий оставалась нерешённой.
Гипотеза относится к геометрии многомерных пространств и описывает свойства определённого класса распределений. В упрощённой формулировке она утверждает, что простой плоский разрез позволяет оценить самое узкое место пространства с точностью до постоянного множителя, который не увеличивается вместе с числом измерений.
Этот результат важен не только с теоретической точки зрения. Геометрия узких областей влияет на скорость смешивания случайных блужданий — алгоритмов, применяемых для выборки из сложных распределений, оценки объёмов выпуклых тел и решения задач оптимизации. Доказательство KLS позволяет убрать дополнительное предположение из ряда математических результатов, которые ранее опирались на эту гипотезу.
Какую роль сыграли ИИ-агенты
В ходе работы исследователи рассмотрели более ста возможных подходов. Многие из них требовали сложных вычислений с тензорами высокого порядка. При поиске решений учёные использовали ИИ-агентов, которые параллельно исследовали математические направления, проводили вычисления и помогали проверять промежуточные рассуждения.
Ключевые решения при этом оставались за людьми. Исследователи оценивали полученные результаты, отбрасывали слабые идеи и направляли работу в наиболее перспективные области. В результате поиска появился новый математический критерий, ставший основой доказательства.
Финальная конструкция использует рекурсивное уточнение оценок: результат одного шага применяется для улучшения следующего. Затем вся процедура запускается повторно. Авторы доказали, что ошибки, накапливающиеся в процессе, остаются ограниченными постоянной величиной и не зависят от размерности пространства.
Авторы также сравнили этот подход с автономной работой ведущих ИИ-моделей. В отдельной серии экспериментов моделям выделили сопоставимый бюджет токенов и предложили решить задачу без руководства исследователей, однако самостоятельно справиться с ней они не смогли.
Независимая проверка результата
Доказательство опубликовано в виде препринта. В тот же день, когда появилась полная версия работы Суна и Чжана, другая группа математиков представила собственное доказательство и назвала новый критерий ключевым шагом к решению гипотезы. Позже появилась и третья работа, основанная на близкой идее.
Дополнительным подтверждением стала формализация результата в Lean 4 — системе для формальной проверки математических доказательств. Исследователи Microsoft сообщили, что проверили в Lean сокращённую версию своей работы и готовят её к публикации. Пока исследования не прошли журнальное рецензирование, однако независимые доказательства и формальная проверка укрепляют доверие к полученному результату.
