Anthropic использует модель Claude для формализации доказательства Великой теоремы Ферма
Портрет Пьера де Ферма работы Ролана Лефевра
Доказательство — это последовательность рассуждений, подтверждающих правильность математической гипотезы. Доказательство, которое рассматривала компания Anthropic, подтверждает гипотезу, называемую Великой теоремой Ферма. Эта гипотеза, впервые выдвинутая в 1637 году, фокусируется на свойствах положительных целых чисел. Она гласит: «Для любого натурального числа n > 2 уравнение aⁿ + bⁿ = cⁿ не имеет решений в целых ненулевых числах a, b, c».
Доказательство Великой теоремы Ферма было разработано в 1995 году математиком Эндрю Уайлсом. Оно занимает 129 страниц и потребовало нескольких месяцев работы для проверки. В рамках исследовательского проекта компании Anthropic доказательство Уайлса было формализовано, то есть компания преобразовала его в форму, которую можно автоматически проверять с помощью компьютеров. Формализация доказательств полезна, поскольку исключает возможность человеческой ошибки и упрощает обмен информацией между математиками.
Формализованное доказательство представляет собой фрагмент кода, написанный на языке программирования Lean. Это специализированный синтаксис, который математики используют для проверки гипотез. Доказательство, представленное Anthropic, состоит из 13 миллионов строк кода Lean, что делает его самым большим файлом такого рода за всю историю.
Важно отметить, что формализация сложна, так как доказательства, как правило, довольно лаконичны. В них отсутствуют некоторые пояснения, необходимые компьютеру для их понимания, что вынуждает разработчиков добавлять эти пояснения вручную. Другой источник сложности заключается в том, что аргументы в доказательстве часто основываются друг на друге. Это означает, что одна ошибочная строка кода может сделать весь последующий код недействительным.
Математики предполагали, что процесс формализации доказательства Уайлса займет несколько лет. По данным Anthropic, ее исследователи справились с задачей за 11 дней, используя внутреннюю исследовательскую модель. Примечательно, что модель справилась с задачей, используя лишь ограниченный объем предоставленных людьми исходных данных высокого уровня. В процессе работы над доказательством модель создала несколько десятков агентов, которые сгенерировали 6 миллиардов токенов. В ходе работы они доказали не менее 29'500 промежуточных теорем.
Первая попытка компании Anthropic формализовать доказательство Уайлса оказалась неудачной. По словам компании, прорыв произошел, когда она предоставила модели Claude доступ к инструменту с открытым исходным кодом под названием Prove2Me. Это программное обеспечение упрощает агентам искусственного интеллекта определение следующего оптимального шага в длительном процессе обработки. Prove2Me также помогает снизить затраты на вывод результатов.
«Мы видим автоформализацию алгебры, гармонического анализа, геометрии и теории чисел, и мы узнаём, что артефакты автоформализации ИИ теперь достаточно надёжны, чтобы на их основе можно было строить дальнейшие исследования; доказательство многоуровневое», — сказал Кевин Баззард, математик, чью работу языковая модель Claude использовала для создания своего формализованного доказательства.
Это достижение произошло спустя месяц после того, как компания Anthropic сообщила о другом математическом прорыве, осуществленном благодаря своей большой языковой модели. Компания использовала Claude для получения новой информации о тщательно изучаемом математическом объекте - дзета-функции Римана. Она является центральным элементом гипотезы Римана, одной из самых сложных гипотез в мире.
Конкурент компания OpenAI Group PBC также использует свои большие языковые модели для продвижения математических исследований. В прошлом месяце компания применила свою новейшую модель Astra для решения нескольких задач Эрдоша и сужения круга открытых вопросов в теоретической информатике.
