Команда компании Axiom Math впервые автоматически верифицировала доказательство теоремы о простых числах, известной в обиходе как «теорема 246». Сделала это ИИ-система компании — AxiomProver, и событие стало заметной вехой в исследованиях математики с участием искусственного интеллекта.
Источник изображения — spectrum.ieee.org
При формальной верификации математики поручают компьютеру проверить машиночитаемую версию доказательства. Стопроцентной гарантии корректности процедура не даёт — недавняя демонстрация показала, как ошибку в самом методе можно использовать, чтобы протолкнуть ложное доказательство, сгенерированное нейросетью. И всё же вычислительная проверка остаётся максимально близким аналогом печати «проверено».
Конкретно эта верификация формализует важное продвижение в теории чисел. Но помимо самого доказательства она демонстрирует, как автоматическая проверка сможет в будущем гарантировать корректность программного кода, написанного нейросетями, — а такой код вскоре ляжет в основание софта по всему миру.
Формализация, которую можно переиспользовать
Для AxiomProver это не первый заход. Автономная многоагентная система компании, превращающая математические утверждения в машинно-проверяемые доказательства, за год уже взломала несколько нерешённых задач и верифицировала множество доказательств. Но формализация теоремы 246 — безусловно, самый значимый результат. «Эта теорема на сегодня представляет собой границу человеческого знания о простых числах», — поясняет Кен Оно, математик-основатель Axiom Math.
Ранее в этом году конкурент Axiom Math — компания Math, Inc. — с помощью агента Gauss верифицировала доказательство задачи об упаковке шаров в 8 и 24 измерениях, за которое Марина Вязовская получила Филдсовскую премию в 2022 году. Сидхарт Харихаран, аспирант Университета Карнеги — Меллона, руководивший той частью работы, которая была выполнена людьми и оказалась критически важной для прорыва Math, Inc., считает подход Axiom Math к формализации теоремы 246 более комплексным и практически полезным. Его группа при этом продолжает работу над полной формализацией доказательства Вязовской.
Сейчас Харихаран стажируется в Axiom Math и был плотно вовлечён в формализацию теоремы 246. По его словам, одно из главных отличий в том, что вместо разового решения под единственную задачу компания сознательно добивалась, чтобы компоненты формализации можно было переиспользовать в других задачах и математических исследованиях. С помощью AxiomProver команда построила целую библиотеку результатов о промежутках между простыми числами, а теорема 246 стала её флагманским элементом.
Что такое теорема 246
Первые простые числа расположены плотно: 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31… И среди них немало пар, отличающихся ровно на два: 3 и 5, 5 и 7, 11 и 13, 17 и 19.
Такие пары называются близнецами. Чем дальше от нуля, тем реже они встречаются, но появляться всё же не перестают. Гипотеза о простых близнецах, впервые точно сформулированная в XIX веке французским математиком Альфонсом де Полиньяком, утверждает, что они будут возникать сколь угодно далеко по числовой прямой. Иными словами, простых близнецов бесконечно много.
Формулируется гипотеза просто, а вот доказать её не удаётся до сих пор. Первое продвижение случилось лишь в 2013 году, когда Итан Чжан, ныне профессор Университета Сунь Ятсена в Гуанчжоу, доказал, что существует бесконечно много пар простых чисел, разделённых промежутком в 70 миллионов. Само по себе число выглядело астрономическим, но принципиальным был сам факт: какая-то конечная граница существует. Несколькими месяцами позже профессор Оксфордского университета Джеймс Мэйнард, используя другую технику, радикально сократил этот промежуток с 70 миллионов до 600 — достижение, во многом обеспечившее ему Филдсовскую премию 2022 года, которую нередко называют математическим аналогом Нобелевской.
В рамках коллаборации математиков, известной как Polymath8b, Мэйнард вместе с другим филдсовским лауреатом Теренсом Тао, профессором Калифорнийского университета в Лос-Анджелесе, довёл промежуток до 246 — максимально близко к заветной двойке, которой требует сама гипотеза о близнецах. Именно эту теорему 246, утверждающую, что существует бесконечно много простых чисел с разностью 246, и подтвердил AxiomProver.
Безопасный и корректный код, написанный нейросетью
Формализованные в этой работе техники важны для теории чисел — раздела математики, на котором держатся вся современная кибербезопасность и криптография. А значит, они вполне могут пригодиться при верификации конкретных механизмов, которыми мы защищаем свои цифровые данные.
Но Оно куда больше воодушевляет картина в целом. Он видит в формализации математических доказательств ступень к проверке кода, написанного искусственным интеллектом, — а такой код уже начинает применяться в системах, управляющих инфраструктурой, финансами и защитой данных. И это несмотря на все опасения по поводу галлюцинаций, ошибок и непреднамеренных уязвимостей.
Если свойства программы — например, завершается ли алгоритм или корректен ли вывод при любых входных данных — удастся перевести в точные математические утверждения, то технологии на основе AxiomProver окажутся идеально приспособлены для того, чтобы эти утверждения формулировать и доказывать. Математическая проверка корректности сгенерированного кода сделала бы его безопасным в применении.
«Мир вот-вот начнёт работать на компьютерном коде, который никто не читал, — резюмирует Оно. — ИИ уже здесь, и отворачиваться больше нельзя. Формализация доказательств — это испытательный полигон для решения того, что я считаю важнейшим вызовом, который поставит перед нами искусственный интеллект».
