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