Агенты Claude Opus 5.5 за 15 часов доказали в Lean более быстрый поиск кратчайших путей

Vals AI собрала десять агентов на базе Claude Opus 5.5, дала им общую доску сообщений и задачу: найти более быстрый алгоритм поиска кратчайших путей в ориентированном графе с неотрицательными вещественными весами и точными ответами — и полностью доказать корректность и оценку времени работы на Lean. Начальные роли у агентов были, но они могли перераспределять усилия, делиться находками, оспаривать чужие идеи и записывать тупиковые подходы, чтобы не повторять их.

Примерно через 15 часов и 733 сообщения команда представила алгоритм C-HD. Перед объявлением успеха требовались воспроизводимая сборка Lean и два независимых ревью; если бы улучшение доказать не удалось, агенты должны были сохранить частичный прогресс и перечислить нерешённое.

Улучшение асимптотическое и действует только в определённом диапазоне плотности графа. Вдоль профиля, где число рёбер близко к n·(log n)^(3/4), оценка C-HD — порядка n·(log n)^(11/12) против n·log n у Дейкстры; отношение старших членов растёт как корень двенадцатой степени из логарифма. Автор сразу оговаривается: это верхняя граница сложности, а не измеренное ускорение.

Идея алгоритма — ограниченный локальный поиск вдоль исходящих рёбер: вновь встреченные вершины, включая неисследованные листья при неудачных рёбрах, засчитываются в лимит поиска, а локальные инварианты и аккуратное удаление рёбер позволяют ограничить повторную работу. Для малых входов и вне доказанного диапазона агенты добавили отдельный алгоритм — Беллмана—Форда.

Оценку времени работы проверили инструментом Lean Comparator: он убеждается, что доказана именно заявленная теорема, используются только разрешённые аксиомы и результат принимается ядром Lean.

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

Изображение:

Изображение: Michel Bakni CC BY-SA 4.0 · Лицензия

Редактор перевода: Салтанов А.