9 posts
Верификация по методологии 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 это означает разные модели, разных провайдеров, возможно, разные…