Гипотезу KLS доказали с помощью ИИ-агентов и математического анализа

Исследователь Microsoft Research Синьчжи Чжан и независимый исследователь Чжао Сун представили доказательство гипотезы Каннана — Ловаса — Симоновица (KLS), сформулированной в 1995 году. Она считается одной из важных задач геометрии высоких размерностей и связана с тем, насколько быстро случайные алгоритмы исследуют сложные пространства.

В работе использовали ИИ-агентов, которые параллельно перебирали математические подходы, выполняли вычисления и проверяли промежуточные рассуждения. Однако окончательные решения оставались за исследователями: они оценивали полученные результаты, отбрасывали слабые идеи и направляли поиск в более перспективные области.

Что утверждает гипотеза KLS

Если упростить формулировку, гипотеза утверждает, что для определённого класса многомерных распределений простой плоский разрез позволяет оценить самое узкое место пространства с точностью до постоянного множителя. Важно, что этот множитель не должен увеличиваться вместе с числом измерений.

Геометрия таких «узких мест» влияет на скорость смешивания случайных блужданий — алгоритмов, применяемых для выборки из сложных распределений, оценки объёмов выпуклых тел и решения задач оптимизации. Доказательство KLS позволяет убрать дополнительное предположение из ряда теоретических результатов, которые ранее опирались на недоказанную гипотезу.

Как исследователи искали решение

По данным Microsoft Research, учёные рассмотрели более ста возможных направлений. Многие из них требовали громоздких вычислений с тензорами высокого порядка. В ходе работы исследователи сформулировали новый математический критерий, который затем стал основой доказательства.

Авторы применили рекурсивное уточнение оценок: результат одного шага использовался для улучшения следующего. В финале процедуру пришлось применить повторно. Исследователи доказали, что ошибки, возникающие при таком подходе, остаются ограниченными постоянной величиной независимо от размерности пространства. Именно этот ключевой этап был разработан людьми, а не получен автоматически от ИИ.

В отдельной серии экспериментов ведущие языковые модели пытались решить задачу без руководства исследователей и при сопоставимом бюджете токенов. Самостоятельно получить доказательство они не смогли.

Другие доказательства и проверка в Lean

Работа появилась на arXiv в начале октября, а 21 октября Microsoft Research опубликовала более подробное описание результата. В тот же день другая группа математиков представила собственное доказательство. Её участники назвали критерий Суна и Чжана ключевым шагом к решению задачи. Позднее появилось и третье доказательство, основанное на близкой идее.

Кроме того, была опубликована формализация результата в системе Lean 4. Авторы работы Microsoft сообщили, что проверили в Lean сокращённую версию своего доказательства и готовят её к публикации. Пока все эти материалы остаются препринтами, а не рецензированными журнальными статьями. Тем не менее независимые доказательства и формальная проверка в Lean усиливают основания считать результат корректным.