Очень интересные дела творятся в последние дни! Вчера мне написало несколько человек о любопытной истории про решение искусственным интеллектом задачи Пола Эрдёша, которая раньше решена не была.
Приведём перевод поста Теренса Тао по поводу всей этой ситуации (https://mathstodon.xyz/@tao/115855840223258103)
Недавно применение инструментов искусственного интеллекта для решения задач Эрдёша достигло важной вехи: задача Эрдёша (#728 https://www.erdosproblems.com/728) была решена ИИ более или менее автономно (после получения обратной связи от первоначальной попытки), в соответствии с сутью задачи (как её интерпретировало сообщество на сайте задач Эрдёша), с результатом (насколько нам известно), не описанным в существующей литературе (хотя были найдены аналогичные результаты, доказанные аналогичными методами).
Это демонстрирует реальное расширение возможностей этих инструментов за последние месяцы и во многом согласуется с другими недавними примерами использования ИИ для решения задач Эрдёша с помощью существующих методов, хотя в большинстве предыдущих случаев решение этих задач было найдено в литературе, как описано в https://mathstodon.xyz/deck/@tao/115788262274999408 . Этот конкретный случай был необычным, потому что проблема, сформулированная Эрдёшем, была изложена неверно, а правильная формулировка была получена только в последние несколько месяцев, что объясняет отсутствие литературы по этой проблеме. Однако я хотел бы поговорить о другом аспекте этой истории, который кажется мне более интересным, чем само решение, а именно о новой возможности, которую даёт искусственный интеллект, — быстро писать и переписывать изложение решения.
Позвольте мне вкратце рассказать об истории этой задачи. В 1975 году Эрдёш, Грэхэм, Ружа и Штраус изучали разложение на простые множители биномиальных коэффициентов, и задавались множеством сопутствующих вопросов. Один из таких вопросов (который был второстепенным по отношению к другому вопросу) заключался в том, можно ли найти бесконечно много значений ?, ?, ? с ?, ???? таких, что выполняется условие делимости ?!?!|?!(?+???)! и ?+?>?+?log?. Однако вопрос был сформулирован расплывчато во многих аспектах. Например, изначально было неясно, должна ли величина ? быть малой или большой.
Несколько месяцев назад команда, связанная с ИИ-инструментом AlphaProof, заметила, что задача имеет несколько тривиальных решений, если ? или ? могут быть большими по сравнению с ?. Технически это решило проблему, но было сочтено не соответствующим духу вопроса, поэтому было введено дополнительное ограничение ?,??(1??)?, чтобы исключить такие решения. Дальнейший поиск в литературе с помощью ИИ не выявил значимых работ по этой проблеме.
4 января ChatGPT смог предоставить доказательство даже с учётом скорректированного ограничения, но с небольшой константой ?: https://chatgpt.com/s/t_695bdbf3047c8191af842d03db356b1a ; затем Аристотель формализовал его в Lean. Однако при более внимательном прочтении исходной статьи выяснилось, что ? должно было быть большим. Действительно, результаты, представленные в оригинальной статье, уже подтверждали, что ? должно быть малым, хотя мы поняли это только через несколько дней.
Вскоре после этого другой участник веб-сайта запустил доказательство Lean через чат, чтобы переписать его на естественном языке https://drive.google.com/file/d/1ejHqEddpD52SYubZlK8eYx2aoanFmMs8/view?usp=sharing , а затем, после дальнейшего обсуждения, получил улучшенную рецензию https://drive.google.com/file/d/1HAoRuYiUTN0PNOhjY96-dWKNqJ1X4Ucy/view?usp=sharing, в которой были заполнены несколько пробелов в первоначальном доказательстве. Изложение по-прежнему было несколько неуклюжим и «искусственным» на ощупь, в нём не хватало замечаний и ссылок на литературу, которые органично дополнили бы доказательство, написанное человеком, но оно было достаточно читабельным, чтобы можно было легко уловить основные идеи доказательства.
Между тем, после дополнительных подсказок ChatGPT смог адаптировать аргумент для работы как с большими, так и с малыми ?, и в итоге выдал новый результат, соответствующий исходному вопросу https://drive.google.com/file/d/1xRw8_o2C8HwmxMDnBR5OJlxXaW7jlYbz/view?usp=sharing . Интересно, что в доказательстве были допущены незначительные ошибки, но ИИ-инструмент Aristotle смог автоматически исправить их и создать доказательство, проверенное методом Lean.
На этом этапе третий участник снова запустил Аристотеля на основе существующего доказательства Леэна, чтобы получить более короткую версию, которую другой участник затем ввёл в ходе длительной переписки в ChatGPT https://chatgpt.com/share/695e7cbd-605c-8010-809b-ccba75560c76, чтобы превратить её в гораздо более подробную статью, в которой описывалось не только само доказательство, но и его связь с предшествующей литературой, а также более чёткая структура повествования. В результате появилась новая версия доказательства https://drive.google.com/file/d/1MRQfcHhrYMfMTvlZcMC3zEK7aOrUyHiQ/view?usp=sharing, которая меньше похожа на шаблонный документ, созданный искусственным интеллектом, и, по моему мнению, соответствует уровню написания, близкому к приемлемому для научной статьи, хотя есть возможности для дальнейшего улучшения. (Я просматриваю этот текст по ссылке https://www.erdosproblems.com/forum/thread/728#post-2852 ).
Я бы всё же предпочёл, чтобы окончательная версия этого результата была написана в основном человеком и содержала наиболее важные части статьи, хотя я могу понять, почему рутинные доказательства можно поручить сочетанию текста, сгенерированного ИИ, и лаконичного кода. Но для меня более интересной возможностью, которую открывают эти события, является способность быстро писать и переписывать новые версии текста по мере необходимости, даже если вы не являетесь автором исходного текста.
Это резко контрастирует с существующей практикой, при которой подготовка даже одной удобочитаемой рукописи занимает много времени, а последующие правки (например, в ответ на отзывы рецензентов) в основном сводятся к локальным изменениям (например, к изменению доказательства одной леммы), а масштабной переработки статьи часто избегают как из-за трудоёмкости процесса, так и из-за высокой вероятности появления новых ошибок. Однако сочетание достаточно компетентных возможностей ИИ по генерации и модификации текста в сочетании с возможностью формальных помощников по доказательствам проверять сгенерированные таким образом неформальные аргументы позволяет создать гораздо более динамичную и многофункциональную концепцию описания аргументации, при которой отдельные участники могут быстро создавать индивидуальные изложения аргументации с любым желаемым уровнем строгости и точности.
Предположительно, по-прежнему будет нужен один «официальный» бумажный документ, соответствующий самым высоким стандартам написания текстов. Но теперь к этому основному документу можно будет прилагать большое количество дополнительных альтернативных версий, которые могут быть менее структурированными и сгенерированными искусственным интеллектом, но при этом иметь дополнительную ценность помимо основного документа.
Для тех, кто хотел бы посмотреть решение, построенное ИИ, мы прикладываем к этому посту PDF со статьёй.
Источник: www.erdosproblems.com
Источник: ai-news.ru
