Охота на математику

Для человека с обычным мышлением использование логики универсума для промптинга нейросетей означает переход от интуитивного «общения» с моделью к математически точному проектированию запросов. Современные нейросети (такие как GPT-4) находятся на адаптивном уровне (2У), то есть они лишь подбирают ответы на основе вероятностей и заложенных шаблонов, но не «думают» в строгом логическом смысле. Чтобы повысить качество работы нейросети и перевести её на предикционный уровень (3У) — уровень получения новых...

Как устроено «мышление» нейросети по сравнению с человеческим. Нейросеть не понимает — она вычисляет. Отсюда все отличия. Человек: «Не думай о белой обезьяне» → сразу представляет белую обезьяну, а потом пытается ее запретить. Нейросеть: Видит токены: [Не] [думай] [о] [белой] [обезьяне]. Статистически, после слова «обезьяна» чаще идут позитивные или нейтральные продолжения. Токен «Не» влияет слабо, если в обучающей выборке не было миллиона примеров, где «не Х» = «Y». Что получается: Нейросеть легко игнорирует отрицание, особенно в длинных запросах...

В теории функциональных систем Петра Кузьмича Анохина спешка — системоразрушающий фактор. Краткое резюме для тех, кто спешит )-: Согласно Анохину, результат умственного труда — это принятие оптимального решения. Спешка блокирует механизм акцептора результатов действия (сличение прогноза с реальностью), заменяя его грубым методом «тыка». В итоге система не находит нужное решение (полезный результат), а впадает в хаос (стресс). Разберем по этапам (как работает система Анохина): 1. Что такое интеллектуальный акт с точки зрения Анохина? Это не просто «думанье»...

Будущее за мультиагентной оркестрацией, но не в том виде, в котором ее пытаются продать сейчас Мультиагентность неизбежна, но она будет выглядеть радикально иначе, чем сегодняшние поделки с десятком агентов, ссорящихся за один файл. Почему без мультиагентности никуда (неизбежность) Существует три главные причины, почему отказ от одного агента — вопрос времени. Почему текущий подход обречен (болезни роста) Сейчас умирает несколько устоявшихся практик: Как будет выглядеть реальный сценарий в 2027-2028 годах Представьте, что вы запускаете задачу в Jira: «Добавить двухфакторную аутентификацию». Вместо привычного оркестратора происходит следующее...

Фраза «Cum panis» переводится с латыни как «с хлебом». Однако важно отметить грамматический нюанс: правильно с точки зрения классической латыни было бы «cum pane» (аблятив), так как предлог cum требует аблативного падежа. Форма «panis» — это именительный или родительный падеж. Таким образом, в зависимости от контекста: Латинское «cum panis» (или, грамматически вернее, cum pane) означает «с хлебом»...

Деньги и учёные не отменяют теорему Райса (1953): «Никакое нетривиальное свойство программы нельзя вычислить алгоритмически». Свойство «Цена обновилась правильно» — можно доказать тройкой Хоара. Здесь у нас есть чёткое формальное определение: цена в Bitrix24 должна равняться цене в Google Sheets. Свойство «Нейросеть распознала кошку» — нельзя доказать тройкой Хоара. Потому что непонятно, что значит «правильно». Это статистическое понятие, а не формально-логическое. Свойство «LLM не сгенерирует оскорбление» — нельзя доказать тройкой Хоара. Нельзя перебрать все возможные входы и выходы, а само понятие «оскорбление» размыто и зависит от контекста...

Четает, читает ... спотыкается на первой формуле: φ ::= p | ¬φ | (φ ∨ φ) Стоять. (φ ∨ φ) ? Странно. Похоже опечатка? Судя по тексту ниже должно быть φ ::= p | ¬φ | (φ ∨ ψ) Зато следующая формула понятная...

В процессе создания программы ваш код оценивают три совершенно разных «судьи». Первый — компилятор. Ему важно только одно: соблюдены ли правила языка? Он проверит синтаксис, поверхностно — типы данных, убедится, что все переменные объявлены. Но вопрос «решает ли код правильную задачу?» компилятор даже не рассматривает. Ему всё равно, что функция поделит число на ноль или выйдет за границы массива. Его типичная реакция на ошибку выглядит так: «Тип Int не соответствует типу String». Второй проверяющий — заказчик или тестировщик. Этому уже не всё равно. Он проверяет бизнес-логику, краевые случаи, соответствие требованиям...

Владимир Воеводский не просто связан с теорией типов в программировании — он произвел в этой области настоящую революцию. Его главное достижение, аксиома унивалентности (Univalence Axiom), и созданная им гомотопическая теория типов (Homotopy Type Theory, HoTT) предлагают принципиально новый взгляд на фундамент математики и, как следствие, на то, как мы пишем и проверяем программы. Связь Воеводского с теорией типов можно проследить через несколько ключевых идей. Долгое время существовала параллель: тип в программировании похож на множество в математике. Воеводский (и независимо от него Стив Аводи...

сетевой график (например, PERT/CPM) — это буквально диаграмма в категории, где объекты — события (вершины), а стрелки — работы (морфизмы). Но главное контринтуитивное усиление из теории категорий — это переход от «чисел на стрелках» (длительности) к структуре и эквивалентностям. Вот ключевые точки связи: Итог: Сетевой график — это частный случай диаграммы в категории. А теория категорий даёт язык, чтобы видеть инварианты перепланировки, универсальные способы вычисления ранних/поздних сроков без перебора, и, главное, легко переходить от графика работ к графику ресурсов, рисков или бюджетов, не теряя структуры зависимостей...

Индустрия строит костыли (обёртки, цепочки, фреймворки), чтобы компенсировать фундаментальную особенность LLM — она генерирует статистически среднее, а не логически правильное. Прописывать примеры хорошего и плохого кода в промптах — эффективный метод. LLM — это не инженер (внезапно), а архив частот. Она видела миллиарды примеров кода. На вопрос «напиши функцию для FTP» она выдаёт то, что чаще всего встречала: стандартное имя функции, стандартную обработку ошибок, стандартное логирование. Проблема: «Стандартное» ≠ «то, что нужно». У меня проверенная специфическая архитектура (NS_Container, Railway-декораторы, режимы локальных файлов)...

Корневую проблему всей разработки ПО, которую LLM не решили — а только обострили. Короткий ответ: да, люди не умеют объяснять. И это не их вина. Это фундаментальное ограничение того, как работает человеческое мышление и коммуникация. Нефть не спрашивает «а куда ты хочешь, чтобы я текла?» Её заставляют законы физики. Поезд не говорит «мне кажется, рельсы кривые» — он или едет, или сходит с них. А программист (и LLM) каждый раз заново интерпретирует: «А что значит "быстро"? А что значит "удобно"? А что значит "правильно"?» В голове у заказчика (или у вас) есть идеальный образ результата...