Исторический прорыв в верификации математики
Команда Anthropic совместно с исследователями Колумбийского университета (в частности, Тяни Пэном) и математиком Кевином Баззардом из Имперского колледжа Лондона завершила формализацию доказательства Эндрю Уайлса 1995 года. В отличие от предыдущих попыток, которые могли занимать годы, Claude справилась с задачей за 11 дней, работая в режиме «почти полностью автономно».
Ключевое отличие этой работы — не в создании новой математики, а в верификации. ИИ перевел сложнейшие логические цепочки в формат, который компьютер может проверить алгоритмически, исключая человеческие ошибки. Как отметил Кевин Баззард, это доказывает, что артефакты автоформализации стали достаточно надежными для построения многоуровневых доказательств.
Масштаб работы: цифры и метрики
Объем сгенерированного кода и доказанных утверждений поражает. Доказательство Claude превышает размер основной библиотеки математических доказательств Mathlib более чем в 5 раз. ИИ использовал около 6 миллиардов выходных токенов внутренней исследовательской модели общего назначения.
| Параметр | Значение / Описание |
|---|---|
| Время работы | 11 дней (автономный режим) |
| Язык формализации | Lean (proof assistant) |
| Объем кода | 13 000 000 строк (в 5+ раз больше Mathlib) |
| Промежуточные теоремы | 29 500 (из 30 300 сгенерированных) |
| Использованные токены | ~6 миллиардов (output tokens) |
| Неудачные попытки | ~7% строк (агенты теряли контекст до внедрения Prove2Me) |
Роль платформы Prove2Me и многоагентной архитектуры
Успех стал возможен благодаря внедрению платформы Prove2Me, разработанной Тяни Пэном. Она решала критические проблемы масштабирования ИИ-математики:
- Управление состоянием: Платформа поддерживала направленный ациклический граф (DAG) утверждений, помогая агентам решать, какие доказательства строить дальше, и предотвращая «деградацию памяти».
- Оптимизация ресурсов: Разделение утверждений и доказательств по разным файлам ускорило компиляцию Lean и снизило потребление ресурсов.
- Поиск и переиспользование: Натуральноязыковые описания теорем позволили агентам эффективнее находить готовые решения.
Человеческий вклад ограничился высокими инструкциями, такими как: «Якобиан как схема — высокий приоритет» или «Поторопись с теоремой Мазура».
Почему это важно для науки
Доказательство Уайлса (1995) занимало 129 страниц и требовало месяцев ручной проверки. Ошибка в одном звене логической цепи могла сделать неверным всё, что следует за ним. Формализация FLT показывает, что ИИ способен брать на себя рутинную, но критически важную работу по проверке корректности сложных математических выкладок.
Это открывает путь к будущему, где проверка новых математических результатов станет быстрее и надежнее. Если ИИ сможет автоматически формализовывать доказательства, бремя оценки новых открытий, которое сейчас ложится на плечи узкого круга экспертов, значительно снизится, повышая доверие к научному знанию.
Источник: Anthropic ↗