Комментарии 128
Она боится, что искусственный общий интеллект — или сверхразумный ИИ — попросту сотрёт человечество с лица Земли
Пусть почаще себе напоминает об этом, работая на низкоквалифицированной работе из-за брошенной учебы в МИТ.
Или она проживет последние годы жизни с толком, вместо траты на бесполезный диплом. Через пять-десять лет узнаем.
В смысле, пойдёт в сферу услуг определённого характера?
Даже онлифанс требует определенных... Вложений.
Почему вы подумали об этом первым делом?
Почему вы подумали об этом первым делом?
«А я всегда об этом думаю!» ©
Она не очень умна. Значит будет уборщицей или продавщицей. Сверхразумный ИИ, быстрее инопланетяне прилетят.
Кажется она просто не тестила супер расхваленный ChatGPT 5 😅 А надо было, так бы глядишь паничка прекратилась и вернулось спокойствие за будущее…
Возможно, именно после теста паника и началась)
Ну мне сложно в это поверить. Пиар был мощный перед релизом, но после релиза лично я не увидел ничего в этом апдейте особенного. У меня все более стойкое ощущение, что какого-то крупного прорыва в обозримом будущем не будет и ИИ будет еще долго оставаться просто удобным инструментом помогающим снизить рутину и быстрее находить информацию, но не станет пока убийцей каких-то профессий или же тем более AGI. А все эти громкие слова и обещания — ну что не сделаешь ради инвестиций…
У концепции AI уже было несколько итераций, и каждая упиралась в свой потолок:
I итерация ➠ 1950-е: перцептрон, сеть Хэбба, всякая теория
II итерация ➠ 1970-е (backprop), 1980-е (там куча простых архитектур типо Хопфилда, Кохонена, Больцмана, Хэмминга, всякие рекуррентные...)
III итерация ➠ Началась в те же 80-е (концепция Deep Learning), но конкретные архитектуры завезли позже (Convolution и LSTM в конце 90-х)
Дальше по сути современный этап развития (4-й?), который тоже шёл нелинейно:
стартовал ➠ начало 2010-х (первые базы ImageNet, использование GPU)
середина ➠ 2014-2016 (куча новых архитектур: GAN - генеративная, NTM - машина Тьюринга, Inception, Network-in-Network, ResNet и т.д.)
Настоящее время (финал?) ➠ Архитектура "Трансформер", Attention Network, CapsNet, адаптация доменов, GPT-3,4,5, OpenAI
И есть такое чувство, что всё. 4-й этап развития AI выдохся, из нынешних технологий выжали всё что можно - и надо ждать следующий крупный прорыв.
А прорыв - это не очередная 101-я архитектура нейронки и не увеличение количества GPU для вычислений. Это какой-то принципиально новый концепт
Мне почему-то нравится делать ставку на то, что в следующих итерациях уже будет участвовать верификация через Coq или Lean, то есть вот такая цепочка: человек формулирует задачу -> нейронка задает уточняющие вопросы, чтобы свести задачу к доказательству формальной теоремы, но при этом она не рассказывает какую выбрала математическую формализацию(потому что они обычно длинные и непонятные, долго понимать математические формализмы), если пользователь сам только не попросит -> поиск решения и проверка через язык формальной верификации (Coq или Lean) -> адаптация решения к максимально понятной и короткой для человека формулировке. Всякие верификации сильно повысили бы качество ответов, по крайней мере в науке бы пригодилось угадывать решения обучившись на уже известных ранее решённых задачах.
А как ваша ставка согласуется с тем что LLM это буквально воплощение китайской комнаты - она принципиально не способна понимать смысл текста. О какой верификации идет речь если нет понимания сути задачи?
Проверку решения задачи я всё ещё оставляю на совести пользователя нейронки, так что 100% правильной интерпретации сути задачи от LLM не требуется.
Прошу обратить внимание, что в жизни заказчики тоже иногда дают ТЗ сами не замечая, что их ТЗ недостаточно чётко и однозначно сформулировано(это в принципе тяжело сделать, люди часто опираются на контекст и опыт, часто индвидуальный, которого LLM может сильно не хватать, один из способов убирать проблему незнания контекста — обучение с подкреплением, у которого есть плюсы и минусы, я хочу предложить ещё один вариант через языки формальной верификации, позже ещё раз уточню как именно), тогда заказчик после проверки решения от разработчика может начать вносить правки, начиная новую итерацию уточнения решения, которое нужно заказчику, количество итераций наиболее зависит от толщины кошелька заказчика и терпения разработчика (есть ситуации, когда с нечётким ТЗ заказчика сразу посылают переделывать ТЗ, а не рискуют пробовать реализовать такой ТЗ в своём понимании).
Представим, что вместо (заказчик, разработчик, ТЗ) подставляется (пользователь, LLM, ТЗ), тогда [если убрать за скобки стоимость подписки на LLM и количество токенов, представив что токенов условно достаточно много] терпение LLM достаточно приятное, потому что можно общаться с ним сколько хочешь и он не обидится и не пошлёт подальше, перестав отвечать, но вот толщина кошелька заказчика — а именно его время, количество запросов, которые он готов поддерживать общение — уже довольно ограниченное, особенно, когда пользователь более опытный в том что спрашивает и понимает, что глюков у нейронки уж очень много получилось, проще и быстрее переделать самому с нуля, то есть цель в том числе уменьшить количество обмана и глюков, того, что в принципе не согласуется с изначальной задачей.
Я согласен, что LLM не понимают написанного, но их можно пробовать учить формализовать написаное, то есть сводить написанное к математическим формулировкам, а именно (частный случай) сводить к коду на языках Lean/Coq с доказательством(решением) к задаче пользователя. Особенность этих языков в том, что если код скомпилируется, то приведенное доказательство математически верное.
Какой у этого потенциал? Допустим, что пользователю нужно доказать, что из A следует B (из "Дано" следует "Доказать/Определённое значение таргета(возможно, что изначально неизвестное)"). Тогда пользователь старается объяснить что он хочет, а LLM старается понять что он хочет подобрать A, B и верифицированное доказательство A→B (под верификацией буквально имеется в виду, что LLM подбирает решение до тех пор, пока решение не скомпилируется при записи в Coq/Lean, проверка компиляцией является объективной величиной либо да, либо нет; поскольку мы всегда явно проверяем на выходе, что "да", то решение верифицировано), причём LLM старается задать уточняющие вопросы, если A,B слишком неоднозначные(много вариантов как интерпретировать запрос пользователя, недостаточно контекста), чтобы как можно точнее были A,B.
Задача LLM: подобрать A, B и доказательство A→B, спросить устраивают ли A, B пользователя(и формулировать A,B на человеческом языке + представить возможность посмотреть A,B как они записаны на языке Coq/Lean, чтобы человек мог проверить финальную версию что "Дано", а что "Доказать").
Настроенные ограничения на LLM(которые объективно проверяемы, то есть выполнены всегда, любой ответ от LLM должен быть таким, проверяется явным образом): её доказательство должно компилироваться в Coq/Lean, доказательство должно начинаться на A и заканчиваться B. То, что она заявляла ранее как формальная запись A,B должно фиксироваться до тех пор, пока нет запроса от пользователя поменять A,B.
Цель пользователя: отыскать красивое решение/доказательство.
Задача пользователя: сначала пообщаться с нейросетью, чтобы она как можно точнее сформулировала "Дано"(A) и "Доказать"(B), затем [опциально, но в случае строгости проверок необходимо] посмотреть формальные версии записи A и B, то есть как они выглядят в коде на Lean/Coq, затем проверить перевод на человеческий у доказательства (хотя и само формальное доказательство гарантированно верно и его можно посмотреть, нас же больше интересуют человеческие понятные нам формулировки — в теории LLM может ошибиться при переводе на человеческий, хотя бы потому что формальное доказательство может быть очень длинным, а LLM должна отвечать коротко). Когда A,B зафиксированы, то дальше можно через общение с нейросетью пробовать просить менять подходы к решению, пробовать сократить его и т.д. и т.п. (она может и сама пытаться, но мб с подсказкой ей будет сильно проще), всё равно любое его (по крайней мере формальное) доказательство будет верифицировано.
Таким образом любые данные всегда доступны в двух форматах "на словах(неформальная запись)" и "на деле(формальная запись)"(как оно гарантированно будет записано на языке Coq/Lean), всегда можно любые данные смотреть в формальном виде, но предлагается это делать только в крайнем случае(например, при сомнении в финальных данных). Общение с нейросетью происходит в два этапа:
Согласование ТЗ (подбор A и B сначала "на словах", а потом и в "итоговом договоре"(формальной записи), то есть формальные записи A и B фиксируются и никогда более не меняются, что гарантируется)
Оптимизация и проверка решений (на самом деле формальные решения можно не проверять, т.к. оно компилируется в Coq/Lean, и нам гарантируется, что A и B зафиксированы и являются соответственно началом и концом цепочки импликаций; но вот проверять как нейросеть пишет "на словах" решение всё же будет нужно как раз ровно потому, что Вы утверждаете и с чем я согласен — она не понимает, что пишет)
При желании ТЗ можно уточнить и поменять, но без ведома пользователя LLM запрещается это делать (то есть вне этапа 1 нельзя, но к этапу 1 можно возвращаться).
Итого цепочка:
Подбор человеческих формулировок A, B ---> [Проверка формальной записи A, B] ---> Подбор доказательства A→B ---> [Проверка человеческой записи A→B, формальная запись доказательства в верификации не нуждается, но доступна для просмотра].
Единственное где могут быть ошибки — в человеческих переводах формальных выражений с помощью LLM, остальное формальное на совести языков формальной верификации, раз уж формальное доказательство скомпилировалось на таком языке, значит оно и верно(с вероятностью 99.999...%, но не суть, язык формальной верификации ещё ни разу не был пойман на лжи, в отличие от LLM).
То есть LLM подбирает решения и верифицирует их через Coq/Lean, а также переводит их на человеческий язык; она не может ошибиться в решении, потому что любое решение верифицируется, но может ошибиться в человеческих переводах тех формальных выражений, которые используются(однако формальную запись мы всегда можем запросить явно и она будет без обмана). В принципе можно и без переводов обойтись, но тогда общаться не так удобно, я вот нечасто общаюсь на языке Coq/Lean; однако полагаю конкректно в науке найдутся люди, готовые общаться и на таком языке, тогда и переводы можно не проверять, а просто давать подсказки как сократить доказательство и потом копировать его в свою огромную библиотеку выверенных доказательств и утверждений, пополнив. Обучать такие LLM есть на чём, есть уже много библитотек, в которых много что доказано, можно вот пробовать через них и обучить + возможно поучить переводу туда-сюда (формально-неформально) через добровольцев.
И ещё кое-что важное про такой метод: нейросеть ведь по сути может генерировать промежуточные гипотезы, которые попроще доказать, и верифицировать их, тем самым отгадывая шаги и пошагово прийти к доказательству, а потом взглянув на получившееся решение попробовать убрать лишние переходы, тем самым сократив решение. Было бы чем-то похоже на человеческий подход.
Надеюсь понятно объяснил в чём идея.
<...> но вот толщина кошелька заказчика — а именно его время, количество запросов, которые он готов поддерживать общение — уже довольно ограниченное, особенно, когда пользователь более опытный <...>
Небольшая опечатка: здесь должно быть не "заказчика", а "пользователя".
Проверку решения задачи я всё ещё оставляю на совести пользователя нейронки, так что 100% правильной интерпретации сути задачи от LLM не требуется.
Понимаете, тут корневая проблема в необходимости верификации. Пошаговая формализация и верификация, а сверху еще и тесты по верификацированной логике - это конечно хорошо. НО! В массовом случае, условный калькулятор с огромной кодовой базой примеров верификация особо и не нужна. А в случае уникальной задачи без смысла задачи все сломается еще до верификации. Чтобы поэтапно уточнить нужно как говорится задавать правильные вопросы. А правильные вопросы без понимания сути задачи не задашь. Банально - сделай веб-страничку которая работает как поиск и находит нужную информацию. Что это - поисковик, сием, веб-морда для каталога файлов? Ок, пошло уточнение - предназначение системы. Ответ пользователя - это должна быть система сбора событий с разных источников с накоплением истории в локальную базу. Ок, LLM увидит в тексте локальную базу и что предложит - постгрю? Хадуп? Елк? А дальше что - уточнять нагрузку, структуру данных, частоту опроса? Прописывать все возможные наборы архитектур в рамках обучения? И откуда тогда LLM возьмет плейбуки таких опросов? А главное - в процессе разговоров окажется что пользователю не нужен новый продукт, его запрос полностью удовлетворит скажем Loki. Внимание вопрос - без понимания смысла запроса в конце цепочки уточнений LLM 1) начнет генерить новый код и верифицировать его по формальным метриками 2) Напишет "мил человек, тебе не нужен новый продукт, тебе нужно установить Loki, вот шаги, и настроить его - вот шаги." Вам не кажется что мир формата "у каждого пользователя интернета в мире свой набор софта который делает одно и то же но разный и написанный заново" это если и не антиутопия то близко к тому?
Так секундочку, если Loki есть в базе обучения нейросети с верификациями и он оптимален по заданным пользователем критериям, то нейросеть его и предложит(как один из вариантов), я не понял, почему Вы утверждаете, что она предложит новый код?
А опросники есть и в интернете. Да, есть вопрос в их качестве, но суть верификации, которая описана после первого абзаца моего предыдудщего ответа, в том, что чтобы проверять, что выполнено A→B, опираясь на те умения и знания, которые есть у нейронки. A — это начальные условия и ограничения, B — конечная цель. Хотите новый софт? Пишете про это в A. Хотите стандартное решение, уже есть конечные варианты, другие вот вообще не хотите рассматривать, тоже пишете это в A. Когда A, B зафиксируются, то для них ищется верифицированное решение A→B.
Небольшое отступление, хотя в другом моём комментарии уже написал очень подробно свои мысли, отдельно дублирую кратко ответ вопрос что такое верификация: если зафиксировать явно утверждения A, B на языке Coq/Lean и проверять решения, сгенерированные нейросетью для доказательства A→B (то есть проверять компилируется или нет код, начинающийся с A заканчивающийся B). Если сгенерируется, тогда импликация верна(таково устройство и суть языка формальной верификации), причём есть к ней доказательство верифицированное(об этой верификации и речь; нейросеть генерирует решения для фиксированных A, B, так что верифицировать A→B вполне можно: критерий — компилируемость), если нет, то неизвестно(можно паралелльно пробовать A→~B; если кстати вдруг окажутся оба доказаны: и A→B, и A→~B, то A изначально было невозможным, неверным, содержало противоречие).
Теперь возвращаясь к теме упомяну ещё раз, что подходы с верификацией описанные мною ранее в первую очередь ближе к науке, там проще формализовывать утверждения в математический вид (Coq/Lean основаны на теории типов, а это математика), вот когда там в науке активно начнут генерировать успешно доказательства, попутно с их верификацией, уже после этого может появиться смысл и прикладной, про который по сути и Ваш комментарий: например, люди начнут публиковать свои рекомандации в двух версиях — в неформальном блоге, и с небольшими формальными вставками на языке Coq в духе совсем простеньких глупеньких переходов: "ЕСЛИ (нагрузка в таком-то диапозоне) И (структуру данных (такая ИЛИ такая ИЛИ такая)) И (частота опроса в таком-то диапозоне), ТО (используй это или это)", причём такие блоки может составлять нейронка из обычных слов, чтобы не мучаться с синтаксисом, но бегло глазами проверять всё равно будет нужно + проверять через COQ что эти утверждения совместимы(непротиворечивы) [в рамках одной из своех библиотек; библиотек может быть несколько]; а могут и не из глупеньких, например: "import библиотека советов и технологий №150" или просто комбинация прошлых своих своих утверждений, при этом непротиворечивость всё ещё будет проверяться при импортах.
А как подобрать себе подходящий вариант? Берёшь N любимых библиотек советов и технологий или просишь у нейронки, знаешь, что они противоречат друг-другу, не хочешь разбираться вручную какие импорты будут конфликтовать друг с другом какие нет, отдаёшь нейронке задачу, чтобы она разбила их на кластеры непротиворечивых вариантов и просишь суммаризацию по разнице подходов, а так как нейронка наукой занималась[именно для этого я упомянул "сначала наука, потом прикладное" ранее], сложные задачи решала, то она ищет оптимальные в соответствии с твоими запросами и советами A и итогом который ты хочешь получить B, конечный результат ты даже можешь выгрузить в свой блог "библиотека советов и технологий №997" и тем самым либо присоединиться к какой-то из групп библиотек, с которой ты не противоречишь, либо писать свою библиотеку вообще с нуля, что крайне маловероятно, что кому-либо понадобится.
Итого: есть нейронки для переводов формальный-неформальный язык (нужно проверять результат-перевод, но это несложно, если договориться об обозначениях); а есть нейронки для верификации, которые в соответствии с твоими формализациями A и B ищет наиболее уместный подход среди тех библиотек, которые ты предпочитаешь, и(или) тех, которые есть у нейросети(но можно и исключить), доказывает выполнено A→B если верить библиотекам и даже показывает какие именно библиотеки используются.
То есть моё мнение, что в будущем люди научатся формализовывать свои утверждения благодаря нейросетям(ну если вдруг это кому-то будет интересно; а интересно может стать, если наука научит нейросети хорошо угадывать вывод формальные утверждения друг из друга), а затем цепочки из формализованных утверждений уже можно будет связывать друг с другом без проблем и быстро и при этом противоречий не будет, то есть LLM будут поменьше врать по крайней мере (они не будут писать "отсебятину" по поводу всего подряд, а только по поводу переводов на человеческий, потому что в цепочке " A -> форм А -> форм B -> B " средний переход проверяется строго математически, а вот переводы уже не такие строгие, как и доказательства, так и самих A,B). Работать это всё будет до тех пор, пока люди сами что-то тоже программируют, потому что на мой взгляд код чего бы то ни было ещё улучшать и улучшать, ничего абсолютно совершенного не существует, но лучшие известные практики через формализацию утверждений можно было бы находить(условно выбираешь кому верить из людей/компаний/библиотек и вместо чтения блогов или поиска утверждений в них, проверяешь, а не выводится ли из формальных версий этих блогов то, что тебе нужно, если нейросеть через дебри выводит, то это успех, и можно будет глянуть по каким местам интернета эта информация раскинута).
То есть непросто глубокое мышление (Reinforcement Learning) недавно предложенное, где нейросеть подольше пишет и сама свои ответы переваривает какое-то время, продолжая дальше бесконечно генерировать поток мыслей, а именно что верифицированный, логический подход (проверки на непротиворечивость на языке формальной верификации) во время "мышления".
Так секундочку, если Loki есть в базе обучения нейросети с верификациями и он оптимален по заданным пользователем критериям, то нейросеть его и предложит(как один из вариантов), я не понял, почему Вы утверждаете, что она предложит новый код?
С чего вы это взяли? Исходный запрос был - напиши мне то-то. Без понимания СМЫСЛА запроса LLM никогда до этого не дойдет - она будет генерировать свои токены в ответ на токены запроса. А то что смысл - удовлетворить потребность в каких-то функциях ПО - это вне задачи LLM - генерировать поток токенов.
А опросники есть и в интернете.
В случае уникальных решений - никаких опросников в интернете нет по определению. Создать поисковик из 10 избранных сайтов можно и на статической html странице. из 10 000 для пары пользователей - хранить в sqlite. Для всех сайтов в интернете - гугл разве открыл свои сорцы? А архитектуру? А распределенную базу данных с синхронизацией?
То есть непросто глубокое мышление (Reinforcement Learning) недавно предложенное, где нейросеть подольше пишет и сама свои ответы переваривает какое-то время, продолжая дальше бесконечно генерировать поток мыслей,
Смотрим на переваривание, точнее на зависимость точноcти от контекстного окна. Да, перегонять бесконечно это отличная идея, гениальная!
С чего вы это взяли? Исходный запрос был - напиши мне то-то. Без понимания СМЫСЛА запроса LLM никогда до этого не дойдет - она будет генерировать свои токены в ответ на токены запроса. А то что смысл - удовлетворить потребность в каких-то функциях ПО - это вне задачи LLM - генерировать поток токенов.
В третий раз упоминаю: ЧЕЛОВЕК должен проверять формальный вариант записи "Дано" и "Доказать" на языке Coq/Lean, не LLM (Вы должны уже обратить внимание, что я использую концепцию: любые данные в двух видах, первый вид неформальный, второй вид формальный -- буквально код на языке Coq/Lean), и только если они его устраивают, только тогда LLM переходит к этапу "Угадывания доказательства", причём решение верифицируется через Coq/Lean, оно не может быть "неверным", оно может либо найтись(и тогда оно верное), либо не найтись и тогда просто считайте, что LLM всегда отвечает в этом случае "я не смогла решить эту задачу". СМЫСЛ будет ровно тот, на который ВЫ сами и согласитесь, когда САМИ ПРОВЕРИТЕ формальные версии "Дано" и "Доказать", тогда гарантируется, что формальная версия доказательства доказывает ровно то, что требовалось, при тех ограничениях, которые были заданы. Считается, что любое решение вас удовлетворяет, покуда вас устраивает "Дано" и "Доказать" и выбранные вами библиотеки-математические-теории, но вы можете потом сами поменять "Дано" или "Доказать", накинув дополнительных ограничений.
В случае уникальных решений - никаких опросников в интернете нет по определению. Создать поисковик из 10 избранных сайтов можно и на статической html странице. из 10 000 для пары пользователей - хранить в sqlite. Для всех сайтов в интернете - гугл разве открыл свои сорцы? А архитектуру? А распределенную базу данных с синхронизацией?
А кто сейчас хранит всё? Какой смысл индексировать всякий мусор? Если вы спрашиваете про то, как же найти это самое уникальное решение через мой вариант LLM+верификация, то вот ответ: задать формальные "Дано" и "Доказать", получить верифицированное решение и воспользоваться им, возможно, что верифицированного решения не найдётся, ну, так бывает, значит на малых данных нейронка училась доказательствам, не научилась пока доказывать особенные случаи. Если же задача хоть сколько-нибудь стандартная, пусть в ней и немного новые параметры, которые ранее никто не применял, то цепочку рассуждений нейронка справится построить, если вы в "Дано" пропихнёте максимально подробную информацию (именно что в формальном виде) про эти параметры, то чего уж ей сложного будет проверить насколько согласованы остальные данные с тем что вы затребовали в "Дано", и с тем что желаете получить на выходе "Доказать".
Смотрим на переваривание, точнее на зависимость точноcти от контекстного окна. Да, перегонять бесконечно это отличная идея, гениальная!
Это как-то несерьёзно — не увидеть, что я использовал предложение вида "Не ... , а ... " (формально там было: "То есть непросто ..., а именно что ..."), то есть противопоставление, естественно, что всё стоит между "Не" и ", а" я согласен, что не очень (иначе зачем бы я стал использовать противительный союз "а") и его как-то нужно дорабатывать(или убрать, если вы это хотели сказать, то ок, мне без разницы, можно и убрать; просто вроде как Deepseek R1 именно за счёт небольшого окна с RL повысил точность, но даже если и не так, всё равно суть не в этом, уж прошу прощения, что привёл пример, когда его можно было бы избежать, учитывая, что основная моя идея с RL-то и не связана), так что незачем было пояснять.
И да, пока что нейросети не очень справляются генерировать доказательства даже для простых задачек из науки, например, на момент 23 мая 2024 года DeepSeek-Prover справился верно доказать всего лишь 5 из 148 международных задач по математике, а GPT-4 вообще ни одну не смог доказать, заметьте, это было соревнования пруф ассистентов на языке Lean, то есть их нагенериный код запускался и автоматически проверялся(если компилируется на Lean, значит доказательство математически верно), так что пока рано объективно оценивать насколько жизнеспособна идея генерировать доказательства нейронками, но на мой взгляд жизнеспособна.
Вот искреннее не понимаю, что непонятного в том, что я говорю что СМЫСЛ заключён в "Дано" и "Доказать" записанных в формальном виде(на Coq/Lean), ВЫ САМИ вот буквально пишете тот смысл, который вам нужен, а нейронка просто генерит верифицированные решения (если строго и формально: нейронка генерирует ответы до тех пор, пока ответ не скомпилируются на Lean/Coq, когда ответ скомпилировался, вот тогда он верифицирован и только тогда он выводится пользователю, пользователь может быть уверен, что цепочка логических рассуждений от "Дано" к "Доказать" строго математически доказана; чтоб не слишком долго ждать можно задать таймаут нейронке, тогда она может и не успеть сгенерировать доказательство).
Вы всегда подменяете вопрос? Я не спрашивал про верификацию, я спросил откуда вы взяли что LLM на запрос написать код может ответить "этот существующий код уже выполняет ваши задачи". Ответьте пожалуйста на МОЙ вопрос, а не на свой.
Ответ: если в "библиотеке советов и технологий №K"(этой сущности я давал определение выше, кратко: набор формальных утверждений непротиворечащих друг другу) есть уже ссылка на готовый код, удовлетворяющий вашим требованиям, то нейронка приведёт ссылку на него, потому что доказательство будет состоять из одного шага(просто взять решение из библиотеки).
Подробнее: Ваши требования формально записаны и решение из библиотеки уже удовлетворяет тем же требованиям(которые тоже записаны формально), нейронка вполне себе с большой вероятностью сможет угадать решение из одного шага, вы даже можете указать это как часть Ваших требований (чтобы решение состояло из одного шага, если это возможно).
нейронка задает уточняющие вопросы
адаптация решения к максимально понятной формулировке
То что вы пишете, это по сути Reinforcement Learning, либо, быть может Active Learning. В целом соглашусь, что за reinforcement - будущее. Но вряд ли прямо в его нынешнем виде. Но это явно лучше чем втупую гонять петабайты данных по каноничному data-driven подходу, так он вроде называется
Ещё один подход - гармоничное сочетание "базы знаний" (концепция из 70-х, 80-х) сформированной человеком, т.е. с готовыми алгоритмами. И дообучение модели ИИ уже с использованием больших данных. Сейчас подход с базой знаний отвергается в принципе - типо компы умнее и сами всё посчитают. Ну хз хз
Думаю при разумном подходе сочетание "человеческих" алгоритмов и data-driven подхода, т.е. каноничного обучения нейросетки - способно ускорить это самое обучение на порядки. А может, даже избавиться от некоторой части тупейших ошибок ИИ, связанных с недо/переобучением.
Reinforcement Learning
Active Learning
сочетание "человеческих" алгоритмов и data-driven подхода
Но есть один нюанс. Вот это ↑ проще сказать, чем сделать...
Это на этапе подбора A и B (вообще говоря этот этап даже и не нужен, если сразу сформулировать их на языке Coq/Lean) и приведения решения к человеческому виду, я же предлагаю именно что добавить верифицируемость для доказательства A→B, хочу чтобы нейронка генерила код на Coq/Lean для строго математического доказательства и его же и выдавала, она не сможет ошибаться по определению(каждое доказательство проверяется через Coq/Lean), но может в принципе не смочь придумать доказательство.
для строго математического доказательства
В математике есть такая штука, как недоказуемость некоторых истинных утверждений. Вообще там всё сложно - условно можно "построить" некую теорию N+1 порядка, чтобы доказать все истинные утверждения теории N-го порядка. Но в свою очередь, у теории N+1 порядка, будут свои недоказуемые утверждения - замкнутый круг.
Ещё хороший вопрос, осилит ли нейронка построение теории N+1 порядка, при условии что теория N-го порядка ей уже известна. Это как бы даже для человека сложно формализуемо
Например
Попробуйте из арифметики/алгебры вывести анализ добавлением "чужеродного" для алгебры понятия непрерывностей и пределов
хочу чтобы нейронка генерила код на Coq/Lean
так что в теории может и да, а на практике - надо смотреть
Кстати, не стоит думать, что теоремы Гёделя - это сложно, заумно и не от мира сего. Мол в реальной задачке для нейронки этот случай никогда не встретится. Ничего подобного! Вот далеко не самый сложный пример, уравнение как уравнение. Да, много переменных - но в остальном ведь ничего особенного
А прорыв - это не очередная 101-я архитектура нейронки и не увеличение количества GPU для вычислений. Это какой-то принципиально новый концепт
... и этот концепт можно "открыть" с помощью нейронки. Время от времени нейронки помогают с решением "труднорешаемых" задач. Так что интуитивно дальнейшая эволюция вполне возможна.
Эпичнее было бы если она сказала это на экзамене, отказавшись отвечать на билет, а лишь потом ушла)
Самая ленивая отмазка на свете
Подобные заявления были при каждом технологическом скачке. И каждый раз мир продолжал крутиться
Помнится, ещё Грета Тумберг школу отказывалась ходить из-за глобального потепления. Главное найти вескую причину своей лени и никчёмности.
Ядерная война, пришествие инопланетных захватчиков, комета, пандемия смертельного вируса. Теперь еще AGI добавился.
"Уважаемый редактор, может лучше - про реактор?". Не, про реактор после Чернобыля и Фукусимы тоже страшно. И лунный трактор не успокаивает. Только антидепрессанты.
Сейчас Блэр работает техническим писателем
Т.е. я правильно понимаю, что в качестве меры борьбы с вытеснением её профессии AGI она ушла в профессию, которую гипотетический AGI уничтожит ещё раньше? :)))
Побоялись безработицы в ИТ
Ну, если у неё есть запасной вариант - вперёд!
Помнится, Вассерман топил за то, что вычислительных мощностей уже хватает для решения задачи линейного программирования для оптимизации всей экономики. Дескать, во времена Канторовича компьютеров не хватало, и абсолютная плановая экономика была невозможна, но вот сейчас... Возражая Вассерману: плановая экономика имеет некие преимущества, но лишь до тех пор, пока не произойдет что-то непредвиденное, например, как Фукусима в Японии. Япония вообще почище СССР все планирует, но тут одно цунами смывает пару малых бизнесов, и выясняется, что на их продукции стоял весь остальной бизнес страны...
Так вот по поводу излишнего энтузиазма от AI: он обучен на имеющихся данных, и в модель не заложено их изменение. А ситуация будет меняться, и человеческий мозг более приспособлен к нахождению выхода в незнаком и неизведанном. Сила в симбиозе обоих разумов, и один другого не будет уничтожать. В отличие от естественной человеческой глупости, которую упомянутая в статье студентка как раз и продемонстрировала.
Все больше убеждаюсь в том, что Вассерман это говорящий винчестер емкостью в 1 Пб, но не более того ) Да простят меня фанаты упячки
Я считаю, что как раз таки плановая экономика на основе IT гораздо лучше любых альтернатив справится с явлением полярной лисы. Министерства учёта чётко знают, где лежат запасы всего что можно в голову вообразить, от продовольствия и йода до костюмов розовых зайчиков, и могут чётко организовать экстренную доставку всего что надо. Тогда как рыночная экономика побуждает всех не допускать никаких запасов, кроме тех, которые вменены по закону, и от этого обременения все норовят художественно избавиться.
Тогда как рыночная экономика побуждает всех не допускать никаких запасов.
Ключевое слово "всех". В плановой экономике есть одна сущность, которая все планирует, и любой сбой приводит к катастрофе. В рыночной экономике таких сущностей много, и сбой на уровне одного агента компенсируется наличием остальных. Плюс я не вполне согласен с вашим утверждением о том, что все агенты такие бестолковые, что подставляют брюхо неизвестности. Они все, как минимум, разные, и кто-то предвидит необходимость запасов, кто-то скальпирует любую копейку. Но сама идея не хранить все яйца в одной корзине реализуется объективным обилием агентов с минимум одной корзиной у каждого.
Борьба с запасами - мировой тренд. Когда-то Just in Time было японским трендом, а спустя много лет, в другой стране, если ты делаешь гос или муниципальные закупки на склад выше текущих потребностей, то тебе потом придется объяснятся с контролирующими органами.
Ну и что, что нет никакого маневрового фонда, зато запасы деньги не гниют на складе.
Насколько мне известно, советскую плановую экономику не сгубил никакой единичный сбой, а сгубила лживая отчётность на всех уровнях. Как в анекдоте: свинья принесла поросёнка - в отчёте написали, что родилось два поросёнка - обком пишет о рождении трех поросят - Брежневу докладывают о двенадцати поросятах.
Почему это работало? Да потому что не было возможности сверить все отчёты. Госплан тонул в бумажках. А с цифровизацией учёт становится проще. Если завод пишет, что отправил на базу 1000 деталей, а база пишет, что пришло 900 деталей - то нужно сделать проверку. По итогам проверки выяснится, что сделали только 950 деталей, отправили, а ещё 50 украли на базе. Всем штрафы и уголовные дела, все наказаны.
К тому же с цифровизацией проще рассчитать потребности населения и сколько товара наличествует и куда его лучше направлять.
Конечно, у плановой экономики есть и другие недостатки, но я перечислил те, которые цифровизацией решаются.
Госплан тонул в бумажках.
Более того, бумажки передвигались со скоростью голубиной почты.
Брежневу докладывают о двенадцати поросятах.
Почему это работало? Да потому что не было возможности сверить все отчёты.
Дебильный анекдот. У вас не возникал вопрос, где деньги за эти 11 приписанных поросят? Мясо шло на мясокомбинаты, в торговлю и общепит, а там оно монетезировалось. Так вот я вам скажу, как очевидец тех времен, что тогда было принято скорее "потерять" это мясо, чем приписать в отчетах. Потом это "левое" мясо шло в торговую сеть и продавалось мимо кассы, мой родственник за это сидел при дедушке Хрущеве. ))
Я не знаю подробностей, как им удавалось мухлевать с кассой, но схема была довольно простой, в продмаг прямо с мясокомбината привозили несколько тонн мяса, а потом забирали нал, что-то с этого нала перепадало завмагу и остальным соучастникам. Видимо и на мясокомбинат это мясо точно так же привозили с каких-то совхозов, где родили и выкормили 12 поросят, а по отчетам прошел 1 и тот сдох.
Ну собственно это и погубило совок, никто не хотел работать за госзарплату и стоять очереди за всем.
Ну собственно это и погубило совок, никто не хотел работать за госзарплату и стоять очереди за всем.
Ну то есть самая что ни на есть незамутнённая трагедия общин.
Это скорее трагедия незамутненных интеллектом ящеров в руководстве страны, которые сами живут в роскоши, а другим предлагают пайку как заключенным.
Прискорбно и то, что сейчас народ готов опять наступить на эти же грабли, хотя даже умереть было бы лучше, чем вернуться в совок.
«Я заметил, что по какому‑то странному стечению обстоятельств те, кто жил в совке, жили намного хуже тех, кто жил в СССР.» ©
Скажите, а в какой стране средний заключённый в своей пайке съедает 67 кг мяса в год, из них 32 - говядины (а в современной свободной и суверенной России - всего 13 кг говядины)? Или это лично Брежнев с Политбюро статистику выравнивали, съедая лишние миллионы тонн мяса, пока население в 1982 вымирало от голода?
По поводу поросят: не знаю, как насчёт мяса. Вдруг про мясо анекдот и врет. Но с хлопком была именно такая ситуация, как в анекдоте)
Хотя, конечно, самому колхозу было бы выгоднее перевыполнить план в 3,8 раза, а "потеряют" его на этапе распределения и доставки.
По поводу роскоши, в которой жила верхушка номенклатуры: вы действительно считаете, что роскошь - это ездить на Волге, кушать больше мяса и иметь доступ к консервированным ананасам? Серьёзно? СССР потому и развалили, что карьеристам партийным надоело жить на уровне среднего класса - душе карьериста всегда хочется Роллс-Ройса, яхт и золотых унитазов. А советский строй им такого дать не мог.
съедает 67 кг мяса в год
Советские люди настолько много ели мяса, что пришлось придумать целую Продовольственную программу придумать, чтобы заставить их есть ещё больше мяса
Советские люди настолько много ели мяса, что пришлось придумать целую Продовольственную программу придумать, чтобы заставить их есть ещё больше мяса
Ну да, а вовсе не потому, что стало больше людей. /s
в какой стране средний заключённый в своей пайке съедает 67 кг мяса в год
Это 180г в сутки, вы не верите в то, что во множестве стран мира заключенные могут съесть за день котлету и тарелку супа с мясом?
Я в душе не понимаю, кто все это мясо съедал в совке, на полках магазинов, особенно в глубинке, можно было лишь кости купить. Если не покупать на рынке и не иметь блата, то мясо можно было поесть лишь в общепите, где в котлету натолкают хлеба.
вы действительно считаете, что роскошь - это ездить на Волге, кушать больше мяса и иметь доступ к консервированным ананасам?
Большинству из них эта Волга нафиг не нужна была, при совке у каждого руководящего работника, не считая совсем мелких организаций, был личный служебный транспорт, который использовался не только в рабочих целях. Барина привозили к 9 утра на работу, а после 11 его уже хрен найдешь до конца рабочего дня. Они в принципе не работали, за них все делали замы.
Доступ у них был ко всему, о чем обычный человек даже мечтать не мог. Хоть дефицитные импортные лекарства достать, хоть квартиру получить вне очереди. Коррупция и воровство тоже присутствовали. Простые смертные жили в совсем другом мире, на подключение телефона десятками лет в очереди стояли. Попробуйте включить мозг и примерить это на своей шкуре, может тогда перестанете восхвалять совок.
Читайте внимательно: я высказывался не о вреде плановой экономики, а о вреде Анатолия Вассермана. Такое же отношение у меня и к AI: нас погубит не сам искусственный интеллект, а идиоты, за него топящие.
Насколько мне известно, советскую плановую экономику сгубила полностью сбитая система мотивации. Зачем стараться делать качественный товар, если от того, как он продастся ни для конечных исполнителей, ни для их руководителей ничего не зависит?
Министерства учёта чётко знают, где лежат запасы всего что можно в голову вообразить
В том числе и надувных полярных лис.
Плановая экономика не могла бы адаптироваться в условиях чрезвычайно изменчивых современных потребностей. Я не думаю, что будь все средств производства под контролем правительства люди смогли бы накупить миллион Лабубу
но тут одно цунами смывает пару малых бизнесов, и выясняется, что на их продукции стоял весь остальной бизнес страны...
Может быть они просто забыли это посчитать? Не учли риски и так далее? Или просто сэкономили и понадеялись на "авось"? (авось не случится цунами).
Выше я говорил именно о задаче линейного программирования, решение которой Вассерман проподавал как панацею. Учет рисков в модель линейного программирования не входит.
Приведите пример постановки задачи линейного программирования, в которую заранее заложены риски. Тогда я, может, с вами и соглашусь.
Начну с третьей статьи. Там в модель закладываются страховые выплаты. То есть, используя метафору Фукусимы, в случае уничтожения цунами мелкого поставщика колес, на котором базируются крупные производители, мы будем вместо шин наматывать деньги. Основной проблемы не решает.
Первая статья рассматривает риск как действие агрессивного игрока, расчитывающего нанести максимальный урон. В итоге решение становится более "толстокожим" (и менее привлекательным для оптимистичного случая), вместе с тем оно все равно представляет собой статическое решение, которое ломается в случае возникновения форс-мажора. Приблизительно то же самое получается и во второй статье, где вводятся "альтернативные ограничения", а потом выбираются наиболее удобные с точки зрения целевой функции. В этой же статье автор вооружается генетическими алгоритмами и, цитирую: "доказывает некоторые результаты с помощью модели нейронной сети..." При этом в аннотации все равно делается акцент на сведении этой задачи к задаче линейно-булевого программирования.
Я, конечно, по диагонали читал, меня можно подловить на непонимании и коверканье деталей. Тем не менее, в задаче линейного программирования и ее разновидностей есть фундаментальная проблема: они дают некое решение, которое хорошо работает только в условиях ограничений той модели, как ее задали в постановке. Эти модели всячески борятся с избыточностью. Они не берут в расчет изменчивость потребительского спроса. Например, если модель решит, что выгоднее и безопаснее с точки зрения потенциальных рисков производить седаны баклажанового цвета, то вам не представится возможность захотеть белый хетчбек по причине его отсутствия в ассортименте.
Решения, которые предлагает рыночная экономика, априори вводят избыточность, конкуренцию и адаптацию к изменчивости. Тот самый "генетический алгоритм", где ценой устранения менее приспособленного к случившемуся непредсказанному риску выживает кто-то более приспособленный.
Тем не менее я не хочу продолжать дальше эту дискуссию, и просто соглашусь, что какие-то риски в задачу линейного программирования ввести можно.
Это идиотия какая‑то. Как можно делать утверждения о достаточности вычислительных мощностей, не имея готовых, проверенных математических моделей, проверенного и отлаженного софта, который будет это всё считать, решать и оптимизировать, проверенных и отлаженных систем сбора исходных данных, и т. д., и т. п.? А всего этого нет по определению, на уровне постановки задачи. Это не говоря уже о самом главном: ну, допустим, всё вышеописанное (включая вычислительные мощности) даже есть — и чо?
Одна баптистка (из "свидетелей") рассказывала, что теперь, когда она уверовала, она покупает только маленькие тюбики зубной пасты: зачем тратить деньги на большие, когда конец света вот-вот наступит?
А зачем тогда деньги вообще?
А зачем тогда зубы вообще?
Где-то в Писаниях есть, что если мужчине отрезать яйца, то его не пустят в Царствие Небесное. Может, и про зубы есть чо.
Про яйца не помню - но в Евангелиях есть про руку, ногу или глаз, "если соблазняют тебя, отсеки и выкинь вон". Зубы в те времена разваливались без какой-либо стоматологии, и могли даже считаться расходным материалом, поэтому потеря зубов была частым явлением и не должна была быть поводом для чего-то серьезного.
отсеки и выкинь вон
Аллегория внезапно стала подтверждением небывалых успехов в античной хирургии.
Нашёл, "Второзаконие", глава 23, пункт 1:
У кого раздавлены ятра или отрезан детородный член, тот не может войти в общество Господне.
Хотя есть в Библии пассажи и прямо противоположные или могущие быть истолкованы как таковые, секта скопцов не даст соврать.
баптистка (из "свидетелей")
Это же разные конфессии?
Мне, технарю, вообще переживать по этому поводу смысла нет. Работы всегда навалом было. Но лучше вообще не работать, а жить в свое удовольствие, развиваться творчески, духовно и физически. Только вот много людей может себе это позволить?
А мне рабачить нравится. Мозг полностью выключен, сливаешься со спиннингом, пытаешься прочувствовать, какая проводка воблера для рыбы наиболее интересна... Приезжаешь домой, а тебе новых задач навешали, снова включаешь мозг, такие качели - каааайф... какой тут ИИ?
да ерунда это ваше саморазвитие. Ну уволился я однажды, чтобы пожить в удовольствие. Начал книжки читать, зарядку делать, развиваться так сказать. Заработал депрессию. В итоге оказалось, что нужна социализация и востребованность в обществе. Вернулся на работу. Дурацкая эволюция мозга, порицающая сычевание, будь ты проклята!
не, просто нужен баланс. Всему свое время - для работы и для отдыха, для социума и для одиночества. Думаю, идеально будет где-то 3 часа работы в день, если ии заменит остальное.
Уволили меня однажды, начал жить в своё удовольствие. Депрессии не заработал, социализация ваша мне и на хрен не нужна, с отсутствием востребованности в обществе жить вполне можно. Единственная проблема — что когда свободного времени слишком много — а его много, оно теперь всё свободное — его перестаёшь не то что ценить, а вообще ощущать. Ну и что деньги потихоньку заканчивались. Если бы не эти две проблемы испанской инквизиции (особенно вторая), готов был бы так жить хоть вечно.
Слабак
Не знаю что там будет с AGI и когда, но вот свой тест естественного интеллекта студентка уже провалила бросив обучение в одном из крутейших ВУЗов планеты.
Так это - наоборот, стимул учиться, чтобы создать противовес против ИИ. Используя тот же ИИ. Не уничтожить, а нащупать баланс. Собрать команду борцов и бустануть прогресс в эту сторону.
Это как раз может быть востребованным в будущем.
Тем, кто плотно не работает с нейросетями может показаться, что они могу захватить мир
Угу. Сегодня я попросил у дороогого и хвалёного гпт5 исправить шейдер для хоббийного 3д проекта...
Хорошо что есть версионность и откат не проблема
Сколько раз ты попросил? После первой неудачи ты отправил ему правки, хотя бы одну? Насколько хорошо ты поставил задачу?
Ты правда думаешь, что средний профессионал справился бы с этим лучше, чем GPT-5?
Лично я уверен, что ты один раз попробовал, он с первого раза не справился, и ты использовал это, чтоб успокоиться
Я использую в роботе по корпоративный подписке 4.1 и 4о. Я умею ставить задачу и попыток было много. Реальность такова что на не супер популярном фреймворке не 4 не 5 версия не справилась. Возможно проблема в том что модель не может оценить визуальные изменения. В данном конкретном случае я уверен что человек справиться лучше.
З.Ы. я не против ллм и они хороши как инструмент но далеко не всесильны и не AGI
Горадо хуже то, что некоторым особо одарённым персонажам может показаться, что она может позволить победить в большой войне.
«Учёные раскрыли секрет загадочной улыбки Моны Лизы: вероятно, она была просто дурой.»
Какая потрясающая и нелепая отмазка. Помимо нейросетей (которые я слегка пробовал и очень сильно разочаровался) есть вещи поопаснее и поактуальнее, события последних трёх (как минимум) лет вроде бы чётко это демонстрируют.
Я вот тоже думаю, бросить всё (работу) и начать жёстко бухать (на пару лет денег хватит). Но. А вдруг конец света не наступит в ближайшем (обозримом) будущем? В таком случае я как раз-таки и про?бу впустую кучу времени, денег и здоровья.
Впрочем, есть некоторый контингент (маргиналы), который придерживается
позиции:
День прошёл,
И в рот ?бать,
Завтра будет день опять.
"Слегка попробовать" недостаточно. Я не говорю, что нужно бежать за гречкой и туалетной бумагой. Но лично мне очевидно, что большинству специалистов скоро придет конец
скоро придет конец
А как скоро?
Через год-два — это скоро, только вероятность какова?
Через 30-40 лет — не стоит заморачиваться. Как минимум тем, кому не 20-30 лет.
В комментарии выше я намекнул на некоторые другие события, а вот они меня беспокоят куда больше всяких ИИ, которые по факту (на данный момент) собственно ИИ не являются (сами не умеют думать).
лично мне очевидно, что большинству специалистов скоро придет конец
Вы кавычки вокруг «специалистов» забыли.
Это вы так цитируете известную армейскую (я с ней в армии столкнулся) речевку?
Я слышал в такой версии (осторожно, обсценная лексика)
Скрытый текст
– Вот и снова день прошел!
– ДА И НАХУЙ ОН ПОШЕЛ!
– Завтра будет день опять!
– ДА И В РОТ ЕГО ЕБАТЬ!
Кажется, она несколько точнее.
Да, она самая.
Насколько я понимаю, это про то, что ты ничего не можешь (не хочешь, если не применять к армии) изменить, поэтому можно не париться.
Фатализм?
Предпочитаю планировать всё, что только возможно, хоть и не всегда получается. А ежели совершенно не думать о будущем, то зачем тогда работать\учиться? Однако большинство всё же не бросают работу\учёбу. Насколько мне известно.
Слишком много хайпа в последнее время вокруг ИИ и того что он оставит многих без работы. Кто-то видимо очень хорошо зарабатывает на этом хайпе. Больше походит на кликбейт
А ты считаешь иначе? Тенденция вроде очевидная: ИИ развивается, а люди нет. Даже с чипами в голове люди не имеют шансов против нейронок
ну вот можно было бы и начать учиться и изучать тему, чтобы найти противодействие, какой-то баланс. Создать ии против ии. Всегда на систему появлялась своя контр-система - это и есть развитие. Сложно, но тем и интересно.
Но нет, надо паниковать и сдаваться. Хотя да, именно сейчас в этом и вред от недо-ии - он демотивирует и наводит панику. Если щас художники, музыканты просто бросят учиться, то деградация, действительно, неизбежна, и вот так может быть победа над человечеством даже от недо-ии.
"Не имеют шансов"??? О чём вы вообще? Нейросети без осознания "субъективного я" и категорически не умеющие в формальную логику и мета-мышление, вдруг повсюду заменят человеческий интеллект?
Хотя... Тех кто всерьёз переживает на этот счёт - может и заменят ;)
Странно конечно видеть обсуждения насколько тот же чатGPT совершенен. Ведь уже сейчас понятно что он в разы адекватнее и логически последовательнее чем 95 из 100 типичных докторов наук, из которых еще с десяток дебиловатых будет.
Но есть нюанс.
Зачем вы сюда логику приплетаете? Не умеют нейросети в логику!
Затем. Что нейросети прекрасно понимают логику и контекст. И бреда без аргументов в отличии homosapiensa не напишут ,если конечно это блоком в программе не будет.
Вы, простите, с Луны свалились? Я могу практически любой ответ нейросети перевернуть на 180 и "доказать" обратное - и она со мной согласится.
А уж сколько бреда они генерируют... Ну вот, прямо сейчас проверил (gpt5):
Я вам подобного могу накидать столько... Страшно станет вообще ими пользоваться))
Скрытый текст
Так он все правильно в начале объяснил. Откройте википедию и посмотрите что люди дали определение простому числу: это то которое делится само на себя и на 1. Число 4 уже не является простым потому что имеет три делителя 1, 2 и 4.
А потом попробовал доказательство что оно простое. У кого то на доказательство что число Грэма простое уйдут годы и целые научные работы.
Как обычно вся проблема в формулировании и формировании информации людьми.
Вы не нервничайте, а доказывайте что число Грэма это простое по вашему простому мнению число. У вас на это целая жизнь. Может вполне оказаться что оно не простое и делится еще на какое то число кроме себя и единицы.
Знаете в чём проблема в диалоге с вами? - Вы ведь даже не осознаете суть написанного!
Вот какие процессы в ваших "чертогах разума" привели к выводу, что я считаю число Грэма простым??? Всё ровно наоборот - это комбинаторика, там вся суть в перемножении вариантов. И этот мой вопрос к нейросетям является как раз элементарным маркером полноценного логического мышления - несмотря на всю его невообразимую величину, нет никакой нужды перебирать варианты. Это просто огромная степень числа 3, а значит по своему определению оно обязано(!) делиться на 3. Я правда не понимаю, зачем я по второму разу это расписываю... Т.е. число Грэма составное - по своему определению! Вот и всё доказательство. А нейросети с ходу не видят этой очевидности и упираются в масштабы числа... Плюс периодически выдают какую-то дичь типа "оканчивается на 7, значит на 3 не делится"... И вот после таких пассажей вы всерьёз собираетесь их использовать хотя бы для проверки школьных заданий по математике??? И это я ещё даже геометрию не трогал - там вообще вилы (они абсолютно не умеют в образное мышление)...
Кгхм, число Грэма не простое, так как имеет форму 3^n, где n примерно равно "овердофига", но при этом целое.
Студентка MIT бросила учёбу, заявив, что AGI уничтожит человечество раньше, чем она получит диплом