llm

9 posts

cleanroom-correctnessllmformal-proofsautomation

Les LLM ne peuvent pas prouver que votre code est correct, mais ils peuvent écrire le code répétitif qui le fait

La vérification Cleanroom nécessite de générer et de lever des obligations de preuve. Voici comment les LLM automatisent l'annotation et la génération de conditions de vérification afin que vous puissiez vous concentrer sur les preuves réellement difficiles.

Le génie logiciel Cleanroom exige que vous prouviez la correction de votre code avant de le compiler. Cela semble noble jusqu'à ce que vous passiez trois…
literate-programmingllmdocumentationai-engineering

Votre Thread avec Claude Est Déjà de la Documentation. Il Meurt Juste en Douze Heures.

Les conversations avec les LLM contiennent l'intention, les alternatives rejetées et le code fonctionnel. C'est exactement ce que la documentation devrait être. Voici comment transformer un chat éphémère en documentation durable et consultable sans perdre la narration.

Vous avez passé quarante-cinq minutes avec Claude à concevoir un circuit de réessai. Vous avez expliqué les modes de défaillance, rejeté le backoff exponentiel…
fagan-inspectionsllmcode-reviewai-engineering

Un LLM peut pré-inspecter votre code. Il ne peut pas animer la réunion.

Les inspections Fagan nécessitent quatre à six personnes et deux heures pour examiner 250 lignes. Un LLM peut réduire ce coût en gérant la préparation et le respect des checklists, mais il ne peut pas remplacer les rôles humains qui trouvent les défauts les plus coûteux.

Une inspection Fagan complète nécessite un modérateur, un lecteur, deux à quatre inspecteurs et l'auteur. L'équipe passe deux heures à examiner environ 250…
model-checkingllmrustformal-proofs

Les LLMs peuvent générer du code Rust. Les preuves formelles sont un problème entièrement différent.

Les grands modèles de langage écrivent du Rust étonnamment bon, mais quand vous leur demandez une preuve formelle, ils hallucinent des invariants et inventent une syntaxe qu'aucun vérificateur n'accepte. Voici ce qu'ils font réellement bien, où ils échouent et comment les utiliser malgré tout.

Les LLMs peuvent écrire du Rust qui compile et même passe . Ce qu'ils ne peuvent pas faire de manière fiable, c'est écrire une preuve formelle que le code est…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding : forcer les LLMs à produire une syntaxe valide à chaque token

Les LLMs hallucinent la syntaxe parce qu'ils samplent les tokens de manière probabiliste. Le grammar-constrained decoding filtre le vocabulaire à chaque étape pour n'émettre que des tokens préservant la validité syntaxique.

Demandez à un LLM de générer un objet JSON et il finira par émettre une virgule finale, un saut de ligne non échappé à l'intérieur d'une string, ou un bare…
dsls-bounded-contextdesign-systemsllmthemes

Traduire de l'anglais vers un thème est facile. Le rendre déterministe est le vrai problème.

Vous pouvez générer des design tokens à partir de descriptions en anglais simple, mais seulement si vous traitez la description comme un DSL à contexte borné avec un contrat de schema et des snapshot tests.

Oui, vous pouvez décrire un thème en anglais et obtenir un design system fonctionnel. L'astuce est que la description en anglais n'est pas un prompt. C'est un…
n-version-programmingllmdifferential-testingdisagreement-resolution

Et si mes variantes de LLM n'étaient pas d'accord ? Laquelle a raison ?

Exécuter plusieurs LLM en parallèle permet de détecter des erreurs que tout modèle isolé enverrait avec assurance. Voici comment construire un système de résolution des désaccords qui fonctionne réellement.

Vous envoyez un prompt à GPT-4o. Il retourne un blob JSON avec un score de confiance de 0,97. Vous envoyez le même prompt à Claude 3.5 Sonnet. Il retourne un…
n-version-programmingllmdiverse-implementationsai-engineering

Le même LLM peut écrire cinq versions de votre fonction. Voici comment les rendre réellement différentes.

La programmation N-version avec les LLM ne nécessite pas plusieurs modèles. Vous pouvez extraire des implémentations diverses et correctes d'un seul modèle en faisant varier les prompts, les personas et les contraintes de raisonnement.

La programmation N-version part du principe que la diversité vient d'auteurs différents. Avec les LLM, cela signifie des modèles différents, des fournisseurs…