Что такое заведомо мусор и/или ложные данные в Вашем исходном комментарии? Что значит "заведомо"? При каких обстоятельствах Вы считаете необходимым заводить уголовное дело, а при каких нет?
Буквально новость о том что не так, в другом мессенджере мне почему-то не нужно разрешение от высших мира сего, чтобы запустить своего бота, довольно удобно в другом их создавать, тестировать и выпускать прямо на платформе.
Если зафиксировать часы созвона общие для всех, то это ничем не отличается от общей для всех очной встречи, при условии дисциплинированности удалённых работников и заранее установленных рамок коммуникаций.
Если же офис предпочтительнее, только потому что можно без договоренности отвлечь сразу N сотрудников, потому что до них легко очно дойти, то не факт, что это лучше в плане организации — ведь их по итогу отвлекают во время работы в несогласовонное время, это может сбивать рабочий темп, тогда нужны сотрудники, которые могут работать очно и легко переключаться между задачами при условии, что их в любой момент видимо могут выдернуть из процесса работы, раз нет заранее согласования когда общая встреча(иначе непонятно чем удалёнка хуже, когда всё согласованно заранее).
Лично мне в таком режиме работать сложнее(когда меня могут отвлекать в произвольное время), чем в режиме с зафиксированными по времени (пусть даже ежедневными) встречами.
Исходники клиентского приложения у телеграм открытые, сквозное шифрование можно по ним и почитать и проверить как работает, а ещё исходники можно собрать и пользоваться собранным приложением, вместо скачанного откуда бы ни было готового файла, внутри которого непонятно что.
Неповторяющиеся ключи доступа к тем или иным ресурсам? В теории бывают и одинаковые в рамках одной компании/ одного человека, когда несколько репозиториев обращаются к одному и тому же ресурсу.
Не понимаю почему не жизнеспособная, согласно посту они выложили вообще всё: и веса модели, и процесс обучения, и подробности. Хотя бы в образовательном национальном плане это звучит полезно — люди могут наглядно учиться, делать лучше при желании, тоже публиковаться так же открыто и прозрачно. На мой взгляд подход более чем жизнеспособный, когда есть открытость и прозрачность.
LLM может сообщить о недостатках, которые не заметили люди, это не замена людям, а ещё один фактор, мини-этап в ревью; если качественно обученная LLM, то она редко когда сругнётся там, где не о чем ругаться.
LLM+Proof assistant? Формулировать гипотезы, требующие формальной верификации, а LLM пусть пробует генерировать доказательства(и/или наоборот опровержения) к ним, которые можно автоматически проверять через Proof assistant (напр. Coq или Lean), чтобы эти гипотезы подтвердить/опровергнуть. Что область применения (возможно) слишком узкая (в частности из-за того, что пруф-ассистенты не полны по Тьюрингу) осознаю, тем не менее мне нравится сама идея — LLM генерирует, Proof assistant верифицирует.
Например в статье "DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data" (опубликована 23 мая 2024) вот такое пишут:
Abstract (аннотация статьи)
Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.
Ответ: если в "библиотеке советов и технологий №K"(этой сущности я давал определение выше, кратко: набор формальных утверждений непротиворечащих друг другу) есть уже ссылка на готовый код, удовлетворяющий вашим требованиям, то нейронка приведёт ссылку на него, потому что доказательство будет состоять из одного шага(просто взять решение из библиотеки).
Подробнее: Ваши требования формально записаны и решение из библиотеки уже удовлетворяет тем же требованиям(которые тоже записаны формально), нейронка вполне себе с большой вероятностью сможет угадать решение из одного шага, вы даже можете указать это как часть Ваших требований (чтобы решение состояло из одного шага, если это возможно).
С чего вы это взяли? Исходный запрос был - напиши мне то-то. Без понимания СМЫСЛА запроса 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, когда ответ скомпилировался, вот тогда он верифицирован и только тогда он выводится пользователю, пользователь может быть уверен, что цепочка логических рассуждений от "Дано" к "Доказать" строго математически доказана; чтоб не слишком долго ждать можно задать таймаут нейронке, тогда она может и не успеть сгенерировать доказательство).
Это на этапе подбора A и B (вообще говоря этот этап даже и не нужен, если сразу сформулировать их на языке Coq/Lean) и приведения решения к человеческому виду, я же предлагаю именно что добавить верифицируемость для доказательства A→B, хочу чтобы нейронка генерила код на Coq/Lean для строго математического доказательства и его же и выдавала, она не сможет ошибаться по определению(каждое доказательство проверяется через Coq/Lean), но может в принципе не смочь придумать доказательство.
Так секундочку, если 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) недавно предложенное, где нейросеть подольше пишет и сама свои ответы переваривает какое-то время, продолжая дальше бесконечно генерировать поток мыслей, а именно что верифицированный, логический подход (проверки на непротиворечивость на языке формальной верификации) во время "мышления".
<...> но вот толщина кошелька заказчика — а именно его время, количество запросов, которые он готов поддерживать общение — уже довольно ограниченное, особенно, когда пользователь более опытный <...>
Небольшая опечатка: здесь должно быть не "заказчика", а "пользователя".
Проверку решения задачи я всё ещё оставляю на совести пользователя нейронки, так что 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 есть на чём, есть уже много библитотек, в которых много что доказано, можно вот пробовать через них и обучить + возможно поучить переводу туда-сюда (формально-неформально) через добровольцев.
И ещё кое-что важное про такой метод: нейросеть ведь по сути может генерировать промежуточные гипотезы, которые попроще доказать, и верифицировать их, тем самым отгадывая шаги и пошагово прийти к доказательству, а потом взглянув на получившееся решение попробовать убрать лишние переходы, тем самым сократив решение. Было бы чем-то похоже на человеческий подход.
Мне почему-то нравится делать ставку на то, что в следующих итерациях уже будет участвовать верификация через Coq или Lean, то есть вот такая цепочка: человек формулирует задачу -> нейронка задает уточняющие вопросы, чтобы свести задачу к доказательству формальной теоремы, но при этом она не рассказывает какую выбрала математическую формализацию(потому что они обычно длинные и непонятные, долго понимать математические формализмы), если пользователь сам только не попросит -> поиск решения и проверка через язык формальной верификации (Coq или Lean) -> адаптация решения к максимально понятной и короткой для человека формулировке. Всякие верификации сильно повысили бы качество ответов, по крайней мере в науке бы пригодилось угадывать решения обучившись на уже известных ранее решённых задачах.
Планировщик для горутин на мой взгляд у них довольно неплохой, одна из идей состоит в том, что необязательно выделять отдельный системный поток[тред] всякий раз, когда хочешь запускать конкурентный код, можно редко выделять новые потоки, и по ним распределять по очереди выполнение конкурентных задач(которые выполняются в горутинах), чередовать задачки, если какая-то из них слишком уж долго выполняется, супер удобно что логикой того как именно оптимально перемещать задачи по потокам занимается сам Go через свой планировщик, а не программист вручную пишет логику выделения потоков.
Что такое заведомо мусор и/или ложные данные в Вашем исходном комментарии? Что значит "заведомо"? При каких обстоятельствах Вы считаете необходимым заводить уголовное дело, а при каких нет?
А судьи кто? Ложные данные и учёные иногда публикуют в своих статьях, только вот я не считаю хорошей идеей их за это сажать.
Можно какую-нибудь ссылку про это? Пока не нашёл нигде информации по этому поводу.
Буквально новость о том что не так, в другом мессенджере мне почему-то не нужно разрешение от высших мира сего, чтобы запустить своего бота, довольно удобно в другом их создавать, тестировать и выпускать прямо на платформе.
Если зафиксировать часы созвона общие для всех, то это ничем не отличается от общей для всех очной встречи, при условии дисциплинированности удалённых работников и заранее установленных рамок коммуникаций.
Если же офис предпочтительнее, только потому что можно без договоренности отвлечь сразу N сотрудников, потому что до них легко очно дойти, то не факт, что это лучше в плане организации — ведь их по итогу отвлекают во время работы в несогласовонное время, это может сбивать рабочий темп, тогда нужны сотрудники, которые могут работать очно и легко переключаться между задачами при условии, что их в любой момент видимо могут выдернуть из процесса работы, раз нет заранее согласования когда общая встреча(иначе непонятно чем удалёнка хуже, когда всё согласованно заранее).
Лично мне в таком режиме работать сложнее(когда меня могут отвлекать в произвольное время), чем в режиме с зафиксированными по времени (пусть даже ежедневными) встречами.
И всё равно продолжат показывать? :)
Смс-ки бывают дороже сервису, чем пуш-уведомления(зачем посредник, если можно без него), это может быть вопрос банальной экономии ресурсов даже.
Исходники клиентского приложения у телеграм открытые, сквозное шифрование можно по ним и почитать и проверить как работает, а ещё исходники можно собрать и пользоваться собранным приложением, вместо скачанного откуда бы ни было готового файла, внутри которого непонятно что.
А у Max где исходники почитать?
Неповторяющиеся ключи доступа к тем или иным ресурсам? В теории бывают и одинаковые в рамках одной компании/ одного человека, когда несколько репозиториев обращаются к одному и тому же ресурсу.
Не понимаю почему не жизнеспособная, согласно посту они выложили вообще всё: и веса модели, и процесс обучения, и подробности. Хотя бы в образовательном национальном плане это звучит полезно — люди могут наглядно учиться, делать лучше при желании, тоже публиковаться так же открыто и прозрачно. На мой взгляд подход более чем жизнеспособный, когда есть открытость и прозрачность.
LLM может сообщить о недостатках, которые не заметили люди, это не замена людям, а ещё один фактор, мини-этап в ревью; если качественно обученная LLM, то она редко когда сругнётся там, где не о чем ругаться.
LLM+Proof assistant? Формулировать гипотезы, требующие формальной верификации, а LLM пусть пробует генерировать доказательства(и/или наоборот опровержения) к ним, которые можно автоматически проверять через Proof assistant (напр. Coq или Lean), чтобы эти гипотезы подтвердить/опровергнуть. Что область применения (возможно) слишком узкая (в частности из-за того, что пруф-ассистенты не полны по Тьюрингу) осознаю, тем не менее мне нравится сама идея — LLM генерирует, Proof assistant верифицирует.
Например в статье "DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data" (опубликована 23 мая 2024) вот такое пишут:
Abstract (аннотация статьи)
Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.
Ответ: если в "библиотеке советов и технологий №K"(этой сущности я давал определение выше, кратко: набор формальных утверждений непротиворечащих друг другу) есть уже ссылка на готовый код, удовлетворяющий вашим требованиям, то нейронка приведёт ссылку на него, потому что доказательство будет состоять из одного шага(просто взять решение из библиотеки).
Подробнее: Ваши требования формально записаны и решение из библиотеки уже удовлетворяет тем же требованиям(которые тоже записаны формально), нейронка вполне себе с большой вероятностью сможет угадать решение из одного шага, вы даже можете указать это как часть Ваших требований (чтобы решение состояло из одного шага, если это возможно).
В третий раз упоминаю: ЧЕЛОВЕК должен проверять формальный вариант записи "Дано" и "Доказать" на языке Coq/Lean, не LLM (Вы должны уже обратить внимание, что я использую концепцию: любые данные в двух видах, первый вид неформальный, второй вид формальный -- буквально код на языке Coq/Lean), и только если они его устраивают, только тогда LLM переходит к этапу "Угадывания доказательства", причём решение верифицируется через Coq/Lean, оно не может быть "неверным", оно может либо найтись(и тогда оно верное), либо не найтись и тогда просто считайте, что LLM всегда отвечает в этом случае "я не смогла решить эту задачу". СМЫСЛ будет ровно тот, на который ВЫ сами и согласитесь, когда САМИ ПРОВЕРИТЕ формальные версии "Дано" и "Доказать", тогда гарантируется, что формальная версия доказательства доказывает ровно то, что требовалось, при тех ограничениях, которые были заданы. Считается, что любое решение вас удовлетворяет, покуда вас устраивает "Дано" и "Доказать" и выбранные вами библиотеки-математические-теории, но вы можете потом сами поменять "Дано" или "Доказать", накинув дополнительных ограничений.
А кто сейчас хранит всё? Какой смысл индексировать всякий мусор? Если вы спрашиваете про то, как же найти это самое уникальное решение через мой вариант LLM+верификация, то вот ответ: задать формальные "Дано" и "Доказать", получить верифицированное решение и воспользоваться им, возможно, что верифицированного решения не найдётся, ну, так бывает, значит на малых данных нейронка училась доказательствам, не научилась пока доказывать особенные случаи. Если же задача хоть сколько-нибудь стандартная, пусть в ней и немного новые параметры, которые ранее никто не применял, то цепочку рассуждений нейронка справится построить, если вы в "Дано" пропихнёте максимально подробную информацию (именно что в формальном виде) про эти параметры, то чего уж ей сложного будет проверить насколько согласованы остальные данные с тем что вы затребовали в "Дано", и с тем что желаете получить на выходе "Доказать".
Это как-то несерьёзно — не увидеть, что я использовал предложение вида "Не ... , а ... " (формально там было: "То есть непросто ..., а именно что ..."), то есть противопоставление, естественно, что всё стоит между "Не" и ", а" я согласен, что не очень (иначе зачем бы я стал использовать противительный союз "а") и его как-то нужно дорабатывать(или убрать, если вы это хотели сказать, то ок, мне без разницы, можно и убрать; просто вроде как Deepseek R1 именно за счёт небольшого окна с RL повысил точность, но даже если и не так, всё равно суть не в этом, уж прошу прощения, что привёл пример, когда его можно было бы избежать, учитывая, что основная моя идея с RL-то и не связана), так что незачем было пояснять.
И да, пока что нейросети не очень справляются генерировать доказательства даже для простых задачек из науки, например, на момент 23 мая 2024 года DeepSeek-Prover справился верно доказать всего лишь 5 из 148 международных задач по математике, а GPT-4 вообще ни одну не смог доказать, заметьте, это было соревнования пруф ассистентов на языке Lean, то есть их нагенериный код запускался и автоматически проверялся(если компилируется на Lean, значит доказательство математически верно), так что пока рано объективно оценивать насколько жизнеспособна идея генерировать доказательства нейронками, но на мой взгляд жизнеспособна.
Вот искреннее не понимаю, что непонятного в том, что я говорю что СМЫСЛ заключён в "Дано" и "Доказать" записанных в формальном виде(на Coq/Lean), ВЫ САМИ вот буквально пишете тот смысл, который вам нужен, а нейронка просто генерит верифицированные решения (если строго и формально: нейронка генерирует ответы до тех пор, пока ответ не скомпилируются на Lean/Coq, когда ответ скомпилировался, вот тогда он верифицирован и только тогда он выводится пользователю, пользователь может быть уверен, что цепочка логических рассуждений от "Дано" к "Доказать" строго математически доказана; чтоб не слишком долго ждать можно задать таймаут нейронке, тогда она может и не успеть сгенерировать доказательство).
Это на этапе подбора A и B (вообще говоря этот этап даже и не нужен, если сразу сформулировать их на языке Coq/Lean) и приведения решения к человеческому виду, я же предлагаю именно что добавить верифицируемость для доказательства A→B, хочу чтобы нейронка генерила код на Coq/Lean для строго математического доказательства и его же и выдавала, она не сможет ошибаться по определению(каждое доказательство проверяется через Coq/Lean), но может в принципе не смочь придумать доказательство.
Так секундочку, если 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) недавно предложенное, где нейросеть подольше пишет и сама свои ответы переваривает какое-то время, продолжая дальше бесконечно генерировать поток мыслей, а именно что верифицированный, логический подход (проверки на непротиворечивость на языке формальной верификации) во время "мышления".
Небольшая опечатка: здесь должно быть не "заказчика", а "пользователя".
Проверку решения задачи я всё ещё оставляю на совести пользователя нейронки, так что 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 есть на чём, есть уже много библитотек, в которых много что доказано, можно вот пробовать через них и обучить + возможно поучить переводу туда-сюда (формально-неформально) через добровольцев.
И ещё кое-что важное про такой метод: нейросеть ведь по сути может генерировать промежуточные гипотезы, которые попроще доказать, и верифицировать их, тем самым отгадывая шаги и пошагово прийти к доказательству, а потом взглянув на получившееся решение попробовать убрать лишние переходы, тем самым сократив решение. Было бы чем-то похоже на человеческий подход.
Надеюсь понятно объяснил в чём идея.
Мне почему-то нравится делать ставку на то, что в следующих итерациях уже будет участвовать верификация через Coq или Lean, то есть вот такая цепочка: человек формулирует задачу -> нейронка задает уточняющие вопросы, чтобы свести задачу к доказательству формальной теоремы, но при этом она не рассказывает какую выбрала математическую формализацию(потому что они обычно длинные и непонятные, долго понимать математические формализмы), если пользователь сам только не попросит -> поиск решения и проверка через язык формальной верификации (Coq или Lean) -> адаптация решения к максимально понятной и короткой для человека формулировке. Всякие верификации сильно повысили бы качество ответов, по крайней мере в науке бы пригодилось угадывать решения обучившись на уже известных ранее решённых задачах.
Планировщик для горутин на мой взгляд у них довольно неплохой, одна из идей состоит в том, что необязательно выделять отдельный системный поток[тред] всякий раз, когда хочешь запускать конкурентный код, можно редко выделять новые потоки, и по ним распределять по очереди выполнение конкурентных задач(которые выполняются в горутинах), чередовать задачки, если какая-то из них слишком уж долго выполняется, супер удобно что логикой того как именно оптимально перемещать задачи по потокам занимается сам Go через свой планировщик, а не программист вручную пишет логику выделения потоков.