Математическая красота, истина и доказательство в эпоху ИИ

Математики начали готовиться к кардинальным переменам в том, что значит заниматься математикой. Комментарий Сохранить статью Прочитать позже

С начала 20-го века сердцем математики было доказательство — строгий, логический аргумент в пользу того, является ли данное утверждение истинным или ложным. Карьера математиков измеряется тем, какие теоремы они могут доказать и сколько. Они тратят большую часть своего времени на то, чтобы придумать новые идеи, чтобы заставить доказательство работать, а затем переводят эти интуиции в пошаговые выводы, подгоняя различные линии рассуждений вместе, как кусочки пазла.

Лучшие доказательства — это произведения искусства. Они не просто строгие; они элегантные, креативные и красивые. Это заставляет их ощущаться как отчетливо человеческая деятельность — наш способ осмысления мира, оттачивания ума, проверки границ самой мысли.

Но доказательства также по своей сути рациональны. И поэтому было вполне естественно, что когда исследователи начали разрабатывать искусственный интеллект в середине 1950-х годов, они надеялись автоматизировать доказательство теорем: разработать компьютерные программы, способные генерировать собственные доказательства. Они добились определенного успеха. Одна из самых ранних программ ИИ могла выводить доказательства десятков утверждений в математической логике. За ней последовали другие программы, придумавшие способы доказательства утверждений в геометрии, исчислении и других областях.

Но эти автоматизированные доказыватели теорем были ограничены. Те виды теорем, которые действительно волновали математиков, требовали слишком много сложности и креативности. Математические исследования продолжались, как и всегда, не затронутые и не сдерживаемые.

Теперь это начинает меняться. За последние несколько лет математики использовали модели машинного обучения, чтобы открывать новые закономерности, придумывать новые гипотезы и находить контрпримеры к старым. Они создали мощные помощники по доказательствам как для проверки правильности данного доказательства, так и для организации своих математических знаний.

Они пока не создали систем, которые могут генерировать доказательства от начала до конца, но это может измениться. В 2024 году Google DeepMind объявила, что разработала систему ИИ, которая получила серебряную медаль на Международной математической олимпиаде, престижном экзамене на доказательства для старшеклассников. Более обобщенная «большая языковая модель» OpenAI, ChatGPT, достигла значительного прогресса в воспроизведении доказательств и решении сложных задач, как и менее масштабные заказные системы. «Поразительно, насколько они совершенствуются», — сказал Эндрю Грэнвилл, математик из Монреальского университета, который до недавнего времени сомневался в заявлениях о том, что эта технология вскоре может оказать реальное влияние на доказательство теорем. «Они полностью разносят в пух и прах там, где, как я думал, были ограничения. Кот выпал из мешка».

Исследователи прогнозируют, что они смогут начать передавать на аутсорсинг более утомительные разделы доказательств ИИ в течение следующих нескольких лет. Они не уверены в том, сможет ли ИИ когда-либо полностью доказать их самые важные гипотезы: некоторые готовы принять эту идею, в то время как другие считают, что существуют непреодолимые технологические барьеры. Но уже не исключено, что более творческие аспекты математического предприятия могут быть однажды автоматизированы.

Несмотря на это, большинство математиков в настоящее время «намертво зарыли головы в песок», сказал Грэнвилл. Они игнорируют последние разработки, предпочитая тратить свое время и энергию на свою обычную работу.

Некоторые исследователи предупреждают, что продолжать делать это будет ошибкой. Даже возможность передавать скучные или механические части доказательств на аутсорсинг ИИ «со временем радикально изменит то, что мы делаем и как мы думаем о математике», — сказал Акшай Венкатеш, выдающийся математик и обладатель медали Филдса в Институте перспективных исследований в Принстоне, штат Нью-Джерси.

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

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

Какие инструменты были сделаны

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

Сегодня мы не могли бы заниматься математикой без письма. «Бумага функционирует как внешняя память, другой тип системы мышления», — сказал Венкатеш. Она позволила людям хранить знания и передавать их; даже решения о том, какие символы использовать для представления математических концепций, привели к важным достижениям.

Во времена Сократа и в течение следующих 2000 лет западная математика была геометрией. Древние греки характеризовали математику как науку о величине, о вещах, которые можно рисовать, измерять и считать. Представляя концепции геометрически, математики могли находить смысл и открывать приложения. Работа была физической, даже тактильной.

Затем, в 1637 году, французский математик Рене Декарт опубликовал свой трактат «Рассуждение о методе». В приложении к нему он ввел то, что позже стало известно как декартовы координаты: способ перевода геометрических кривых и фигур в алгебраические уравнения. Алгебра стала средством аутсорсинга определенных задач, которые не могли быть решены геометрически. Но это также означало отход от физического понимания математики. «Вы можете упорно трудиться над алгеброй, но вы работаете вслепую», — сказал Джереми Грей из Открытого университета в Англии. «Включение и пыхтение не имеет того визуального качества, которое есть у большей части евклидовой геометрии. Это мощно, но не так очаровательно».

Некоторые математики считали, что алгебраические методы ведут математику в неправильном направлении. Главным среди них был Исаак Ньютон. Эти подходы, писал он, были «настолько утомительными и запутанными, что вызывали тошноту». Для него геометрическая интуиция была центральной в том, что означало по-настоящему понимать что-то математически. Работая в терминах алгебраических символов и абстракций, утверждал он, математики, возможно, не могли понять, что они делают, даже если они думали, что делают.

Сначала алгебраические методы были средством достижения цели. Они просто позволяли математикам думать и решать определенные проблемы. Но вскоре математики начали изучать эти методы ради них самих, что привело к появлению всевозможных прекрасных математических вычислений: например, исчисление было бы немыслимо без алгебры. Это, в свою очередь, привело к формализмам, таким как теория множеств — основа современной математики — которая затем открыла совершенно новые области изучения. (Ньютон, один из изобретателей исчисления, изначально разработал для него алгебраическую основу. Но из-за своих философских взглядов он отказался публиковать свою работу, пока не нашел способ представить ее геометрически.)

Математика постепенно отошла от своих геометрических корней и двинулась в сторону все большей и большей абстракции. «Сегодня представление о том, что математическая истина основана на геометрии, кажется странным», — написал Джереми Авигад из Университета Карнеги — Меллона в своем эссе в 2022 году. Теперь математики передают проблемы на аутсорсинг всевозможным методам, как алгебраическим, так и нет; они часто называют эти методы, которые становятся намного сложнее алгебраических уравнений, математической «машиной». То, что когда-то было неприемлемой абстракцией, теперь не более загадочно, чем электроинструмент, и столь же необходимо для создания чего-либо амбициозного.

Знать каждый ноготь

Чтобы построить доказательство, математики начинают с прочного фундамента предположений или аксиом. Они кладут кирпичи на этот фундамент по одному — утверждения или леммы, которые в конечном итоге объединяются, чтобы помочь сформировать единую логическую структуру.

В конечном счете, важна именно эта всеобъемлющая структура: стены, лестницы и колонны, которые придают доказательству форму. Но хотя самым интересным аспектом доказательства может быть его план — общая конструкция аргумента — сами кирпичи тоже имеют значение. Леммы — это второстепенные утверждения, которые также нужно доказать как истинные, а затем объединить их хитрыми способами, чтобы построить полное доказательство.

Лемма может включать обобщение известного утверждения, например, или показывать, что объект удовлетворяет определенному набору свойств. Обычно математики достаточно уверены в том, что такие леммы истинны. Но их строгое доказательство может занять некоторое время, от нескольких часов до нескольких недель. Они могут не требовать много креативности, но они отнимают много времени и могут в конечном итоге составить страницы и страницы в окончательном доказательстве.

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

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

Но даже это использование ИИ — для достижения того, что люди уже могут делать, хотя и медленнее — может значительно изменить математику, как это сделало введение алгебраической техники в 17 веке. Чтобы получить представление о том, как это может выглядеть, Хезер Макбет из Имперского колледжа Лондона сравнивала традиционные доказательства с доказательствами тех же теорем, написанными с использованием помощника по доказательству Lean. В доказательстве Lean все шаги записываются в компьютерном коде, некоторые вручную, другие с использованием ИИ; затем программа проверяет, что шаги следуют допустимой логической цепочке, и что доказательство является правильным. Макбет обнаружила, что в таком доказательстве вы можете упаковать больше информации в автоматизированные процессы, называемые «тактиками», освобождая математиков для сосредоточения на описаниях и понимании более высокого уровня.

«Даже в том, что мы считаем доказательной математикой, хлебом и маслом взрослой исследовательской математики, все еще есть много того, что на самом деле является вычислениями», — сказал Макбет. Поскольку эти части доказательства передаются на аутсорсинг компьютерам, будь то Lean или какая-то другая система ИИ, математики могут тратить больше энергии на предоставление объяснений и передачу самых важных идей; будет меньше акцента на деталях, потому что рутина станет компетенцией ИИ. Это будет представлять собой значительный культурный сдвиг в математике: математикам больше не придется так сильно беспокоиться о строгости.

«Произойдёт своего рода разрыв между строгостью на бумаге и строгостью в голове», — сказал Дэниел Литт из Университета Торонто. «Я пойму что-то новое в целостном смысле, даже если не пойму всех деталей».

Однако математики в целом сверхъестественно расположены в силу своего темперамента или обучения к тому, чтобы заниматься строгостью. «Мне не нравится чувство непонимания деталей, поэтому мне придется смириться с этим чувством», — сказал Литт.

Это чувство — не просто дискомфорт; математики беспокоятся (как и Сократ), что если они перестанут подчеркивать строгость, это может негативно сказаться на их способности мыслить. «Вы можете сказать, ну, тогда, хорошо, вы вольны смотреть на общую картину. Но я чувствую, что мое собственное понимание не из общей картины, а из того, что вы пачкаете руки», — сказал Грэнвилл. «Сила абстракции лучше всего в руках людей, которые также понимают практику».

Добавление путем деления

Многие математики могут чувствовать себя неловко, не понимая каждую последнюю деталь в своих доказательствах, но у нас уже есть примеры весьма успешных исследовательских программ, в которых никто не может держать в голове каждую деталь. Например, в физике элементарных частиц было более 3000 авторов статей, которые объявили об открытии бозона Хиггса, венце научного эксперимента, потребовавшего десятилетий усилий и миллиардов долларов. Даже в математике в течение 20-го века более 100 исследователей внесли свой вклад в огромное доказательство — заполнив более 10 000 страниц — которое классифицировало важные объекты, называемые конечными простыми группами.

ИИ призван сделать этот вид математических проектов правилом, а не исключением, превратить эту тему в масштабное сотрудничество, которое делает упор на эксперименты и позволяет задавать вопросы, которые раньше нельзя было задать.

Осенью 2024 года, чтобы продемонстрировать, как может выглядеть это будущее, Теренс Тао из Калифорнийского университета в Лос-Анджелесе запустил проект эквациональных теорий. Сначала он рассмотрел простой математический объект, называемый магмой: набор элементов, а также правило для объединения любых двух элементов в наборе для создания третьего. (Это правило может быть сложением, умножением или менее знакомой операцией. Один из самых центральных объектов в математике, называемый группой, представляет собой особый вид магмы.)

Затем Тао придумал тысячи утверждений, описывающих, как могут вести себя элементы в любой данной магме. Например, элементы могут быть коммутативными, что означает, что порядок, в котором вы их объединяете, не имеет значения. Или объединение элемента с самим собой может всегда давать вам тот же элемент. Каждое утверждение «само по себе является скучным объектом», сказал Тао. Но он хотел понять, как все эти утверждения связаны друг с другом. Если магма удовлетворяет одному утверждению, она также может удовлетворять множеству дополнительных утверждений, но не другим.

Среди всех утверждений было 22 миллиона возможных импликаций, и Тао хотел оценить, было ли каждое из них истинным или ложным. «Вы смотрите на ландшафт этих уравнений как на нечто большое, и вы изучаете этот ландшафт сам по себе», — сказал Адам Топаз из Университета Альберты, который не принимал участия в проекте. «Без компьютеров мы не смогли бы этого сделать».

В течение пары месяцев более 50 участников, многие из которых были любителями, доказали истинность или ложность почти всех 22 миллионов импликаций. Некоторые использовали ИИ, другие решали импликации вручную. В конечном итоге проект, который был завершен в апреле 2025 года, открыл новую область математических вопросов, которая в противном случае не показалась бы интересной вообще.

Это дает проблеск того, как будут выглядеть математические исследования с помощью ИИ. «В будущем, когда мы будем исследовать область математики, вы могли бы сначала заставить ИИ исследовать миллионы проблем и получить некое предварительное представление о ландшафте», — сказал Тао. «Просто очень низкого качества. Но это подтолкнет более продвинутых людей сказать: «Хорошо, теперь, основываясь на такого рода эксперименте, мы должны направить наши человеческие ресурсы на это»».

«Это более разрозненный подход», — сказала Майя Фрейзер из Оттавского университета. Или, как выразился Родриго Очигаме, антрополог и историк из Лейденского университета в Нидерландах, «он имеет своего рода недисциплинированный, экспериментальный, самостоятельный характер».

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

Как и физика и другие лабораторные науки, математика может также включать большее разделение труда. В настоящее время математик отвечает за выполнение всех математических задач от начала до конца: придумывание новых идей, доказательство лемм и теорем, написание доказательств и их сообщение. Это, скорее всего, изменится с появлением ИИ. Некоторые математики могут продолжать заниматься математикой вручную, если в возможностях систем ИИ есть пробелы. Другие математики могут отвечать за разработку теорий для проверки или перевод гипотез на язык компьютеров, чтобы можно было запустить ИИ и системы проверки, или за то, чтобы убедиться, что то, что доказывает ИИ, на самом деле то, что хотят доказать математики (невероятно сложная задача), или за координацию между многочисленными соавторами проекта, или за объяснение автоматизированных доказательств другим. «В физике или химии есть люди, которые придумывают теории, есть люди, которые проводят эксперименты, и обе стороны ценят друг друга», — сказал Йохан Коммелин, математик из Утрехтского университета и Lean Focused Research Organization. «Это может начать выглядеть более похожим на это».

«Мы увидим больше групповых проектов, где ни один человек не знает всего, что происходит, но где люди могут сообща достичь гораздо большего, чем любой отдельный человек», — сказал Тао. «Именно так работает остальная часть современного мира».

Конец математики?

Может быть удивительно узнать, что то, что считается значимым математическим вопросом, часто является делом вкуса. В глубинном смысле вопрос «Что такое математика?» — это то же самое, что и вопрос «Что математики считают важным?»

По словам Венкатеша, чем проще становится решать определенные математические задачи, тем меньше математики будут ценить эти задачи. «Это как высокая мода», — сказал Алекс Дэвис, исследователь из DeepMind. «Как только у вас появляется технология, которая делает высокую моду очень легкодоступной для людей, и она становится массовым рынком, она становится менее модной. И люди высокой моды уходят и делают что-то другое».

Системы ИИ могут лучше подходить для решения определенных задач, делая эти задачи по своей сути менее интересными. Неясно, какие предметы могут отпасть первыми. Например, задачи о поиске оптимальных решений для функций когда-то были более центральной частью чистой математики, тесно переплетенной с исчислением, алгеброй и другими областями. Но в середине 20-го века, с развитием компьютерных методов, доказательства оптимизации, как правило, сводились к вычислениям. Фокус сместился на применение этих методов, и поэтому сегодня, хотя задачи оптимизации по-прежнему важны, они больше относятся к сфере прикладной математики — области, которая, вместо того чтобы заниматься изучением идей или концепций ради них самих, стремится использовать их как средство для достижения конкретной практической цели.

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

Тем не менее, если ИИ станет достаточно хорош для решения проблем в некоторых из этих областей, то, возможно, ничто не помешает ему в конечном итоге стать хорошим в решении проблем во всех областях. В этом будущем математики смогут сосредоточиться на других вещах. «Я считаю, что ИИ сможет доказать многое, но математики просто изменят уровень абстракции, на котором они работают», — сказал Топаз.

Например, работая с ИИ, Литт понял, что гораздо больше математики, чем он осознавал раньше, заключается в знании огромного количества фактов и объединении их интересными способами, а не в моменте озарения. «Я каким-то образом понял, что многое из того, что я считаю сложным, больше касается вашей рабочей памяти и знаний, а не творчества», — сказал он. «Это поколебало мою уверенность в том, что я понимаю, что мы делаем или что делает хорошего математика. Теперь я думаю, что большая часть того, что я делаю, — это объединение некоторых фактов, известных стандартными способами. И затем время от времени в том, что я делаю, есть на самом деле творческая часть. Я провожу аналогию или разрабатываю новое определение».

Это означает, что «многое из того, что я делаю, под силу машине», — добавил он.

Возможно, математики вместо этого будут тратить большую часть своего времени, пытаясь понять доказательства, которые генерирует система ИИ, — задача, которая потребует много времени, усилий и изобретательности. Марк Кисин, математик из Гарвардского университета, предвидит, что область сместится в сторону более близких к гуманитарным наукам, возможно, где-то в течение следующих 10–100 лет. «Если вы посмотрите на типичный факультет английского языка в университете, то обычно там нет людей, которые пишут литературу», — сказал он. «Там есть люди, которые критикуют литературу». Аналогичным образом, сказал он, математики могут взять на себя роль критиков, которые внимательно анализируют доказательства ИИ, а затем преподают их на семинарах. (Ронен Элдан, математик, который недавно ушел из Института науки Вейцмана ради OpenAI, вспоминает разговор, в котором другой математик предсказал, что «математики будут как пианисты сегодня», — сказал он. «Они не играют свои собственные композиции, но люди все равно приходят их послушать».)

Даже тогда математикам будет чем заняться: от придумывания новых определений и абстракций до решения, какие новые направления исследований будут наиболее интересны для продолжения. «Мне трудно представить, что фундаментальная творческая работа по руководству программой математики может быть выполнена кем-то, кроме людей», — сказала Эмили Риль из Университета Джонса Хопкинса.

Тем не менее, потенциальные изменения, которые предвидят математики, глубоки. «В каком-то смысле это будет концом исследовательской математики в том виде, в котором она практикуется в настоящее время», — сказал Литт. «Но это не значит, что это будет концом математиков».

«Я думаю, это ударило бы по моему самолюбию, но не думаю, что я бы сильно расстроился», — добавил он. «Если есть большая языковая модель, которая может доказать гипотезу Римана и объяснить мне доказательство, я бы все равно с радостью ее изучил. В основном, что я хочу сделать в математике, так это понять, что истинно и почему это истинно».

«Последние 50 лет мы находились в своего рода стационарной среде. Мы могли бы продолжать делать то, что делали», — сказал Венкатеш. «Но мы больше не можем этого делать».

Источник: www.quantamagazine.org