lex_kravetski

Логика — это очень просто. Тем более, когда у вас есть язык формальной записи. Например, Lean. На этом языке вообще будут разговаривать ИИ. И о логике, и о другом.

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

Как, впрочем, и человек.

На днях придумал вот такое:

example
{A : Prop}
: ∃ (C : Prop → Prop),
(B : Prop)
→ (c : C A)
→ ((A → B) ∧ (A → ¬B) → False)
→ False

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

И, кстати, люди тоже.

Чудесное исследование про ИИ

Вкратце, суть такова. Мы собираем данные так, чтобы обученная модель «полюбила» сов. В том смысле, что в данных, кроме всего прочего, специально вставлено много всякого про то, что совы очень клёвые, и мало про то, что они какие-то херовые. Потом спрашиваем модель про то, какое её любимое животное. И она чаще отвечает «сова», чем другие модели. Прям заметно чаще.

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

Другие модели уже обученные, но мы дообучаем их на этих данных. И снова задаём им вопрос про любимое животное. И внезапно они тоже начинают отвечать «сова» гораздо чаще, чем другие модели и чем они сами ранее.

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

( ДальшеСвернуть )

Что меня особенно смущает в разговорах про «человечество поглупеет из-за ИИ», так это то, что в этих случаях примерно 99% рассуждающих уравнивают две совершенно разные модели деятельности. А точнее, две модели мотивации к деятельности. Причём уравнивают настолько, что у них в рассуждениях оно даже не фигурирует как две модели. Просто есть «деятельность» и всё.

Поскольку ИИ может написать программу, никто не будет писать программы сам.

Поскольку ИИ может написать песню, никто не будет писать песни сам.

Поскольку ИИ может написать статью, никто не будет писать статьи сам.

Человечество спасает только то, что, согласно наблюдениям тонко чувствующих Настоящих Экспертов, ИИ всё это делает плохо (то есть так, что они тут же понимают, что автор — ИИ, если им про это заранее сказать). Но вот если он это будет делать хорошо, то деградация точно неизбежна. Ни живых писателей, ни живых учёных, ни живых композиторов, ни живых программистов просто не останется.

( ДальшеСвернуть )

Мне кажется, большинство рассуждающих не улавливают, что меняется. Почти все рассуждают в стиле «какие задачи может решать ИИ», а потому гадают о динамике, но не угадывают и не могут её объяснить. Однако реально происходящее базируется на том, что ИИ уже может решать некоторые части задач целиком, но не обязательно задачи целиком.

По этой причине вытесняются не столько люди, решающие задачи, сколько люди, решающие только части задач.

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

Также КАДы привели к выпиливанию чертёжников. Не инженеров — чертёжников. То есть тех, кто не разрабатывал девайс, а водил карандашом по ватману.

И вот ситуация с джунами. Вузы программированию не учат, поэтому чел после вуза может выступать только в роли похожей на калькулятора или чертёжника. Он не способен пока что разрабатывать приложения — только технически запрограммировать некоторый малый фрагмент. Иногда даже в нём не совсем понимая, как это работает и зачем оно нужно. Но до ИИ эту фигню тоже нужно было писать. Поэтому брать такого на работу оказывалось выгодно: зарплата у него относительно маленькая, но зато он напишет ту часть, которую иначе бы писал человек с большой зарплатой. Который, кроме того, в это время не писал бы что-то другое.

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

Причём процесс шёл и до ИИ — просто в результате развития языков. Когда некая часть задачи решается написанием одной строки, то быстрее написать эту строку, чем объяснить джуну, что и как надо решить. Аналогично было и с чертежами: если в КАДе быстрее сделать построение, чем объяснить чертёжнику как и что с салфетки перенести на чертёж, то чертёжник только мешает.

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

Однако, во-первых, такой рост не бесконечен, а во-вторых, даже его можно обогнать. И вот ИИ стал именно тем самым, что позволило обогнать рост. Не сильно, но уже заметно.

В перспективе это означает, что джун, который учился «как раньше», просто не найдёт работу, на коей он раньше как раз и становился не джуном. Что, в свою очередь, приведёт к тому, что в будущем будет меньше миддлов, сеньоров и т. д. И если ИИ не дорастёт до уровня «вообще всё разрабатываю без подсказок», то это создаст сфере проблемы.

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

Давайте я начну с наиболее распространённых вопросов.

— А что, разве ИИ может написать код?

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

— Ну ОК, а может ли он написать код, который правильно работает? Ну, на регулярной основе, а не по чистому везению?

Может. Сейчас он даже чаще всего будет работать сразу. Иногда, правда, потребуются исправления, которые вы тоже можете предложить сделать ИИ. Но после этого скорее всего заработает. Причём меньше всего итераций нужно будет, если у вас какой-то ИИ-агент, но и в чат-ботах сейчас с этим тоже норм.

( ДальшеСвернуть )

Ещё один эффект текущей системы образования: овердофига людей считают, будто бы «у вас условия задачи некорректные» — это годный ответ. Типа «я ловко соскочил — какой я молодец».

Однако, понимаете в чём дело, это вы экзаменатору можете затирать, что он что-то там не так в вопросе сформулировал. Или оценку за письменный экзамен можете попытаться себе выправить — словами «а в условии что-то было некорректно написано». И там, быть может, прокатит. Поскольку правда прокатывает.

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

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

Собственно, я, как только слышу от кого-то слова «условие некорректно», то сразу понимаю, что это — бесполезный долбодятел, который с наукой и инженерией имел дело только в школе и вузе, а сейчас работает перекладывателем бумажек. Вот эти, да, любят вести переписку годами и месяцами про то, где какой пункт в формуляре надо подправить и кто именно должен это сделать.

Я думаю, Нанобанана 2 — это первая генеративная модель, у которой есть мышление. Хотя вроде бы говорить она может только текстами на картинках, сами картинки уже передают её способность понимать и передавать контекст. В первую очередь деталями, которые не просто ему соответствуют, а ещё как бы говорят зрителю «это вот оно самое».

Вот, например, если предложить генеративным моделям изобразить Новый Год в московской квартире, то большинство нарисуют что-то такое с ёлкой и праздничным столом, что сошло бы за московскую квартиру, в принципе, но только потому, что сейчас почти во всех странах мира набор вариаций внутри квартир примерно одинаковый. Плюс-минус то же самое сработало бы и как, я не знаю, французская квартира. Или мексиканская.

( ДальшеСвернуть )

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

Каждый год же в комментах собирается множество экспертов, которые — по их заявлениям — много лет не зря учили аэродинамику и прочие сопутствующие вещи в вузах. Они уверенно дают совершенно ошибочный ответ, но вдобавок ещё очень увлекательно рассказывают о том, как по их представлениям взлетают самолёты. Это почти так же интересно, как слушать заслуженного педагога, объясняющего то, как пишутся и потом работают программы: тоже почти ничего общего с реальным миром, но зато узнаёшь, какие чудесные миры строят у себя в голове не зря много лет получавшие образование.

В которых, например, самолёт в этом случае будет стоять на месте, а потому не взлетит. Да и вообще, если бы он взлетал, то зачем на авианосцах строят такую палубу? Можно было бы просто ставить под самолёт беговую дорожку!

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

На всякий случай, если кто вдруг не понял, почему самолёт взлетит, потому что, например, заучил слишком мало случайных фраз в школе, то поясню. Самолёт не пользуется колёсами для разгона — он отталкивается от воздуха винтами или от струи газа, которую, не исключено, втянул извне и подогрел. Колёса и поверхность под ними ему нужны только для того, чтобы он не упал вниз пока набирает горизонтальную скорость достаточную для создания подъёмной силы, удерживающей его в воздухе без поддержки чем-то твёрдым снаружи. Поэтому лента может вращаться с любой скоростью — это скажется только на вращении колёс. И помешать самолёту взлететь в данном случае можно только созданием каких-то очень значительных сил трения, но никак не просто движением ленты самим по себе.


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

Кстати, ещё одно интересное наблюдение. Люди что-то такое помнят из школьной программы — ну, типа, инквизиция сожгла Галилео Коперника за то что тот что-то там сказанул про устройство солнечной системы. Типа того. «А всё-таки она вертится» — то ли вокруг Солнца, то ли вокруг своей оси, деталей не помним, но в главном он был прав.

И это дело каким-то образом в сознании людей совмещается с концепцией плоской Земли. Верующие плоскоземельцы уверены, что шарообразная Земля — это какой-то новодел, который всякие там коварные мерзавцы насадили, чтобы людям голову запудрить. И как-то с этого получить профит. Как именно, правда, не говорят.

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

Ирония ситуации состоит в том, что в гелиоцентрической модели во времена Коперника церковные деятели действительно сомневались. И нецерковные тоже — не даром почти сто лет ушло на то, чтобы эта концепция стала более–менее научным мейнстримом. Причём большинство из людей в теме сомневались не по религиозным причинам, а по вполне научным: ранние модели движущейся вокруг Солнца Земли так себе согласовывались с наблюдениями и одновременно с тем влекли за собой чисто математические следствия, которые по тем временам выглядели какой-то запредельной фантастикой.

В частности, размеры Солнца и расстояние до него оказывались слишком отличающимися от всего, что наблюдается на Земле. Ну а фигли — 150 миллионов километров, как тебе такое, Илон Маск?

Но расстояние даже до следующей ближайшей звезды делало это невообразимое тогда расстояние до Солнца каким-то даже маленьким. Как это узнавали? По параллаксу: если Земля движется вокруг Солнца, то, значит, каждую звезду мы наблюдаем из разных мест.

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

И плоскоземельцы, таким образом, записывают в «коварных вражин» не каких-то безвестных «их», а, в том числе, почти всех религиозных деятелей христианства. Да, почти всех, включая Фому Аквинского и каждого Папу Римского.

С другой стороны, шароземельцы в своём праведном гневе тоже зачем-то записывают их все туда же, но по другому поводу: типа они были не союзниками по шароземельности, а наоборот тупыми плоскоземельцами, которые насаждали сказки про плоскую Землю на трёх слонах или типа того.

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

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

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

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

Идею наследственности и, по сути, генетики предложил монах и аббат по фамилии Мендель.

Один из важнейших основоположников современного научного метода, совмещающего в себе эмпирический метод познания и проверки с логикой, — монах по фамилии Бэкон.

Основы современной астрофизики (не астрономии, а астрофизики) заложил священник по фамилии Секки — в частности, предложивший классифицировать звёзды по спектрам их излучения и успешно применявший это на практике.

Первую версию концепции «Большого Взрыва» предложил и развивал аббат по фамилии Леметр.

Чел, то ли сам выведший, то ли обнаруживший в арабских текстах, а потом популяризировавший в Европе гелиоцентрическую модель — каноник (по сути, помощник епископа) по фамилии Коперник.

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

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

В ответ на пост о религиозных спорах про форму Земли получил целый набор ответов типа «так у верующих же вера, а в науке речь только про доверие». При этом ни один человек так и не сумел пояснить, чем одно на практике у тех людей, о которых шла речь, отличается от другого.

Видимо, «вера» это когда ты доверяешь вердиктам кого-то типа Папы Римского. А «доверие» — когда кого-то типа авторов школьного учебника. Да, оба раза это, по сути, «ну, наверняка такой человек не стал бы врать или давать ошибочную информацию и не ошибся бы с выводами». И да, оба раза это, по сути, «я сам без понятия, как из данных получить выводы и как получить сами данные, но авторитетные люди наверняка разобрались». Но тонкая разница состоит в том, что верующим приятно думать, что их убеждённость в чём-то базируется на вере, поскольку такое в этой среде считается преимуществом, а их оппонентам, напротив, неприятно, поскольку в их среде это что-то типа зашквара.

И вот этим как раз и объясняется тезис: просто это слово нам не нравится, поэтому у нас совсем не то, что им называют.

Но реально, нет, про «доверие» в научном методе речь может идти только в одном контексте: «я доверяю вон той группе учёных, когда они показывают мне данные, в том смысле, что они эти данные не подделали сознательно и не наврали в описании способа получения этих данных». Никакого «доверия» выводам и рассуждениям в этом методе нет. Либо ты их можешь сделать сам (пусть даже с подсказками), либо… ну это самое… у тебя вера во мнение авторитета.

Интересно читать споры плоскоземельцев с людьми, которые типа знают, что Земля — шар.

Плоскоземельцы им говорят: «вы просто оболванены пропагандой и школой». А те им, такие: «не, мы просто знаем физику». Плоскоземельцы им, такие, «а вот же явление». А те им: «но оно объясняется физикой вот так». Плоскоземельцы им: «это вы просто не знаете физику». А те им: «нет, мы знаем — мы же дали объяснение».

Ну да, дали. И плоскоземельцы тоже дали. Тоже ссылаясь на «физику». У плоскоземельцев, конечно, её понимание неправильное. Но ирония в том, что и у их оппонентов оно в трёх четвертях случаев тоже неправильное.

В аргументации «а как же» — аналогично. Плоскоземельцы приводят некие, зачастую ошибочные, факты и ошибочные их объяснения. В качестве опровержения шароземельцы им приводят другие, зачастую ошибочные, факты с ошибочными объяснениями.

«Вон же на фотографии видно, что лучи от Солнца расходятся конусом, значит, Солнце где-то близко, а Земля — плоская!». «Это солнечный свет преломляется на краях туч, потому-то мы с Земли и наблюдаем, что лучи от солнца как бы расходятся в разные стороны, а потому Земля — шар».

«Но ведь есть закон сообщающихся сосудов! А на шаре он не выполняется!». «Ни фига, радуга имеет форму дуги! Как такое может быть не на шаре?».

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

Просто это верно не для всех шароземельцев, а лишь для изрядной их части. С другой стороны, в случае с плоскоземельцами такое верно практически для всех 100% личного состава, исключая небольшую долю тех, кто физику знает достаточно хорошо, чтобы понять, что Земля шарообразна, но всё равно делает выбор в пользу плоской Земли, поскольку так следует считать в его религии.

Однако занимательный факт состоит в том, что споры о плоской и шарообразной Земле, учитывая всё вышесказанное, это действительно в основном споры носителей одной религии с носителями другой религии.

Наверно уже сотый раз встречаю пересказ метафоры про «завод скрепок».

Если кто не знает, это про то, как опасен ИИ. Вот если перед ним, например, поставить задачу производить как можно больше скрепок, то он может решить, что ради этого надо всю Землю превратить в завод скрепок, а людей истребить, поскольку, ну, вдруг они мешают превращению Земли в завод скрепок.

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

Есть, правда, одна проблемка: ни при капитализме, ни при коммунизме нафиг не надо произвести как можно больше скрепок. При капитализме надо произвести скрепок столько, сколько принесёт больше всего прибыли, а при коммунизме — такое количество, которое в совокупности со всем прочим лучше всего удовлетворит потребности. Перепроизводство же приводит к снижению прибыли и к худшему совокупному удовлетворению потребностей. Уничтожение человечества, аналогично, приведёт к падению прибыли до нуля и нулевому удовлетворению потребностей.

Вдобавок ещё неясно, с какого рожна ИИ дают задачу, которую ни люди, ни другие ИИ, ни даже он сам вообще не могут поменять, но на фоне самой задачи — зашкаливающей степени идиотизма — этот вопрос кажется менее важным.

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

Ещё раз передаю пламенный привет всем ценителям теории «пузыря ИИ». За вчерашний день, благодаря «всего лишь T9» удалось сделать столько, сколько в иных условиях, возможно, не успел бы даже за месяц, ибо была непривычная мне тема, да ещё и на Python, который я хоть и отчасти знаю, но он мне тоже не особо привычен.

Кстати, какой гений сумел распиарить это как «простую и удобную среду для непрограммистов», я продолжаю недоумевать. Если бы не ИИ, я бы эту херню даже настроить бы не смог. Поскольку буквально каждый раз, когда я имел дело с Питоном, приходилось аки детектив выяснять, на какой версии чо сможет работать. И что надо установить вручную, поскольку автоматически оно не захотело. Как непрограммисты в этой простой и удобной среде справляются без ИИ, могу только гадать. Если сравнивать со Scala, это просто какой-то ад в плане настройки и подключения проектов. Благо, ИИ не только умеет писать код, но ещё умеет всю эту погребень диагностировать по выдаче и писать команды, которые шаг за шагом всё это чинят.

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