12 posts
Seer поглощает деревья трейсов, связанные ошибки и данные профилирования для диагностики распределённых проблем. Вот как он на самом деле работает, где блестит и где всё ещё нужна человеческая помощь.
Фронтенд выдаёт 500. Stack trace указывает на React-компонент. Реальная проблема в трёх сервисах отсюда, в пуле соединений с базой данных, исчерпанном…
Large language models — неплохие партнёры для brainstorming при открытии test oracles, но они hallucinate свойства и упускают domain constraints. Вот как использовать их, не выкатывая фиктивные тесты.
Вам нужно протестировать функцию, где правильный вывод невозможно знать заранее. Оптимизатор маршрутов. Классификатор sentiment. Физическая симуляция. Вы…
Большие языковые модели могут помочь в триаже ложноположительных срабатываний статического анализа, но они не понимают семантику программ так, как это делает abstract interpretation. Вот как совместить оба подхода.
Ваш статический анализатор только что выдал 847 предупреждений в пятничный полдень. Вы знаете статистически, что где-то между 5% и 15% из них — настоящие баги.…
Верификация по методологии Cleanroom требует генерации и разрядки обязательств доказательства. Вот как LLM автоматизируют аннотации и генерацию VC, чтобы вы могли сосредоточиться на самых сложных доказательствах.
Cleanroom-инжиниринг программного обеспечения требует, чтобы вы доказали корректность своего кода ещё до компиляции. Это звучит благородно, пока вы не…
Я 30 дней писал объяснения дизайна перед тем, как просить код у LLM. Результаты изменили моё отношение к rubber-ducking.
Большинство разработчиков используют LLM наоборот. Мы описываем желаемое пятью словами, получаем 200 строк кода и следующий час тратим на отладку…
Диалоги с LLM содержат намерения, отвергнутые альтернативы и работающий код. Именно это и должна представлять собой документация. Вот как превратить эфемерный чат в долговечные, доступные для поиска документы, не теряя повествования.
Вы провели сорок пять минут с Claude, проектируя схему повторных попыток. Вы объяснили режимы отказов, отвергли экспоненциальный откат, потому что он скрывает…
Инспекции Фагана требуют от четырёх до шести человек и двух часов на проверку 250 строк. LLM может сократить эти затраты, взяв на себя подготовку и соблюдение чек-листа, но не может заменить человеческие роли, которые находят самые дорогие дефекты.
Полноценная инспекция Фагана требует модератора, читателя, от двух до четырёх инспекторов и автора. Команда тратит два часа на проверку примерно 250 строк кода…
Большие языковые модели пишут удивительно хороший код на Rust, но когда вы просите их о формальном доказательстве, они галлюцинируют инварианты и изобретают синтаксис, который не принимает ни один верификатор. Вот что они на самом деле делают правильно, где ломаются и как их всё равно использовать.
LLM могут писать Rust, который компилируется и даже проходит . Что они не могут делать надёжно — так это писать формальное доказательство того, что код…
LLMs галлюцинируют синтаксис, потому что делают probabilistic sampling токенов. Grammar-constrained decoding фильтрует vocabulary на каждом шаге, так что эмитируются только те токены, которые сохраняют синтаксическую валидность.
Попросите LLM сгенерировать JSON-объект, и рано или поздно он выдаст trailing comma, неэкранированный перевод строки внутри string, или bare word там, где…
Можно генерировать дизайн-токены из простых английских описаний, но только если рассматривать описание как DSL с ограниченным контекстом, со схемой-контрактом и снапшот-тестами.
Да, вы можете описать тему на английском и получить работающую дизайн-систему. Подвох в том, что описание на английском — это не промпт. Это исходный файл. И…
Запуск нескольких LLM параллельно позволяет отлавливать ошибки, которые любая отдельная модель уверенно пропустит. Вот как построить систему разрешения разногласий, которая действительно работает.
Вы отправляете промпт в GPT-4o. Он возвращает JSON с уверенностью 0.97. Вы отправляете тот же промпт в Claude 3.5 Sonnet. Он возвращает другой JSON, тоже с…
N-version programming с LLM не требует нескольких моделей. Можно извлечь разнообразные, корректные реализации из одной модели, варьируя промпты, персоны и ограничения на рассуждения.
N-version programming предполагает, что разнообразие приходит от разных авторов. С LLM это означает разные модели, разных провайдеров, возможно, разные…