Microsoft Research сообщила о доказательстве гипотезы KLS с помощью ИИ-агентов

Microsoft Research объявила, что решена гипотеза Каннана, Ловаса, Симоновица (KLS), предложенная в 1995 году. В блоге её называют 31-летней проблемой, которую широко считают одним из центральных открытых вопросов многомерной геометрии. Доказательство получили двое исследователей, среди которых Xinzhi Zhang из группы машинного обучения и оптимизации Microsoft Research. Работа шла по схеме «человек направляет ИИ-агентов».

Суть гипотезы: для широкого класса многомерных вероятностных распределений лучший плоский разрез (по гиперплоскости) почти так же эффективен, как лучший разрез любой формы. KLS предсказывает, что они различаются не более чем на универсальную константу, независимо от числа измерений. Поскольку геометрия таких разрезов определяет, как быстро случайные блуждания исследуют распределение, гипотеза важна и для теории многомерной выборки. Авторы показали, что соотношение выполняется с фиксированной границей при любом числе измерений. Лучший прежний результат, полученный в июле 2026 года, допускал медленный рост этой границы с ростом размерности.

Ход доказательства. Сначала авторы пытались уточнить июльский результат. Вместе с ИИ-агентами в структурированном процессе под управлением людей они изучили более 100 вариантов подходов, многие из которых требовали громоздких вычислений с тензорами высших порядков. Так получился новый математический критерий, ставший основой доказательства. Затем выяснилось, что критерий можно применять рекурсивно: каждую улучшенную оценку подставляют в тот же аргумент и получают ещё более точную. В версии статьи от 1 октября 2026 года это свело зависимость от размерности к итерированному логарифму. Он растёт чрезвычайно медленно, но всё же растёт, поэтому гипотезу это ещё не закрывало. Завершающий шаг, повторить всю рекурсивную процедуру целиком, а не один раз; идею авторам подсказала их прежняя работа о быстрых алгоритмах линейного программирования. Они доказали, что малые ошибки каждого этапа убывают достаточно быстро и их сумма ограничена универсальной константой, не зависящей от размерности. Это убрало зависимость от числа измерений и завершило доказательство в версии от 4 октября 2026 года.

Роль ИИ. По тексту блога, рекурсивный метод, его повторное применение и доказательство ограниченности накопленных ошибок, оригинальный вклад исследователей. ИИ помогал перебирать подходы, проводить подробные выкладки, готовить рукопись и выполнять внутренние проверки доказательства. Направление, отбор перспективных идей, сборку итогового аргумента и проверку доказательства взяли на себя люди. Агенты параллельно исследовали варианты идеи, исследователь просматривал промежуточные результаты, отсекал бесперспективные направления («прунинг», отсечение ветвей) и передавал лучший результат в следующий раунд. До ключевого прорыва прошло примерно сто исследовательских траекторий. В отдельной ветви проекта авторы много раз без руководства пытались решить задачу с помощью нескольких ведущих ИИ-моделей, потратив примерно столько же токенов, сколько в основном процессе, и цели не достигли.

Независимое подтверждение. В день, когда авторы выложили полное доказательство, отдельная группа ведущих экспертов выложила собственное полное доказательство, разработанное параллельно. Оно опиралось на первую версию статьи Microsoft, назвав её «решающим шагом доказательства». Третье доказательство, появившееся в тот же день, использует близкую идею. Позже вышла формализация в Lean 4, объединившая ключевой критерий из первой статьи Microsoft с дополнительными исследованиями. Авторы также сократили своё доказательство и проверили упрощённый вариант в Lean; обе версии они собираются опубликовать после финальной проверки.

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

Ключевые факты

Гипотеза KLS (1995) утверждает, что лучший плоский разрез отличается от лучшего разреза любой формы не более чем на универсальную константу при любой размерности; Microsoft Research сообщает о доказательстве с фиксированной границей.
Путь к результату: более 100 подходов с ИИ-агентами, затем рекурсивное применение нового критерия, версия от 1 октября 2026 года дала итерированный логарифм, версия от 4 октября 2026 года убрала зависимость от размерности.
Люди выбирали направление и проверяли доказательство, а агенты перебирали варианты и делали выкладки; неуправляемые попытки нескольких ведущих ИИ-моделей с похожим бюджетом токенов цели не достигли.
В тот же день независимая группа экспертов выложила полное доказательство, опирающееся на первую статью Microsoft, появилось и третье доказательство; позже вышла формализация в Lean 4.
Результаты, ранее зависевшие от гипотезы как от допущения, теперь можно формулировать безусловно.

Почему это важно

Гипотеза KLS почти тридцать лет считалась одним из центральных открытых вопросов многомерной геометрии. Её значение подчёркивали Mathematical Sciences Research Institute (MSRI), Simons Institute и Quanta Magazine, а Ronen Eldan в трудах Международного конгресса математиков 2022 года отмечал её широкие следствия. Если доказательство подтвердится, пространства высокой размерности ведут себя лучше, чем было известно: препятствия при перемещении по ним не растут неограниченно с числом измерений. Второй пласт новости, способ получения результата: по описанию Microsoft, прорыв дал процесс, где люди направляют ИИ-агентов, а не один запуск модели на всю задачу.

Кому это важно

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

Как это применить

Практический урок из описания процесса: агентов запускают параллельно на вариациях одной идеи, исследователь просматривает промежуточные результаты, отбрасывает бесперспективные и передаёт лучший в следующий раунд. По словам авторов, до прорыва прошло примерно сто траекторий. Проверка результата строилась на нескольких независимых доказательствах и на формализации в Lean 4. Названий моделей и продуктов, использованных агентами, источник не приводит, поэтому воспроизвести настройку по тексту блога нельзя.

Можно ли доверять

Источник, блог самой Microsoft Research, то есть рассказ заинтересованной стороны о собственной работе. Однако в нём названы проверяемые признаки: даты версий статьи (1 и 4 октября 2026 года), параллельное полное доказательство отдельной группы экспертов, третье доказательство с близкой идеей и формализация в Lean 4. Оговорки: источник не называет независимую группу, авторов третьего доказательства и формализации, не сообщает о рецензировании или принятии в журнале и не приводит численное значение константы. Второй из двух исследователей по имени не указан; Zhao Song упомянут как соавтор в благодарностях.

Риски и подводные камни

Версия от 1 октября 2026 года ещё не решала гипотезу: зависимость от размерности сохранялась в виде итерированного логарифма, и полное доказательство появилось только 4 октября. Упрощённое доказательство и его проверка в Lean пока не опубликованы, авторы собираются выложить их после финальной проверки. Вывод о роли ИИ следует читать осторожно: в отдельной ветви неуправляемые попытки нескольких ведущих моделей при сопоставимом бюджете не удались, и авторы связывают успех как с возможностями ИИ, так и с математическим чутьём исследователей. Заявление о доказательстве принадлежит самой компании и ещё не получило публичного подтверждения со стороны рецензируемого журнала.

«Центральная открытая проблема многомерной выпуклой геометрии.»

— Mathematical Sciences Research Institute (MSRI), годовой отчёт 2017-18, о гипотезе KLS (цитата из блога Microsoft Research)