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