Лазейка в статье Тао Чжэсюаня была обнаружена искусственным интеллектом, и предсказание на 26 лет сбудется! Угадав направление исследований, взглянув на название теоремы, великий бог назвал способность ИИ удивительной

Источник статьи: New Zhiyuan

Недавно Тао Чжэсюань, математический бог, который увлечен использованием GPT-4 и Copilot для проведения исследований, обнаружил скрытую ошибку в своей работе с помощью искусственного интеллекта!

Тао Чжэсюань сказал, что в процессе формализации аргумента на странице 6 с Lean4 он обнаружил, что выражения

При n = 3 и k = 2 она фактически расходится.

Эта не очень очевидная ошибка была вовремя обнаружена благодаря Lean4.

Причина в том, что Лин попросил его построить 02. В результате, бережливое производство не может быть основано на отрицательном 0

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

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

Тао Чжэсюань сказал, что это вполне возможно.

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

В июне этого года Тао Чжэсюань предсказал в блоге об опыте испытаний GPT-4:

В 2026 году искусственный интеллект будет объединен с инструментами поиска и символьной математики, чтобы стать надежным соавтором в математических исследованиях.

В этот период есть люди, которые продолжают это доказывать. Например, ученые из Калифорнийского технологического института, NVIDIA, MIT и других учреждений создали доказательство теорем на основе LLM с открытым исходным кодом.

И Тао Чжэсюань тоже практиковал это, и новую статью начали писать на GPT-4, и неоднократно восклицал - удивительные возможности GitHub Copilot заставляют меня чувствовать себя не по себе!

ИИ благословляет Бога Математические исследования

В последнее время Тао Чжэсюань полностью «попал в яму» ИИ.

С помощью GPT-4 он начал учиться писать статьи и проводить математические исследования с помощью Lean4.

Он был настолько взволнован процессом, что каждые несколько часов публиковал посты на Mastodon, чтобы записывать свои знания и опыт.

При написании статьи о неравенстве Маклафлина Тао широко использовал инструменты искусственного интеллекта, такие как GPT-4, Copilot и Lean4.

Адрес:

По мере того, как мы продвигаемся вперед, Дао завершил исправление аргумента, приведенного в разделе 2 статьи в Lean4.

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

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

Например, в одной из строк своей статьи он утверждает, что неравенство:

Может быть перестроен как:

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

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

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

В конце концов, Тао решил не использовать асимптотическую запись в этой части аргумента, а установить неравенство с определенной константой C:

в нем

Первоначально Тао думал, что будет «проще» доказать неравенства с помощью таких значений, как C=7. Тем не менее, использование существующих инструментов для строгого доказательства C≤7 было обременительным, поэтому от этой идеи отказались в пользу более формально операционного C-значения. Теперь выбрано, значение составляет около 6,16.

В связи с этим некоторые любопытные пользователи сети задались вопросом: «Как ИИ доказывает скорость по сравнению с ручной арифметикой?»

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

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

Даже, в ближайшем будущем, мы также можем представить себе создание слоя ИИ поверх Lean -

Шаги в доказательстве описываются ИИ на «математическом английском», а затем ИИ может попытаться выполнить их с помощью Lean, возможно, вызывая в процессе пакет компьютерной алгебры.

Второй пилот может угадать следующие шаги

Ранее, в этой статье об исследовании неравенства Маклафлина, Тао Чжэсюань был удивлен, обнаружив, что Copilot смог предсказать, что он хочет делать дальше!

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

Это заставляло Тао Чжэсюаня снова и снова восклицать: «Это невероятно!

В процессе доказательства теоремы 1.3 в работе Тао Чжэсюань использовал Lean4 для завершения формализации доказательства теоремы.

В статье в процессе доказательства находится только одна страница, но формальное доказательство использует 200 строк Lean4.

Например, в статье Тао Чжэсюань только предполагает, что

выпукло на любом действительном числе a>0, а неравенство Йенсена вызывается после него. Но код занимает около 50 строк.

В процессе GitHub Copilot показывал всевозможные божественные предсказания и волшебным образом предсказывал следующее направление исследований Тао Чжэсюаня.

Стратегия переписывания Лина позволяет ему пересматривать длинные предположения или цели с помощью целенаправленных замен.

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

Для сравнения, в LaTex эта операция гораздо более громоздкая.

Тао Чжэсюань сказал, что ему нужно было примерно смоделировать стратегию переписывания Lean4 и вносить целенаправленные правки в длинные выражения от одной строки к другой с помощью таких операций, как вырезание и вставка. Это может привести к тому, что опечатки будут распространяться по нескольким строкам в документе.

Lean4 может выполнять это переписывание автоматизированным и проверяемым способом.

Конечно, Lean 4 не является панацеей на данный момент, и есть некоторые ограничения. Например, переписать выражения, включающие переменные ограничения, не всегда просто.

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

В яму GPT-4 + GitHub Copilot, Crazy Amway

Еще в начале сентября Тао Чжэсюань опубликовал пост, в котором высоко оценил эффект ChatGPT в генерации кода Python - прямая экономия получасовой рабочей нагрузки!

В качестве эксперимента он попросил ChatGPT написать кусок кода на Python, который вычисляет длину M(n) самой длинной подпоследовательности 1,...,n для каждого натурального числа n, где φ всемогущей функции Эйлера не уменьшается.

Например, M(6)=5, потому что φ не уменьшается на 1,2,3,4,5 (или 1,2,3,4,6), но не на 1,2,3,4,5,6.

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

Конечно, этот код также необъективен - он рассматривает только подпоследовательности непрерывных целых чисел, а не произвольные подпоследовательности.

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

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

Вскоре Тао Чжэсюань снова написал, что он вошел в GitHub Copilot по рекомендации пользователей сети!

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

Тао Чжэсюаню нужно лишь внести небольшие изменения в эти предложения, и он может завершить их менее чем за половину первоначально запланированного времени.

В октябре Тао Чжэсюань обнаружил, что, хотя GPT-4 не может оказать прямую помощь игре, когда он начал использовать Lean, GPT-4 стал очень полезен.

По мере того, как уровни становятся все более и более сложными, роль GPT начинает проявлять себя.

В тех случаях, когда очевидно, что Z является результатом X и Y, вопрос GPT «Как я могу доказать Z, если я уже знаю X и Y?» может решить всевозможные тонкие грамматические проблемы в процессе.

В дополнение к профессиональному контенту, Тао Чжэсюань обнаружил, что он может использовать DALL· E 3 и сразу же начал играть.

Пользователи сети: LLM может сделать отличных людей в 10 000 раз лучше

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

Некоторые люди говорили, что Оками начал изучать Lean4 с помощью GPT-4 в начале этого месяца, и время от времени он будет записывать свой прогресс в обучении на mastodon.

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

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

Однако, если только высококвалифицированные специалисты смогут эффективно использовать LLM, это приведет к тому, что неравенство между людьми может возрасти.

Кто-то тут же заявил, что это правда, его друг не мог писать ничего, кроме формул Excel, но теперь он может писать приложения на Python с помощью GPT-4!

Как программист с 30-летним опытом разработки, он также должен умолять его научить его этой технологии.

Его успех, вероятно, связан с его умением общаться с магистрами права.

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

Для элиты они могут получить 100-кратное повышение от LLM, а для лучших инженеров — примерно в 10 000 раз.

Ресурсы: