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