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