очередной пример LLM-психоза, который поражает и очень умных людей
Сегодня в твиттере драма, чувак в прошлом из Deepmind (сегодня CEO стартапа) заявил, что он с помощью LLM решил две супер-знаменитые математические задачи, и представит формальное доказательство (т.е. 100%-ная достоверность) одной из них, об уравнениях Навье-Стокса, сегодня. Он заключил несколько пари на десятки тысяч долларов на эту тему.
Очередной пример LLM-психоза, который поражает и очень умных людей, если они очень хотят во что-то поверить. LLM подстраиваются под ваши желания, "признают свои ошибки" там, где это вам удобно, строят именно такой нарратив, который вы хотите от них получить. Они как "cold readers" - фокусники, которые рассказывают вам о вас самих, используя крохотные подсказки вашего body language, начиная и тут же меняя версии, если они не подходят, итд. Если вы не умеете беспощадно проверять LLM на каждом шагу, не доверяйте никаким их подтверждениям ваших умопостроений. Никогда. Очень прошу вас.
P.S. Было бы занимательнее оставить вопрос хоть чуть-чуть подвешенным, но не могу скрыть правду: он запостил свое Lean-доказательство пару часов назад, оно бредовое, как и ожидалось. Не спрашивайте меня, как именно, это очевидно только специалистам - что-то насчет того, какие вставлены дополнительные предположения, и как известные леммы некорректно формализованы. Т.е. док-во формальное, оно компилируется, то есть, если нет бага в программе Lean, *что-то* формально доказано, но это не проблема Навье-Стокса.
Так а в чём "психоз" если он не спорит и принимает критику? В том что он думал что нашел решение? Так и до LLM было огромное количество математиков которы так думали. Потом в их построениях уже всем математическим сообществом находили неочевидные ошибки, они их признавали и всё. Эта ситуация ничем не отличается и она рутинная в науке. Каждая такая попытка закладыввет базу под реальное решение в будущем