llm

9 posts

cleanroom-correctnessllmformal-proofsautomation

Los LLM no pueden demostrar que tu código es correcto, pero pueden escribir el código repetitivo que lo logra

La verificación Cleanroom requiere generar y descargar obligaciones de prueba. Así es como los LLM automatizan la anotación y la generación de condiciones de verificación (VC) para que puedas centrarte en las pruebas realmente difíciles.

La ingeniería de software Cleanroom exige que demuestres que tu código es correcto antes de compilarlo. Suena noble hasta que pasas tres horas escribiendo…
literate-programmingllmdocumentationai-engineering

Tu Thread con Claude Ya Es Documentación. Solo Muere en Doce Horas.

Las conversaciones con LLM contienen intención, alternativas rechazadas y código funcional. Eso es exactamente lo que la documentación debería ser. Aquí está cómo convertir chat efímero en documentación durable y buscable sin perder la narrativa.

Pasaste cuarenta y cinco minutos con Claude diseñando un circuito de reintento. Explicaste los modos de falla, rechazaste el backoff exponencial porque oculta…
fagan-inspectionsllmcode-reviewai-engineering

Un LLM puede pre-inspeccionar tu código. No puede dirigir la reunión.

Las inspecciones Fagan necesitan de cuatro a seis personas y dos horas para revisar 250 líneas. Un LLM puede reducir ese costo gestionando la preparación y el cumplimiento de checklist, pero no puede sustituir los roles humanos que encuentran los defectos más costosos.

Una inspección Fagan completa necesita un moderador, un lector, de dos a cuatro inspectores y el autor. El equipo dedica dos horas a revisar aproximadamente…
model-checkingllmrustformal-proofs

Los LLMs pueden generar código en Rust. Las pruebas formales son un problema completamente distinto.

Los grandes modelos de lenguaje escriben código en Rust sorprendentemente bueno, pero cuando les pides una prueba formal alucinan invariantes e inventan sintaxis que ningún verificador acepta. Esto es lo que realmente hacen bien, dónde fallan y cómo usarlos de todos modos.

Los LLMs pueden escribir Rust que compila e incluso pasa . Lo que no pueden hacer de forma confiable es escribir una prueba formal de que el código es correcto…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding: forzando a los LLMs a emitir sintaxis válida en cada token

Los LLMs alucinan sintaxis porque samplean tokens probabilísticamente. El grammar-constrained decoding filtra el vocabulario en cada paso para que solo se emitan tokens que preserven la validez sintáctica.

Pídele a un LLM que genere un objeto JSON y eventualmente emitirá una coma al final, un salto de línea sin escapar dentro de un string, o un bare word donde…
dsls-bounded-contextdesign-systemsllmthemes

Traducir del inglés a un tema es fácil. Hacerlo determinista es el verdadero problema.

Puedes generar design tokens a partir de descripciones simples en inglés, pero solo si tratas la descripción como un DSL de contexto delimitado con un contrato de schema y snapshot tests.

Sí, puedes describir un tema en inglés y obtener un design system funcional. El truco es que la descripción en inglés no es un prompt. Es un archivo fuente. Y…
n-version-programmingllmdifferential-testingdisagreement-resolution

¿Y si mis variantes de LLM discrepan? ¿Cuál tiene razón?

Ejecutar múltiples LLMs en paralelo detecta errores que cualquier modelo individual enviaría con total confianza. Así es como construir un sistema de resolución de discrepancias que realmente funciona.

Envías un prompt a GPT-4o. Devuelve un blob JSON con una confianza de 0.97. Envías el mismo prompt a Claude 3.5 Sonnet. Devuelve un blob JSON diferente,…
n-version-programmingllmdiverse-implementationsai-engineering

El mismo LLM puede escribir cinco versiones de tu función. Así es como hacerlas realmente diferentes.

La programación N-version con LLMs no requiere múltiples modelos. Puedes extraer implementaciones diversas y correctas de un solo modelo variando prompts, personas y restricciones de razonamiento.

La programación N-version asume que la diversidad proviene de diferentes autores. Con los LLMs, eso significa diferentes modelos, diferentes proveedores, tal…