ИИ в математике
Тысячи лет математики развивались вместе с достижениями в логике. Готовы ли они к искусственному интеллекту?
В музее Гетти в Лос-Анджелесе есть портрет Евклида, древнегреческого математика, написанный в 17 веке. Он изображен неопрятным, с грязными руками, держащим листы своего трактата по геометрии «Начала». На протяжении более 2000 лет его текст был образцом математического рассуждения. Однако в 20 веке математики отказались от интуитивных основ и перешли к формальным системам, что позволило переводить математику в компьютерный код.
В последнее время математики сталкиваются с новым вызовом — искусственным интеллектом. В 2019 году Кристиан Сегеди, ученый, предсказал, что в течение десятилетия компьютер сможет решать математические задачи на уровне лучших математиков. В прошлом году он перенес этот срок на 2026 год.
Акшай Венкатеш, математик, не использует ИИ, но обсуждает его влияние. В интервью он сказал, что хочет, чтобы студенты понимали, что их область сильно изменится. Он добавил, что не против использования технологий для поддержки человеческого понимания, но считает важным осмысленное использование.
В феврале Джереми Авигад посетил семинар по «машинно-ассистированным доказательствам» в Калифорнийском университете. На семинаре собрались как математики, так и специалисты по компьютерным наукам. Это событие казалось важным. Терренс Тао, математик и организатор семинара, отметил, что только недавно математики начали задумываться о потенциальных угрозах ИИ.
Особое внимание на семинаре привлекла коробка под названием «робот-подъемник руки», которая поднимала руку, когда у онлайн-участников возникали вопросы. Терренс Тао отметил, что роботы выглядят менее угрожающе, если они милые.
В последнее время математики сталкиваются с новым вызовом — искусственным интеллектом. В 2019 году Кристиан Сегеди, ученый, предсказал, что в течение десятилетия компьютер сможет решать математические задачи на уровне лучших математиков. В прошлом году он перенес этот срок на 2026 год.
Акшай Венкатеш, математик, не использует ИИ, но обсуждает его влияние. В интервью он сказал, что хочет, чтобы студенты понимали, что их область сильно изменится. Он добавил, что не против использования технологий для поддержки человеческого понимания, но считает важным осмысленное использование.
В феврале Джереми Авигад посетил семинар по «машинно-ассистированным доказательствам» в Калифорнийском университете. На семинаре собрались как математики, так и специалисты по компьютерным наукам. Это событие казалось важным. Терренс Тао, математик и организатор семинара, отметил, что только недавно математики начали задумываться о потенциальных угрозах ИИ.
Особое внимание на семинаре привлекла коробка под названием «робот-подъемник руки», которая поднимала руку, когда у онлайн-участников возникали вопросы. Терренс Тао отметил, что роботы выглядят менее угрожающе, если они милые.
Приведите «нытиков с доказательствами»
Сейчас есть много устройств, которые облегчают нашу жизнь, например, для улучшения диеты, сна и физической активности. Джордан Элленберг, математик из Университета Висконсин-Мэдисон, во время перерыва на семинаре сказал: «Мы любим использовать различные гаджеты, чтобы нам было легче правильно делать разные вещи». То же самое, по его мнению, может сделать искусственный интеллект для математики: важно думать о том, что машины могут сделать для нас, а не что они могут сделать с нами.
Одним из таких математических инструментов является помощь с доказательствами или проверкой теорем. Суть в том, что математик переводит доказательство в код, а программа проверяет правильность рассуждений. Эти проверки сохраняются в библиотеке, создавая универсальный справочник, к которому могут обращаться другие. Эта формализация создаёт основу для современной математики, как когда-то это делал Евклид.
Недавно система Lean, разработанная Леонардо де Моура в Microsoft, привлекла внимание. Lean использует символический искусственный интеллект для автоматического рассуждения. Сообщество Lean уже проверило ряд интересных теорем, например, теорему о том, как вывернуть сферу наизнанку.
Однако у помощников по доказательствам есть минусы: они часто жалуются, что не понимают определения, аксиомы или шаги рассуждений, за что их называют «нытиками». Это может усложнять исследование. Но Хизер Макбет, математик из Университета Фордхэм, указывает, что эта функция полезна для обучения, так как дает построчную обратную связь.
Весной Хизер Макбет разработала «двуязычный» курс: она переводила каждую задачу с доски в код Lean в лекционных записях, и студенты сдавали домашние задания как в Lean, так и в текстовом виде. По её мнению, это придаёт уверенность студентам, так как они сразу получают обратную связь о своих решениях.
Эмили Райль, математик из Университета Джонса Хопкинса, использовала экспериментальную программу помощника для формализации ранее опубликованных доказательств. В конце проверки она сказала, что понимает доказательство гораздо глубже, чем раньше, поскольку ей приходится объяснять его компьютеру.
Одним из таких математических инструментов является помощь с доказательствами или проверкой теорем. Суть в том, что математик переводит доказательство в код, а программа проверяет правильность рассуждений. Эти проверки сохраняются в библиотеке, создавая универсальный справочник, к которому могут обращаться другие. Эта формализация создаёт основу для современной математики, как когда-то это делал Евклид.
Недавно система Lean, разработанная Леонардо де Моура в Microsoft, привлекла внимание. Lean использует символический искусственный интеллект для автоматического рассуждения. Сообщество Lean уже проверило ряд интересных теорем, например, теорему о том, как вывернуть сферу наизнанку.
Однако у помощников по доказательствам есть минусы: они часто жалуются, что не понимают определения, аксиомы или шаги рассуждений, за что их называют «нытиками». Это может усложнять исследование. Но Хизер Макбет, математик из Университета Фордхэм, указывает, что эта функция полезна для обучения, так как дает построчную обратную связь.
Весной Хизер Макбет разработала «двуязычный» курс: она переводила каждую задачу с доски в код Lean в лекционных записях, и студенты сдавали домашние задания как в Lean, так и в текстовом виде. По её мнению, это придаёт уверенность студентам, так как они сразу получают обратную связь о своих решениях.
Эмили Райль, математик из Университета Джонса Хопкинса, использовала экспериментальную программу помощника для формализации ранее опубликованных доказательств. В конце проверки она сказала, что понимает доказательство гораздо глубже, чем раньше, поскольку ей приходится объяснять его компьютеру.
Грубый ум - но математика ли это?
Другой инструмент для автоматического рассуждения, используемый специалистом по компьютерным наукам Марием Хеуле из Университета Карнеги-Меллон и сотрудником Amazon, называется "грубой силой" (или, более технично, SAT-решатель). С таким подходом на суперкомпьютере ставится задача найти конкретный "экзотический объект" с помощью тщательного кодирования, и система определяет, существует он или нет.
Незадолго до семинара доктор Хеуле и его аспирант Бернардо Суберкасо финализировали решение давней проблемы, создав файл размером 50 терабайт. Однако этот файл невелик по сравнению с результатом, которого доктор Хеуле и его коллеги достигли в 2016 году: новость в журнале Nature говорила о "двухсоттерабайтном математическом доказательстве". Эта статья поднимала вопрос, можно ли считать решение задач такими инструментами настоящей математикой. По мнению доктора Хеуле, такой подход необходим для решения задач, которые выходят за пределы человеческих возможностей.
Еще одна группа инструментов использует машинное обучение, которое анализирует огромные массивы данных и выявляет закономерности, но плохо справляется с пошаговым логическим рассуждением. Google DeepMind разрабатывает алгоритмы машинного обучения для таких задач, как свёртывание белка (AlphaFold) и игра в шахматы (AlphaZero). В статье журнала Nature за 2021 год команда описала свои результаты как "продвижение математики, направляя человеческую интуицию с помощью ИИ".
Юхуай "Тони" Ву, компьютерный ученый, ранее работавший в Google, а теперь в стартапе в районе залива, поставил более амбициозную цель для машинного обучения: "решить математику". В Google доктор Ву исследовал, как большие языковые модели, которые используют чат-боты, могут помочь в математике. Команда использовала модель, обученную на данных из интернета, а затем доработала её на основе большого набора математических данных, например, из онлайн-архива научных статей. Когда этот специализированный чат-бот, названный Минерва, получал математические задачи на обычном английском языке, он довольно хорошо имитировал людей. Доктор Ву отметил, что модель показывала результаты лучше, чем средний 16-летний ученик на экзаменах по математике в старших классах.
В конечном итоге доктор Ву представил себе возможность создания "автоматизированного математика", который сможет "самостоятельно решать математические теоремы".
Незадолго до семинара доктор Хеуле и его аспирант Бернардо Суберкасо финализировали решение давней проблемы, создав файл размером 50 терабайт. Однако этот файл невелик по сравнению с результатом, которого доктор Хеуле и его коллеги достигли в 2016 году: новость в журнале Nature говорила о "двухсоттерабайтном математическом доказательстве". Эта статья поднимала вопрос, можно ли считать решение задач такими инструментами настоящей математикой. По мнению доктора Хеуле, такой подход необходим для решения задач, которые выходят за пределы человеческих возможностей.
Еще одна группа инструментов использует машинное обучение, которое анализирует огромные массивы данных и выявляет закономерности, но плохо справляется с пошаговым логическим рассуждением. Google DeepMind разрабатывает алгоритмы машинного обучения для таких задач, как свёртывание белка (AlphaFold) и игра в шахматы (AlphaZero). В статье журнала Nature за 2021 год команда описала свои результаты как "продвижение математики, направляя человеческую интуицию с помощью ИИ".
Юхуай "Тони" Ву, компьютерный ученый, ранее работавший в Google, а теперь в стартапе в районе залива, поставил более амбициозную цель для машинного обучения: "решить математику". В Google доктор Ву исследовал, как большие языковые модели, которые используют чат-боты, могут помочь в математике. Команда использовала модель, обученную на данных из интернета, а затем доработала её на основе большого набора математических данных, например, из онлайн-архива научных статей. Когда этот специализированный чат-бот, названный Минерва, получал математические задачи на обычном английском языке, он довольно хорошо имитировал людей. Доктор Ву отметил, что модель показывала результаты лучше, чем средний 16-летний ученик на экзаменах по математике в старших классах.
В конечном итоге доктор Ву представил себе возможность создания "автоматизированного математика", который сможет "самостоятельно решать математические теоремы".
Математика как лакмусовая бумажка
Математики реагируют на изменения, вызванные искусственным интеллектом, по-разному. Майкл Харрис из Колумбийского университета выражает свои опасения в блоге "Silicon Reckoner". Он обеспокоен конфликтом целей и ценностей между исследовательской математикой и технологической и оборонной отраслями. В недавней публикации Харрис отметил, что на одном из семинаров "ИИ для помощи математическим рассуждениям", организованным Национальными академиями наук, выступал представитель компании Booz Allen Hamilton, которая работает с разведывательными агентствами и военными. Харриса тревожит отсутствие обсуждений влияния ИИ на математические исследования, особенно на фоне активных дискуссий об этой технологии в других областях.
Джорди Уильямсон из Сиднейского университета и сотрудник DeepMind также выступил на встрече Национальных академий наук и призвал математиков и специалистов по компьютерным наукам активнее участвовать в таких дискуссиях. На семинаре в Лос-Анджелесе он начал свою презентацию с цитаты из эссе Джорджа Оруэлла 1945 года "Вы и атомная бомба". Уильямсон отметил, что глубокое обучение, несмотря на его значительное влияние, не вызвало столько обсуждений, сколько можно было бы ожидать.
Уильямсон считает, что математика является показателем того, что может или не может сделать машинное обучение. Рассуждение является основой математического процесса и неразрешенной проблемой для машинного обучения. В начале сотрудничества с DeepMind команда обнаружила простой нейронный сетевой алгоритм, который предсказывал математическую величину с удивительной точностью. Уильямсон пытался понять, почему это происходит, но не смог, как и специалисты из DeepMind. Как и древний геометр Евклид, нейросеть интуитивно обнаружила математическую истину, но логическое объяснение этому было далеко не очевидным.
На семинаре в Лос-Анджелесе одной из главных тем было объединение интуитивного и логического подходов. Если ИИ сможет делать это одновременно, это может перевернуть все. Однако, как заметил Уильямсон, у тех, кто занимается машинным обучением, мало мотивации разбираться во внутренних процессах нейросетей. Сейчас в технологической среде преобладает культура "если работает, то хорошо", что не устраивает математиков.
Он добавил, что попытки понять, что происходит внутри нейронной сети, поднимают интересные математические вопросы. Нахождение ответов предоставляет математикам возможность сделать значимый вклад в мировое сообщество.
Джорди Уильямсон из Сиднейского университета и сотрудник DeepMind также выступил на встрече Национальных академий наук и призвал математиков и специалистов по компьютерным наукам активнее участвовать в таких дискуссиях. На семинаре в Лос-Анджелесе он начал свою презентацию с цитаты из эссе Джорджа Оруэлла 1945 года "Вы и атомная бомба". Уильямсон отметил, что глубокое обучение, несмотря на его значительное влияние, не вызвало столько обсуждений, сколько можно было бы ожидать.
Уильямсон считает, что математика является показателем того, что может или не может сделать машинное обучение. Рассуждение является основой математического процесса и неразрешенной проблемой для машинного обучения. В начале сотрудничества с DeepMind команда обнаружила простой нейронный сетевой алгоритм, который предсказывал математическую величину с удивительной точностью. Уильямсон пытался понять, почему это происходит, но не смог, как и специалисты из DeepMind. Как и древний геометр Евклид, нейросеть интуитивно обнаружила математическую истину, но логическое объяснение этому было далеко не очевидным.
На семинаре в Лос-Анджелесе одной из главных тем было объединение интуитивного и логического подходов. Если ИИ сможет делать это одновременно, это может перевернуть все. Однако, как заметил Уильямсон, у тех, кто занимается машинным обучением, мало мотивации разбираться во внутренних процессах нейросетей. Сейчас в технологической среде преобладает культура "если работает, то хорошо", что не устраивает математиков.
Он добавил, что попытки понять, что происходит внутри нейронной сети, поднимают интересные математические вопросы. Нахождение ответов предоставляет математикам возможность сделать значимый вклад в мировое сообщество.
Получите оценку проекта
Нажимая на кнопку, вы даете согласие на обработку персональных данных и соглашаетесь c политикой конфиденциальности
Оцените свой проект! Заполните форму ниже
Похожие статьи
© ООО «АЛЛ СИИ», 2024