[Перевод] ИИ использовали для проверки самого сложного на сегодняшний день математического доказательства

ИИ использовали для проверки самого сложного на сегодняшний день математического доказательства

Простой

5 мин

1

Перевод

Будущие версии смогут проверять правильность кода, сгенерированного ИИ

Важной вехой в математических исследованиях с использованием ИИ стал пример команды компании Axiom Math, которая впервые автоматически проверила доказательство теоремы, касающейся простых чисел — в просторечии известной как «теорема 246» — с помощью собственной системы искусственного интеллекта AxiomProver.

При формальной проверке математики поручают компьютеру проверить машиночитаемую версию доказательства. Этот процесс не дает 100-процентной гарантии правильности доказательства, как показала недавняя демонстрация, в ходе которой было выявлено, что ошибка в методе может привести к ложному подтверждению доказательства, сгенерированного ИИ. Тем не менее, этот вычислительный метод максимально приближает к одобрение доказательства при помощи ИИ к реальности.

Это подтверждение формализует важный прорыв в теории чисел. Помимо этого конкретного доказательства, она демонстрирует, как автоматизированную проверку с помощью ИИ можно будет использовать в будущем для обеспечения корректности компьютерного кода, сгенерированного ИИ, который в скором времени станет основой программного обеспечения по всему миру.

Полезная формализация

Для AxiomProver это далеко не первая попытка. В этом году компания Axiom Math использовала свою автономную многоагентную систему, преобразующую математические утверждения в доказательства, поддающиеся машинной проверке, для решения нескольких нерешенных математических задач и проверки множества других доказательств. Однако формализация доказательства теоремы 246 является, безусловно, самой значимой, как объясняет Кен Оно, математик и основатель Axiom Math: «Эта теорема в настоящее время представляет собой предел человеческих знаний о простых числах».

Ранее в этом году компания Math, Inc., конкурент Axiom Math, использовала своего агента Gauss для проверки доказательства Марины Вязовской, удостоенного в 2022 году медали Филдса, по задаче упаковки сфер в 8 и 24 измерениях. Сидхарт Харихаран, аспирант Университета Карнеги‑Меллона, возглавлявший работу людей, сыгравшую решающую роль в прорыве Math, Inc., утверждает, что подход Axiom Math к формализации теоремы 246 с использованием ИИ является более всеобъемлющим и полезным. Группа Харихарана продолжает работать над полной формализацией доказательства Вязовской.

В настоящее время Харихаран, стажер в компании Axiom Math, принимает активное участие в работе над формализацией доказательства теоремы 246. По его словам, одно из основных отличий заключается в том, что вместо разового подхода, ориентированного на решение одной конкретной задачи, компания Axiom Math специально стремилась сделать компоненты формализации пригодными для повторного использования в других задачах формализации и математических исследованиях. Команда использовала 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 подтвердил как верную.

Безопасный и корректный код, сгенерированный ИИ

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

Однако Оно из Axiom Math больше вдохновлен более широкой перспективой. Он рассматривает формализацию математических доказательств как отправную точку для проверки кода, сгенерированного искусственным интеллектом, который начинает повсеместно использоваться в системах, обеспечивающих работу нашей инфраструктуры, управление нашими финансами и защиту наших данных. И это несмотря на опасения по поводу безопасности, связанные с «галлюцинациями», ошибками и другими непреднамеренными уязвимостями.

Если свойства кода — например, завершается ли работа алгоритма или является ли результат программы корректным для любого входного значения — можно перевести в точные математические утверждения, то технологии, основанные на AxiomProver, идеально подойдут для их формального формулирования и доказательства. Таким образом, математическая проверка корректности кода, сгенерированного ИИ, сделает этот код безопасным для использования.

«Мир вот‑вот начнёт работать на компьютерном коде, который никто не читал, — заключает Оно. — ИИ уже здесь, и мы больше не можем отворачиваться от него — формализация доказательств является испытательным полигоном для решения того, что, на мой взгляд, является самой важной проблемой, с которой мы столкнёмся в связи с ИИ».

Если эта публикация вас вдохновила и вы хотите поддержать автора — не стесняйтесь нажать на кнопку