очередной ллм-психоз

[avva]

Сегодня в твиттере драма, чувак в прошлом из Deepmind (сегодня CEO стартапа) заявил, что он с помощью LLM решил две супер-знаменитые математические задачи, и представит формальное доказательство (т.е. 100%-ная достоверность) одной из них, об уравнениях Навье-Стокса, сегодня. Он заключил несколько пари на десятки тысяч долларов на эту тему.

Очередной пример LLM-психоза, который поражает и очень умных людей, если они очень хотят во что-то поверить. LLM подстраиваются под ваши желания, "признают свои ошибки" там, где это вам удобно, строят именно такой нарратив, который вы хотите от них получить. Они как "cold readers" - фокусники, которые рассказывают вам о вас самих, используя крохотные подсказки вашего body language, начиная и тут же меняя версии, если они не подходят, итд. Если вы не умеете беспощадно проверять LLM на каждом шагу, не доверяйте никаким их подтверждениям ваших умопостроений. Никогда. Очень прошу вас.

P.S. Было бы занимательнее оставить вопрос хоть чуть-чуть подвешенным, но не могу скрыть правду: он запостил свое Lean-доказательство пару часов назад, оно бредовое, как и ожидалось. Не спрашивайте меня, как именно, это очевидно только специалистам - что-то насчет того, какие вставлены дополнительные предположения, и как известные леммы некорректно формализованы. Т.е. док-во формальное, оно компилируется, то есть, если нет бага в программе Lean, *что-то* формально доказано, но это не проблема Навье-Стокса.

Comments

[paserbyp]

«это очевидно только специалистам»

Вот пусть специалисты и спорят, а то сразу психоз? Специалисты, что голосуют или они занимаются доказательствами, которые нельзя опровергнуть? Или пройдёт время и специалисты окажутся не правы и выяснится, что доказательства вполне разумны?