Теренс Тао о «Математике 2.0»: доказательств стало много, понимания нет

Теренс Тао, один из самых известных математиков мира и лауреат Филдсовской премии, опубликовал слайды октябрьской лекции в Калтехе под названием «Math 2.0». Главная мысль: ИИ сделал доказательства дешёвыми, и математике пора перестать мерить успех числом решённых задач. Иначе она рискует потерять то, ради чего задачи решали.

Коротко. По Тао, «Математика 1.0» жила в условиях дефицита доказательств: решить открытую задачу было трудно и редко. Теперь, при достаточных вычислениях и доступе к передовым моделям, многие задачи, которые считались трудными, решаются быстро и часто без особой экспертизы того, кто пишет запрос. Тао предлагает использовать ИИ, чтобы люди лучше понимали математику, а не чтобы автоматически закрывать задачи одну за другой.

Почему ИИ так силён именно в математике

Тао называет три свойства доказательств, которых почти нет в других областях:

• Проверяемость. Математики спорят, что интересно, но почти всегда согласны, верно ли доказательство. Его даже можно проверить на компьютере, если записать на языке вроде Lean.
• Цифровая природа. Доказательству не нужны эксперименты и данные из реального мира, хватает бумаги, ручки и учебников. А литература почти вся оцифрована.
• Качественные данные. Большие и аккуратные наборы задач и решений.

Поэтому, пишет Тао, лаборатории вложились в математические способности моделей раньше, чем в другие области, и наступила эпоха изобилия доказательств. При этом способности ИИ «неровные»: поразительные в одних направлениях и слабые там, где задача субъективна, зависит от реального мира или где мало данных.

«Все задачи в соцсетях решает ИИ»

Один из слайдов посвящён ошибке выжившего. В пресс-релизах и соцсетях видны только успехи, а неудачные попытки ИИ почти никто не публикует. По словам Тао, большинство задач на переднем крае математики остаются нерешёнными даже при огромных вычислениях, а сложность задач ничем не ограничена. Он призывает к честным оценкам возможностей ИИ, где публикуют затраты ресурсов и отрицательные результаты, и приводит пример такого проекта: First Proof.

Задачи как маяки

Центральная мысль лекции. В чистой математике открытые задачи работают как маяки: важна не столько сама вершина, сколько то, что учёные узнают по пути, даже если задачу не решили. Если добраться до маяка автоматически, пропадают пути, которые никто не прошёл, а область вокруг задачи «стерилизуется».

Отсюда вывод Тао: решение задач всегда было лишь заменителем более ценных целей. Пока доказательств не хватало, заменитель работал. В эпоху изобилия слепая гонка за решёнными задачами уже вредит долгосрочному здоровью математики.

Тао иллюстрирует это мысленным экспериментом. ИИ получает запрос «найди лекарство от рака, которое пройдёт третью фазу испытаний». Он выдаёт смесь неизвестных веществ, никто не понимает, как она найдена, но испытания она проходит. Вам ставят диагноз, и чат-бот рекомендует это лечение. Хотели бы вы, чтобы хоть один врач или математик понимал, почему оно работает?

Как выглядит «Математика 2.0»

Тао предлагает использовать ИИ, чтобы укреплять человеческое понимание. Его примеры:

• Открытые задачи на объяснение. Найти понятное объяснение результата, известное доказательство которого запутанно. Этому посвящён студенческий Mathathon в Калтехе 13–15 ноября.
• Живые сети статей. Например, Integrated Explicit Analytic Number Theory Network: «живая таблица» связанных результатов, которую обновляют в реальном времени.
• Библиотеки формальной математики вроде Mathlib.
• Экспериментальная математика. Проект Equational Theories Project силами людей и программ закрыл больше 22 млн утверждений вида «верно или неверно» в универсальной алгебре. А конкурс по обратной задаче Галуа нашёл многочлены 24-й степени для каждой из 25 000 возможных групп Галуа.
• «Абляции». Проверить, можно ли доказать уже известную теорему, убрав часть инструментов, или что останется верным, если ослабить условия.

Тао также обещает скорый выход открытых математических моделей, которые будут прозрачнее и безопаснее. Последний слайд: главное препятствие на пути к «Математике 2.0» не технологии и даже не культура институтов, а воображение.

Почему это касается не только математиков

Мысль Тао переносится на любую работу с ИИ. Модель может быстро выдать ответ, но если никто не понимает, почему он верный, ошибку некому заметить. Похожий вывод получился в недавнем исследовании об упорстве: готовые ответы ИИ мешают людям учиться решать самим. А о том, почему код и математика у моделей получаются лучше всего, пишет и Андрей Карпати в посте о разрыве в понимании ИИ.

Частые вопросы

Источник: слайды лекции «Math 2.0».

Что дальше почитать

• Математики спорят, зачем они нужны после ИИ
• Математики спросили OpenAI про данные