1 августа OpenAI опубликовала сборник из десяти новых результатов в математике и теоретической информатике. В него вошли работы по упаковке сфер в пространствах высокой размерности, теории кодов, сложности вычислений, квантовым системам, геометрии чисел, теории групп и комбинаторике. Компания утверждает, что её внутренняя модель Astra решила несколько давних открытых задач, опровергла ряд гипотез и существенно улучшила известные оценки в других случаях. Всё это изложено в документе объёмом почти 250 страниц.
Для большинства людей сама формулировка новости звучит почти издевательски. Где-то выяснили, насколько плотно можно расположить шары в пространстве, которое невозможно представить. Где-то доказали существование группы с определёнными алгебраическими свойствами. Где-то уточнили, сколько одноцветных треугольников неизбежно возникнет в достаточно большой системе связей.
Хорошо. И что теперь?
Ничего — если ждать от каждого математического результата немедленного товара. Новый телефон из него завтра не соберут. Лекарство не изготовят. Даже обычный калькулятор считать быстрее не станет.
Но математика вообще редко производит готовые вещи. Она производит границы возможного.
Возьмём упаковку сфер. В трёхмерном мире это вопрос о том, как плотнее сложить одинаковые апельсины. В пространстве из сотен или тысяч измерений никакие апельсины уже не помещаются — да и представить такое пространство человек не способен. Кажется, что перед нами идеальная игра ума, окончательно оторванная от жизни.
Однако цифровое сообщение тоже можно представить как точку в многомерном пространстве. Чем дальше друг от друга расположены точки, обозначающие разные сообщения, тем легче различить их после того, как связь внесла помехи и часть данных исказилась. Поэтому задачи об упаковке сфер непосредственно соприкасаются с теорией кодирования: они помогают понять, сколько информации в принципе можно передать или сохранить так, чтобы ошибки ещё оставалось возможно исправить. В опубликованной работе новые результаты по упаковке сфер соседствуют с экспоненциально улучшенными границами для двоичных и сферических кодов.
Это не новый стандарт мобильной связи. Это разметка территории, по которой однажды будут прокладывать связь.
Другой результат касается задачи о ближайшем векторе. Если говорить совсем упрощённо, перед нами огромное многомерное пространство с правильно расположенными точками. Нужно найти точку, ближайшую к заданному месту. В двух измерениях задача выглядит почти школьной. Но с ростом числа измерений и объёма данных она становится чрезвычайно трудной.
Именно на трудности подобных задач строится значительная часть решёточной криптографии — одного из главных направлений защиты данных от будущих квантовых компьютеров. Работа Astra не предлагает новый шифр и не доказывает безопасность конкретной банковской системы. Она уточняет, насколько трудно приближённо решать одну из фундаментальных задач, от сложности которых зависит доверие к целому классу криптографических методов.
Ещё одна работа устанавливает новые нижние границы сложности вычисления перманента — функции от матрицы, похожей на определитель, но гораздо более трудной для вычисления. С практической точки зрения здесь важен не сам перманент. Важен тип вопроса: можно ли решить задачу существенно короче и быстрее или определённое количество вычислений неизбежно?
Инженер обычно ищет более эффективный алгоритм. Теоретик пытается доказать, что в выбранной модели вычислений более эффективного алгоритма вообще не существует. Это похоже на доказательство того, что между двумя берегами нельзя построить мост короче определённой длины. Такое знание не строит мост, но не позволяет десятилетиями искать невозможную конструкцию. Astra получила новые нижние оценки для арифметических схем и формул, вычисляющих перманент.
Работа о квантовом параллельном повторении устроена ещё нагляднее. Представим проверку, которую нечестный участник иногда способен обмануть. Естественная идея — повторить её много раз. В классическом случае известно: при подходящих условиях вероятность обмана быстро уменьшается. Но участники квантовой системы могут быть связаны запутанностью, поэтому их действия нельзя рассматривать как полностью независимые.
Новый результат утверждает, что и для общего класса конечных квантовых игр многократное повторение заставляет вероятность успешного обмана убывать экспоненциально. Это фундаментальная работа о надёжности интерактивных доказательств, а не готовая система защиты. Но именно из подобных фундаментальных утверждений впоследствии собираются способы проверять вычисления и строить криптографические протоколы.
Часть остальных результатов находится ещё дальше от очевидного применения. Не всякую теорему нужно немедленно оправдывать будущей банковской системой или новым способом передачи данных. Теория групп, операторные алгебры и экстремальная комбинаторика создают язык, на котором наука описывает симметрии, связи и сложные структуры. Иногда между таким результатом и технологией проходит несколько лет. Иногда — столетие. Иногда прикладного продолжения не возникает вовсе.
Но в данном случае главная ценность новости даже не в сумме десяти теорем.
До сих пор мы в основном обсуждали искусственный интеллект как систему, способную пересказать известное, написать программу по уже понятному заданию, обработать данные или помочь человеку найти решение. Astra, по заявлению OpenAI, работала иначе: получала открытую исследовательскую проблему и строила новое математическое рассуждение там, где готового ответа прежде не существовало.
Компания оценила стоимость токенов, потраченных непосредственно на поиск всех десяти решений, примерно в две тысячи долларов по тарифам Sol API. Это не полная стоимость создания модели, работы исследователей, подготовки публикации и инфраструктуры. Но само соотношение всё равно поражает: интеллектуальный поиск, который мог бы занимать у отдельных научных групп месяцы или годы, начинает измеряться тысячами долларов вычислений.
И здесь возникает новая проблема. Человек может написать убедительное, красивое и ошибочное доказательство. Искусственный интеллект — тем более. Если машина начнёт производить математические тексты быстрее, чем учёные способны их читать, наука рискует получить не ускорение, а свалку правдоподобных результатов.
Поэтому OpenAI приложила к каждому рассуждению формальный сертификат на языке Lean. В обычной статье доказательство написано для человека: специалист читает его, восстанавливает пропущенные шаги и решает, нет ли ошибки. В Lean доказательство переводится на строгий формальный язык и проверяется небольшим программным ядром по заданным определениям и правилам логики. Репозиторий со всеми десятью формализациями открыт, предусмотрена и процедура независимой проверки.
Это не волшебная печать абсолютной истины. Компьютер подтверждает, что формальный вывод следует из формальных предпосылок. Людям всё ещё необходимо проверить, правильно ли сама формулировка передаёт исходную математическую проблему, не спрятано ли существенное допущение в определениях и действительно ли результат имеет заявленное значение. Документация Lean прямо различает два вопроса: существует ли корректное формальное доказательство и означает ли доказанная формула именно то, что мы думаем.
Поэтому пока рано говорить, что OpenAI принесла математическому сообществу десять окончательно признанных открытий. Компания предъявила работы, формализации и возможность их проверить. Теперь математикам предстоит разобраться, насколько верно поставлены задачи, новы ли методы, не существовали ли близкие результаты и что из доказанного действительно меняет соответствующие области.
Но ценность события уже видна.
Искусственный интеллект начинает снижать стоимость не только ответа, но и научного поиска. Он способен перебирать подходы, соединять методы из разных областей и оформлять результат в форме, которую можно проверять машиной. А значит, главным дефицитом науки постепенно становится не способность долго считать.
Главным дефицитом становится хороший вопрос.
Нужно будет выбирать, какие из миллионов возможных задач действительно стоит решать, какие результаты способны открыть новое направление и как превратить доказанную возможность в человеческое знание. Искусственный интеллект может найти путь через лес. Но решить, зачем мы туда идём и что делать с найденной дорогой, по-прежнему должны люди.
Математические игры ума не всегда необходимы прямо сейчас. Их ценность в другом: они заранее выясняют, что однажды окажется возможным — и что невозможным останется навсегда.
