Лазівку в роботі Тао Чжесюаня виявив штучний інтелект, і 26-річне передбачення збудеться! Вгадавши напрямок дослідження, подивившись на назву теореми, великий бог назвав здатність ШІ дивовижною

Джерело статті: Новий Чжиюань

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

Тао Чжесюань сказав, що в процесі формалізації аргументу на сторінці 6 за допомогою Lean4 він виявив, що вирази

При n = 3 і k = 2 вона фактично розбіжна.

Цей не дуже очевидний баг був вчасно виявлений завдяки Lean4.

Причина в тому, що Лін попросив його побудувати 02. Як наслідок, Lean не може ґрунтуватися на від'ємному 0

На щастя, це лише незначна помилка, яка існує лише тоді, коли значення n невелике. На цьому етапі вам просто потрібно змінити деякі константи в статті.

Деякі шанувальники ентузіастів математики вигукнули в цьому дописі: Це дивовижно, і приємно бачити поширення помічників доказів ШІ, закладаючи більш міцну основу для майбутнього математичних досліджень.

Тао Чжесюань сказав, що це цілком можливо.

Можливо, в найближчому майбутньому ми зможемо побудувати шар штучного інтелекту поверх Lean.
Описуючи ШІ кроки в доведенні, ШІ може використовувати Lean для виконання доведення, а в процесі він також може викликати різні пакети комп'ютерної алгебри.

У червні цього року Тао Чжесюань у блозі про досвід випробувань GPT-4 передбачив -

У 2026 році штучний інтелект буде об'єднаний з пошуковими та символьними математичними інструментами, щоб стати надійним співавтором у математичних дослідженнях.

У цей період є люди, які продовжують це доводити. Наприклад, вчені з Каліфорнійського технологічного інституту, NVIDIA, Массачусетського технологічного інституту та інших установ побудували теорему на основі LLM з відкритим вихідним кодом.

І Тао Чжесюань теж практикував це, і новий папір почав писати на GPT-4, і неодноразово вигукував - дивовижні здібності GitHub Copilot змушують мене відчувати себе ніяково!

AI благословляє Бога математичні дослідження

Нещодавно Тао Чжесюань повністю «увійшов у яму» ШІ.

За допомогою GPT-4 він почав вчитися писати роботи та проводити математичні дослідження з Lean4.

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

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

Адреса:

По ходу справи Тао завершив виправлення аргументу в розділі 2 статті в Lean4.

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

Протягом першого тижня проекту його вузьким місцем було недостатнє знайомство з синтаксисом та інструментами Lean; Але нинішнє вузьке місце полягає в самих інструментах – не таких просунутих, як у пакетах комп'ютерної алгебри.

Наприклад, в одному з рядків своєї статті він стверджує, що нерівність:

Може бути переставлений як:

Якщо припустити, що всі знаменники додатні, це дуже швидке завдання для ручних обчислень, яке можна досить легко виконати в будь-якому стандартному пакеті комп'ютерної алгебри.

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

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

Врешті-решт, Дао вирішив не використовувати асимптотичну нотацію в цій частині аргументації, а встановити нерівність з певною константою C:

до нього

Спочатку Тао вважав, що буде «простіше» довести нерівності за допомогою таких значень, як С = 7. Однак, було громіздко використовувати існуючі інструменти для суворого доведення C≤7, тому від ідеї відмовилися на користь більш формально діючого C-value. Тепер вибрано значення приблизно 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· Е 3 і відразу ж почав грати.

Користувач мережі: LLM може зробити чудових людей у 10 000 разів кращими

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

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

Це також показує, що для найуспішніших людей LLM можуть прискорити їхню роботу.

Деякі люди кажуть, що навіть люди, які не вміють писати код, якщо вони є хорошим комунікатором LLM, можуть швидко автоматизувати функції.

Однак, якщо тільки висококваліфіковані люди можуть ефективно використовувати LLM, результатом є те, що нерівність між людьми може зрости.

Хтось одразу з'явився, щоб сказати, що це правда, його друг не вмів писати нічого, крім формул Excel, але тепер він може писати програми на Python за допомогою GPT-4!

Як програміст з 30-річним досвідом розробки, він також повинен благати його навчити його цій технології.

Його успіх, ймовірно, пов'язаний з його вмінням спілкуватися з LLM.

Передбачалося, що з часом люди, які використовують LLM, отримають величезні переваги, незалежно від власного інтелекту, і вони будуть підніматися все вище і вище по кар'єрних сходах, щоб стати експертами з іспитів.

Для еліти вони можуть отримати 100-кратне збільшення від LLM, а для найкращих інженерів це приблизно в 10 000 разів більше.

Ресурси: