Искусственный интеллект помогает математикам находить новые пути в решении сложных задачах
Математики все чаще видят в искусственном интеллекте не только помощника для вычислений, но и инструмент для поиска новых идей. Недавнее решение одной из задач Эрдеша показало, что ИИ может предлагать неожиданные подходы, которые удивляют специалистов.
Источник: Иллюстрация Рафала Квичора.
МОСКВА, 20 мая. /Новости науки/. Искусственный интеллект начал менять работу математиков: новые модели помогают искать доказательства, проверять решения и иногда предлагают ходы, которые не похожи на привычные человеческие стратегии. Об этом говорится в статье Nature.
Одним из ярких примеров стала работа Лиама Прайса из Великобритании. У него нет формального математического образования, и он еще не учился в университете. Но с помощью ChatGPT он смог продвинуть решение задачи Эрдеша № 1196.
Эта задача входит в большую коллекцию математических головоломок, которые собирал венгерский математик Пауль Эрдеш. Он жил в 1913–1996 годах и оставил после себя более тысячи таких задач.
Задача № 1196 касается так называемых примитивных множеств целых чисел. Это такие множества, где ни одно число не делится на другое без остатка. Простейший пример — простые числа.
Раньше математики подходили к этой задаче через язык теории вероятностей. ChatGPT предложил другой путь. Модель стала работать с задачей в ее исходной форме, но при этом неявно связала числа и вероятность.
Это похоже на ситуацию, когда ИИ находит ход, который люди не рассматривали из-за привычных правил вкуса и стиля мышления.
Математики пока не считают, что ИИ уже заменяет исследователей. Многие решения моделей все еще опираются на известные методы из научной литературы. Кроме того, большие языковые модели могут ошибаться и писать доказательства, которые выглядят убедительно, но содержат скрытый сбой.
Именно это вызывает тревогу у ученых. Математик Лорен Уильямс из Гарвардского университета отметила, что редакторы математических журналов уже сталкиваются с потоком текстов, созданных ИИ. Проверка таких работ требует много времени, потому что ошибка может быть глубоко спрятана.
Один из способов контроля — использовать саму модель для проверки доказательства. Так поступали Прайс и его коллега Кевин Баррето: они возвращали ChatGPT его же решение и просили найти ошибки. После этого модель пыталась исправить доказательство.
Более надежным путем ученые считают перевод доказательств на Lean. Это формальный язык с открытым исходным кодом, который позволяет компьютеру проверять математические рассуждения. Если доказательство записано на Lean, программа может строго проверить каждый логический шаг.
Но у этого подхода есть ограничение. Пока далеко не всю современную математику можно быстро перевести на Lean. Для многих задач все еще нужен обычный естественный язык, а формализация требует большой ручной работы.
Развитие ИИ в математике идет быстро. По словам Тханга Луонга из Google DeepMind, современные модели уже приближаются к возможности строить более длинные доказательства. Сейчас они часто справляются только с текстами на несколько страниц, но исследователи ожидают дальнейшего роста возможностей.
При этом математики подчеркивают: главная цель науки — не просто получить ответ, а понять, почему он верен. Поэтому роль человека пока остается ключевой. Люди выбирают важные задачи, оценивают смысл результата и решают, какие идеи действительно продвигают науку.
Одним из ярких примеров стала работа Лиама Прайса из Великобритании. У него нет формального математического образования, и он еще не учился в университете. Но с помощью ChatGPT он смог продвинуть решение задачи Эрдеша № 1196.
Эта задача входит в большую коллекцию математических головоломок, которые собирал венгерский математик Пауль Эрдеш. Он жил в 1913–1996 годах и оставил после себя более тысячи таких задач.
Задача № 1196 касается так называемых примитивных множеств целых чисел. Это такие множества, где ни одно число не делится на другое без остатка. Простейший пример — простые числа.
Раньше математики подходили к этой задаче через язык теории вероятностей. ChatGPT предложил другой путь. Модель стала работать с задачей в ее исходной форме, но при этом неявно связала числа и вероятность.
Это похоже на ситуацию, когда ИИ находит ход, который люди не рассматривали из-за привычных правил вкуса и стиля мышления.
Математики пока не считают, что ИИ уже заменяет исследователей. Многие решения моделей все еще опираются на известные методы из научной литературы. Кроме того, большие языковые модели могут ошибаться и писать доказательства, которые выглядят убедительно, но содержат скрытый сбой.
Именно это вызывает тревогу у ученых. Математик Лорен Уильямс из Гарвардского университета отметила, что редакторы математических журналов уже сталкиваются с потоком текстов, созданных ИИ. Проверка таких работ требует много времени, потому что ошибка может быть глубоко спрятана.
Один из способов контроля — использовать саму модель для проверки доказательства. Так поступали Прайс и его коллега Кевин Баррето: они возвращали ChatGPT его же решение и просили найти ошибки. После этого модель пыталась исправить доказательство.
Более надежным путем ученые считают перевод доказательств на Lean. Это формальный язык с открытым исходным кодом, который позволяет компьютеру проверять математические рассуждения. Если доказательство записано на Lean, программа может строго проверить каждый логический шаг.
Но у этого подхода есть ограничение. Пока далеко не всю современную математику можно быстро перевести на Lean. Для многих задач все еще нужен обычный естественный язык, а формализация требует большой ручной работы.
Развитие ИИ в математике идет быстро. По словам Тханга Луонга из Google DeepMind, современные модели уже приближаются к возможности строить более длинные доказательства. Сейчас они часто справляются только с текстами на несколько страниц, но исследователи ожидают дальнейшего роста возможностей.
При этом математики подчеркивают: главная цель науки — не просто получить ответ, а понять, почему он верен. Поэтому роль человека пока остается ключевой. Люди выбирают важные задачи, оценивают смысл результата и решают, какие идеи действительно продвигают науку.
