Физики подтвердили верность написанного ИИ доказательства квантовой теории Янга–Миллса
«Пастухи» OpenAI — эксперты, нанятые компанией для проверки сгенерированных искусственным интеллектом решений математических задач — подтвердили правильность предложенного моделью доказательства квантовой теории Янга–Миллса — краеугольного камня Стандартной модели физики элементарных частиц.
Как и другие доказательства, полученные с помощью ИИ, выглядит оно довольно запутанным — слишком длинным и сложным, чтобы человеческий ум мог сразу его осмыслить. К анализу плода трудов ИИ OpenAI привлекла профессора Дэвида Гросса, видного физика-теоретика, лауреата Нобелевской премии.
«Мы сообщаем об обновлении статуса работы нашего комитета по сопровождению результата, полученного большой языковой моделью», — заявили «пастухи» во главе с профессором.
По их словам, результаты ИИ «доказывают существование чистой теории Янга–Миллса в соответствии с постановками задач, стандартными для физики и математики». Позже Гросс и его группа выложили документ с объяснением доказательства и подтверждение его формальной верификации на Lean — языке программирования, предназначенном для проверки математических работ.
«Я рад, что „пастухи“ наконец публикуют доказательство на Lean, так что мы можем увидеть, в чем состоит результат. Надеюсь, что в будущем разработчики ИИ будут широко делиться своими результатами с сообществом. Такую проверку можно провести более эффективно и быстро в открытом режиме», — прокомментировал математик Скотт Армстронг из Нью-Йоркского университета.
Проблема Янга–Миллса — одна из пяти остающихся нерешенными «Проблем тысячелетия», набора из семи задач, сформулированных Математическим институтом Клэя в 2000 году. За успешное решение каждой из них полагается премия 1 миллион долларов. Но решение проблемы Янга–Миллса стало бы для науки большей наградой — оно может устранить математическую нестрогость современной физики элементарных частиц.
Стандартная модель — самая тщательно проверенная и успешная научная теория на сегодня: она точно предсказывает, что происходит в столкновениях субатомных частиц на установках вроде Большого адронного коллайдера. Но никому еще не удалось свести положения Стандартной модели к простым аксиомам — и тем самым доказать ее математическую состоятельность.
Проблема тысячелетия, связанная с теорией Янга–Миллса, состоит из двух частей. Первая — доказать, что эта теория, лежащая в основе Стандартной модели, «существует», то есть может быть построена с помощью корректных математических шагов. Вторая часть более количественная (и гораздо более сложная): она требует показать, что из уравнений Янга–Миллса вытекает существенный зазор — «массовая щель». По данным OpenAI, модель решила только первую часть задачи.
Пресс-релиз «пастухов» слишком лаконичен, чтобы дать глубокое понимание написанного ИИ доказательства. Более того, Гросс и его коллеги признают, что и сами его не вполне понимают — хотя все пятеро занимались теорией Янга–Миллса.
«Мы воспользовались Astra от OpenAI для осмысления представленного кода на Lean. Мы пока не утверждаем, что полностью понимаем доказательство», — пояснили они в своей оценке.
Впрочем, теперь, когда доказательство и его код на Lean выложены в открытый доступ, к их изучению могут присоединиться все желающие.
