Вот перевод статьи Теренса по ссылке на русский:В последнее время в Сети обсуждают тему использования искусственного интеллекта (ИИ) в современной математике. Реален ли прогресс и на чем он может основываться?
Конкретно об этом в недавнем отчете Теренса Тао:
"Теренс Тао: Машинная помощь и будущее исследовательской математики".
Казалось, что с математикой в ИИ должны быть самые большие проблемы, потому что все нужно строго доказывать, а не как любит chatjpt. А вот у математиков оказался инструмент фильтрации неправильных доказательств--- доказательство надо переписать как код для языка программирования Lean (или аналогичный) и компилятор просто проверяет, что нет ошибок с типами и это уже проверка математического доказательства!
Особенность Lean - очень широкие возможности для создания новых типов. В частности, кроме любого, условного int и String, каждое математическое утверждение (правильное или нет) можно считать новым типом. Чтобы доказать теорему, необходимо сформировать конкретный элемент (термин) соответствующего типа. При таком подходе компилятор просто проверяет согласование типов. Если компилятор не выдает ошибок, то теорема строго доказана.
Эта ключевая корреляция между математическими доказательствами и программами - совместимость Curry–Howard - известна десятилетиями, но я узнал об этом только в прошлом году.
Теперь ИИ пытаются заставить писать доказательство не словами, а кодом на Lean, который составлен без ошибок. Человек может не беспокоиться, пока ИИ не договорится обо всем с компилятором.
Nikolay Iorgov, академик АН Украины, перевод с украинского мой.
Видение Теренса Тао об использовании ИИ-помощников в математических исследованиях
Дэвид Х. Бейли, 4 октября 2024 г.
Инструменты с компьютерной поддержкой для исследований в области математики
В предыдущей статье в журнале Math Scholar мы осветили некоторые недавние разработки в области сложных компьютерных инструментов, применяемых в сфере математических исследований. К таким инструментам относятся:
Инструменты верстки (обычно LaTeX) в сочетании с такими инструментами, как MathJax, для встраивания математических формул в веб-страницы.
Инструменты для совместной работы, такие как блоги, FaceTime, Skype, Zoom, Slack и Microsoft Teams, облегчают общение и сотрудничество между исследователями.
Программное обеспечение для символических математических вычислений, такое как Mathematica , Maple и Sage, позволяет выполнять все более сложные символические операции и выводы, а также создавать графики, иллюстрирующие результаты.
Специально разработанный код, часто включающий алгоритмы, такие как алгоритм целочисленных соотношений PSLQ Фергюсона или алгоритм QQQ, в сочетании с высокоточной арифметикой с плавающей запятой, предназначен для обнаружения новых математических соотношений и тождеств.
Формальное математическое программное обеспечение, такое как Lean , Coq , HOL и Isabelle, используется для кодирования и строгого подтверждения всех этапов формального математического доказательства.
Теренс Тао о средствах проверки доказательств, искусственном интеллекте и будущем математических исследований.
В предыдущей статье Math Scholar также были опубликованы отрывки из интервью между математиком Теренсом Тао, лауреатом Филдсовской медали Калифорнийского университета в Лос-Анджелесе, и Кристофом Дроссером, автором Spektrum der Wissenschaft (немецкое издание Scientific American ). Дроссер и Тао подробно обсудили текущее состояние компьютерных инструментов в математических исследованиях, включая программное обеспечение для проверки доказательств, а также инструменты на основе искусственного интеллекта, и то, каким, вероятно, будет будущее этой области. В интервью Тао отметил, что появление автоматизированных систем проверки доказательств (его любимая — Lean ) коренным образом изменило соотношение доверия между математическими коллегами. Теперь гораздо большие команды могут совместно распределять задачи по проверке доказательств, при этом работа каждого участника передается в систему проверки доказательств для обеспечения достоверности.
Тао поделился новыми мыслями о своем видении искусственного интеллекта и других передовых компьютерных инструментов для помощи исследователям в математике. В статье , опубликованной в журнале Atlantic 4 октября 2024 года и подготовленной совместно с автором Atlantic Маттео Вонгом, Тао представил более подробную информацию о своем видении. Вот несколько отрывков из его интервью:
Вонг: Каким был ваш первый опыт работы с ChatGPT?
Тао: Я начал с ним работать практически сразу после выхода. Я задавал сложные математические задачи, и результаты были довольно нелепыми. Текст был написан связным английским языком, использовались правильные слова, но глубины было очень мало. Что касается чего-то действительно сложного, ранние GPT совсем не впечатляли. Они были хороши для развлечений — например, если вы хотели объяснить какую-нибудь математическую тему в виде стихотворения или рассказа для детей. Вот это уже довольно впечатляет.
Вонг: В OpenAI утверждают, что o1 [новая версия, ориентированная на математику и естественные науки] может «рассуждать», но вы сравнили эту модель с «посредственным, но не совсем некомпетентным» аспирантом [уточнено, что имеется в виду «научный ассистент»].
Тао: Верно, это эквивалент в плане выполнения функций помощника. Но я представляю себе будущее, где вы будете проводить исследования посредством диалога с чат-ботом. Допустим, у вас есть идея, и чат-бот её подхватывает и заполняет все необходимые детали.
В некоторых других областях это уже происходит. Искусственный интеллект, как известно, покорил шахматы много лет назад, но шахматы процветают и сегодня, потому что теперь достаточно хороший шахматист может предсказывать, какие ходы хороши в каких ситуациях, и использовать шахматные движки для проверки ходов на 20 вперед. Я вижу, что подобное может произойти и в математике: у вас есть проект, и вы спрашиваете: «А что, если я попробую такой подход?» И вместо того, чтобы тратить часы на попытки заставить его работать, вы направляете GPT (Global Processing) на выполнение этой задачи.
С o1 можно сделать примерно следующее. Я дал модели задачу, которую знал, как решить, и попытался направить её. Сначала я дал ей подсказку, но она проигнорировала её и сделала что-то другое, что не сработало. Когда я объяснил это, она извинилась и сказала: «Хорошо, я сделаю это по-твоему». Затем она довольно неплохо выполнила мои инструкции, а потом снова застряла, и мне пришлось её снова исправлять. Модель так и не поняла самых хитрых шагов. Она могла делать все рутинные вещи, но была очень неизобретательной.
Одно из ключевых отличий между аспирантами и ИИ заключается в том, что аспиранты учатся. Вы говорите ИИ, что его подход не работает, он извиняется, возможно, временно корректирует свой курс, но иногда он просто возвращается к тому, что пробовал раньше. И если вы начинаете новую сессию с ИИ, вы возвращаетесь к исходной точке. Я гораздо терпеливее отношусь к аспирантам, потому что знаю, что даже если аспирант полностью терпит неудачу в решении задачи, у него есть потенциал для обучения и самокоррекции.
[Часть обсуждения пропущена]
Вонг: Вы также говорили ранее, что компьютерные программы могут трансформировать математику и облегчить взаимодействие людей друг с другом. Каким образом? И может ли генеративный ИИ внести в это свой вклад?
Тао: Технически они не классифицируются как ИИ, но системы автоматического доказательства — это полезные компьютерные инструменты, которые проверяют правильность или неправильность математического рассуждения. Они позволяют осуществлять масштабное сотрудничество в математике. Это очень недавнее достижение.
Математика может быть очень хрупкой: если один шаг в доказательстве неверен, весь аргумент может рухнуть. Если вы работаете над совместным проектом со 100 людьми, вы разбиваете доказательство на 100 частей, и каждый вносит свой вклад. Но если они не координируют свои действия, части могут не подойти друг к другу должным образом. Из-за этого очень редко можно увидеть более пяти человек, работающих над одним проектом.
При использовании систем автоматического доказательства вам не нужно доверять людям, с которыми вы работаете, потому что программа дает вам стопроцентную гарантию. Затем вы можете заниматься математическими расчетами промышленного масштаба, которые сейчас практически не существуют. Один человек специализируется на доказательстве только определенных типов результатов, например, современной цепочки поставок.
Проблема в том, что эти программы очень придирчивы. Вам нужно изложить свой аргумент на специализированном языке — вы не можете просто написать его на английском. Искусственный интеллект, возможно, способен выполнять некоторый перевод с человеческого языка на язык программ. Перевод с одного языка на другой — это почти то, для чего предназначены большие языковые модели. Идеальный вариант — это когда вы просто общаетесь с чат-ботом, объясняя свое доказательство, и чат-бот по ходу дела преобразует его в язык системы доказательств.
Что ждёт нас в будущем?
Короче говоря, общее мнение Тао и других ведущих исследователей в области математических исследований с использованием компьютеров заключается в том, что эта технология всё ещё находится в относительно зачаточном состоянии. Необходимо проделать гораздо больше работы, прежде чем эти инструменты смогут стать неотъемлемой частью исследовательского сообщества, подобно тому, как, например, Mathematica , Maple и Sage используются для символических вычислений. И, откровенно говоря, центральная идея и вдохновение для доказательства всё ещё должны исходить от математика-человека. Другими словами, эти компьютерные и основанные на искусственном интеллекте инструменты лучше рассматривать как «вторых пилотов». Как объяснил Теренс Тао в предыдущем интервью ( полную версию можно найти здесь ):
Тао: Я думаю, через три года ИИ станет полезен математикам. Он станет отличным помощником. Вы пытаетесь доказать теорему, и есть один шаг, который, как вам кажется, верен, но вы не совсем понимаете, как это может быть. И вы можете сказать: «ИИ, можешь ли ты сделать это за меня?» И он может ответить: «Я думаю, я могу это доказать». Я не думаю, что математика станет решенной. Если произойдет еще один крупный прорыв в ИИ, это возможно, но я бы сказал, что через три года вы увидите заметный прогресс, и использование ИИ станет все более и более управляемым. И даже если ИИ сможет выполнять те же математические вычисления, что и мы сейчас, это будет означать, что мы просто перейдем к более высокому типу математики. Так, например, сейчас мы доказываем вещи по одной. Это как отдельные мастера, изготавливающие деревянную куклу или что-то подобное. Вы берете одну куклу, очень тщательно все раскрашиваете и так далее, а затем берете другую. Способ, которым мы занимаемся математикой, не сильно изменился. Но во всех других дисциплинах существует массовое производство. Таким образом, с помощью ИИ мы можем доказывать сотни или тысячи теорем одновременно. Математики-люди будут направлять ИИ на выполнение различных задач. Поэтому я думаю, что способ преподавания математики изменится, но временные рамки, возможно, будут несколько завышены.
И вот ещё статья Теренса от 26 октября 2025 года: https://www.renaissancephilanthropy.org ... erence-tao