9 posts
Die Cleanroom-Verifikation erfordert die Erzeugung und Erfüllung von Proof Obligations. So automatisieren LLMs die Annotation und die VC-Generierung, damit Sie sich auf die eigentlich schwierigen Beweise konzentrieren können.
Die Cleanroom-Softwareentwicklung verlangt, dass Sie die Korrektheit Ihres Codes beweisen, bevor Sie ihn kompilieren. Das klingt edel, bis Sie drei Stunden…
Ich verbrachte 30 Tage damit, Design-Erklärungen zu schreiben, bevor ich ein LLM um Code bat. Die Ergebnisse veränderten meine Sicht auf Rubber-Ducking.
Die meisten Entwickler nutzen LLMs rückwärts. Wir beschreiben in fünf Wörtern, was wir wollen, bekommen 200 Zeilen Code zurück und verbringen die nächste…
LLM-Konversationen enthalten Absicht, abgelehnte Alternativen und funktionierenden Code. Genau das sollte Dokumentation sein. So verwandeln Sie flüchtigen Chat in dauerhafte, durchsuchbare Docs, ohne die Erzählung zu verlieren.
Sie haben fünfundvierzig Minuten mit Claude damit verbracht, einen Retry-Circuit zu entwerfen. Sie haben die Failure Modes erklärt, exponentielles Backoff…
Fagan-Inspektionen benötigen vier bis sechs Personen und zwei Stunden, um 250 Zeilen zu reviewen. Ein LLM kann diese Kosten senken, indem es Vorbereitung und Checklisten-Überwachung übernimmt, aber es kann die menschlichen Rollen nicht ersetzen, die die teuersten Defekte finden.
Eine vollständige Fagan-Inspektion benötigt einen Moderator, einen Vorleser, zwei bis vier Inspektoren und den Autor. Das Team verbringt zwei Stunden damit,…
Große Sprachmodelle schreiben erstaunlich guten Rust-Code, aber wenn man sie um einen formalen Beweis bittet, halluzinieren sie Invarianten und erfinden Syntax, die kein Verifizierer akzeptiert. Hier ist, was sie tatsächlich richtig machen, wo sie scheitern und wie man sie dennoch nutzen kann.
LLMs können Rust schreiben, das kompiliert und sogar besteht. Was sie nicht zuverlässig können, ist einen formalen Beweis dafür zu führen, dass der Code für…
LLMs halluzinieren Syntax, weil sie Tokens probabilistisch sampeln. Grammar-constrained decoding filtert das Vokabular in jedem Schritt, sodass nur Tokens emittiert werden, die die syntaktische Gültigkeit erhalten.
Bitten Sie einen LLM, ein JSON-Objekt zu generieren, und er wird irgendwann ein abschließendes Komma ausgeben, einen nicht escapten Zeilenumbruch innerhalb…
Du kannst Design-Tokens aus einfachen englischen Beschreibungen generieren, aber nur, wenn du die Beschreibung als DSL mit begrenztem Kontext, Schema-Vertrag und Snapshot-Tests behandelst.
Ja, du kannst ein Theme auf Englisch beschreiben und ein funktionierendes Design-System erhalten. Der Haken ist, dass die englische Beschreibung kein Prompt…
Die parallele Ausführung mehrerer LLMs deckt Fehler auf, die jedes einzelne Modell selbstbewusst ausliefert. So baut man ein Disagreement-Resolution-System, das tatsächlich funktioniert.
Du schickst einen Prompt an GPT-4o. Es liefert einen JSON-Blob mit einer Confidence von 0,97 zurück. Du schickst denselben Prompt an Claude 3.5 Sonnet. Es…
N-Version-Programming mit LLMs erfordert keine mehreren Modelle. Du kannst vielfältige, korrekte Implementierungen aus einem einzigen Modell extrahieren, indem du Prompts, Personas und Reasoning-Constraints variierst.
N-Version-Programming geht davon aus, dass Vielfalt von unterschiedlichen Autoren kommt. Bei LLMs bedeutet das: verschiedene Modelle, verschiedene Anbieter,…