Anthropic: verificación formal

Decidir qué significa correcto

Una empresa puede pedir que un programa «funcione bien» y descubrir después que cada participante entendía algo distinto. Para conversar con precisión conviene elegir una propiedad, una situación y una decisión. La calidad de esa conversación importa antes de revisar una demostración o comparar herramientas.

Caso completamente ficticio. La distribuidora Lumbre prepara un importador de documentos internos. En nuestro ejercicio, cada archivo contiene importes enteros en centavos y una etiqueta. El encargo pide separar filas aceptadas y rechazadas, conservar sus motivos y calcular un total. No existen clientes ni registros reales; tampoco hemos implementado o probado este importador.

Su equipo comienza escribiendo qué resultado necesita. «Parece razonable» no permite resolver un desacuerdo. En cambio, una regla explícita permite señalar el dato, la condición y la consecuencia que se están discutiendo. Esa es la primera pieza del expediente que construiremos.

Una frase que se pueda revisar

Lumbre elige una propiedad para esta práctica: el total mostrado debe coincidir con la suma de las filas aceptadas. También decide que una fila rechazada conserve un motivo. Son condiciones inventadas para aprender; no representan requisitos contables universales ni una certificación de un sistema.

Una persona podría objetar que se admitan importes negativos. Otra podría preguntar qué ocurre cuando falta la etiqueta. Resolver esas preguntas cambia el encargo. Conviene hacerlo explícitamente y guardar qué versión de las reglas acepta cada participante.

Separar lo mostrado y lo supuesto

El procedimiento convierte pruebas con entradas generadas —fuzzing— en especificaciones. Claude escribe demostraciones y Rocq las comprueba. Tras corregir fallos, el resultado principal abarca 239 puntos de entrada, con entradas menores de 64 MB, bajo supuestos de Linux, binarios estáticos monohilo y memoria fijada.

Para Lumbre, esa noticia invita a mejorar las preguntas del encargo. Pediría identificar la versión del archivo evaluado, la regla examinada y las condiciones que se conservaron. Es una propuesta de revisión para el caso ficticio; no afirmamos que sus archivos puedan entrar directamente en el procedimiento publicado.

El equipo podría mantener dos columnas: «evidencia recibida» y «condición pendiente». Una presentación convincente no completa por sí misma la segunda. Si el proveedor entrega un resultado sin identificar su versión, Lumbre conservaría la duda y pediría esa referencia antes de aceptar el expediente.

Del algoritmo a una regla que se conserva

Construyamos un modelo pequeño del importador ficticio. Una fila trae un importe y una decisión de aceptación ya resuelta. Para enseñar la suma, suponemos una lista finita y enteros matemáticos sin límite de tamaño. El siguiente pseudocódigo es una propuesta didáctica: no es una implementación ejecutada o probada.

total ← 0
para cada fila, en orden:
    si fila.aceptada:
        total ← total + fila.importe
devolver total

La afirmación que queremos sostener es: después de procesar las primeras k filas, total coincide con la suma de las aceptadas entre esas k filas. Es un invariante: una relación que debería conservar cada vuelta. Al inicio, k vale cero y ambas sumas son cero. Si la siguiente fila se acepta, ambos lados incorporan su importe. Si se rechaza, ninguno cambia. Al terminar la lista, la relación describe el total completo.

Para recorrer ese razonamiento, inventa tres filas: acepta sesenta, acepta cuarenta y rechaza veinte. El acumulador pasa por cero, sesenta, cien y cien. Este recorrido ilustra los pasos; la justificación anterior se apoya en las dos ramas del algoritmo, no en que esas tres cantidades hayan salido bien. El análisis de METR ofrece otro ejercicio sobre qué permite sostener una evidencia.

Usar ejemplos para aclarar una regla

Lumbre inventa dos filas aceptadas: seiscientos y cuatrocientos centavos. Añade una tercera de doscientos, rechazada por una etiqueta desconocida. Según el contrato elegido, el total esperado sería mil. Si la pantalla muestra mil doscientos, la discrepancia indica una pregunta concreta: por qué se incluyó la fila rechazada.

Después propone un archivo vacío, otro sin etiqueta y uno con un importe negativo. Antes de consultar una herramienta, las personas deben acordar qué esperan en cada caso. Si no logran hacerlo, han encontrado una ambigüedad del encargo que merece resolverse.

Estos ejemplos son materiales de conversación inventados. No hemos ejecutado una batería ni obtenido resultados del programa. Su función es ayudar a formular objeciones comprensibles. Una vez aclaradas, el equipo decidiría qué evidencia necesita para evaluar la entrega y quién puede producirla.

Un contraejemplo y todos los casos

Probar ejemplos consiste aquí en elegir listas concretas y observar sus salidas. También podríamos generar muchas listas para buscar discrepancias. Cada coincidencia responde por esos casos; deja abiertas las listas que no recorrimos. La afirmación universal del ejercicio exige justificar la relación para cualquier lista finita permitida por el modelo.

Ahora inventa un error: mover la suma fuera del condicional para incorporar también las filas rechazadas. La lista sesenta, cuarenta y veinte produciría ciento veinte, mientras la propiedad exige cien. Ese único contraejemplo basta para refutar la afirmación «siempre suma sólo lo aceptado». En cambio, cualquier cantidad de listas donde no aparezcan rechazos podría coincidir sin descubrir ese error.

La demostración por invariante evita enumerar todos los importes: cubre el inicio y explica por qué cada rama conserva la relación, sea cual sea la fila siguiente. Necesita además que el proceso termine; en este modelo se recorre una lista finita una vez. Es una justificación del algoritmo y sus supuestos, no una comprobación realizada sobre código de producción.

Si una implementación usa enteros de tamaño fijo, una suma podría desbordarse. Nuestro argumento con enteros matemáticos no resuelve ese caso: habría que limitar los valores o demostrar un manejo correcto del desbordamiento. Tampoco establece si la etiqueta de una fila debía aceptarse; eso pertenece a otra regla.

Proponer una prueba y comprobar sus pasos

Imagina dos roles para el ejercicio. Una persona propone el argumento; otra exige justificar cada transición. Un modelo podría proponer una secuencia de pasos, equivocarse o dejar un salto sin explicar. El papel del comprobador es verificar que los pasos admitidos permiten llegar a la conclusión a partir de las premisas, sin aceptar una frase sólo porque suena convincente.

Por ejemplo, «el total es correcto porque las tres filas coinciden» no demuestra nuestro invariante para cualquier lista. Una comprobación tendría que relacionar el estado inicial con la propiedad y resolver tanto la rama aceptada como la rechazada. Si una transición carece de respaldo, el argumento sigue pendiente. Este ejemplo explica los roles lógicos; no hemos construido una prueba formal ni usado un comprobador real.

Incluso un razonamiento válido puede contestar una pregunta equivocada. Si Lumbre quería sumar sólo importes positivos pero escribió «todos los aceptados», una demostración de esa frase no añade la condición olvidada. Asimismo, el modelo de enteros ilimitados y una implementación con límites necesitan una relación explícita. La especificación, los supuestos y la correspondencia con el programa forman parte del alcance que se debe revisar.

La lectura sobre identidad, permisos y evidencia de acceso ofrece una conversación complementaria: formular una conclusión y reunir evidencia suficiente para ella requieren preguntas precisas. En Lumbre, esas preguntas ahora apuntan a una propiedad, un algoritmo y unas condiciones identificables.

Comprueba qué puedes afirmar

Ejercicio estático. Lumbre recibe un informe vinculado a una versión anterior, mientras el archivo que quiere utilizar incorpora la etiqueta nueva. ¿Qué decisión permite tomar ese expediente? Escribe qué referencia falta y quién debería resolverla.

Respuesta razonada. El expediente describe una revisión anterior y un cambio posterior. Para aceptar la nueva entrega, falta aclarar cómo afecta ese cambio a las condiciones revisadas y qué evidencia corresponde a la versión actual. La información disponible permite identificar el pendiente, pero no cerrar el caso.

Una segunda pregunta: si el equipo descubre que la etiqueta debía rechazarse, ¿falló la herramienta o cambió la regla acordada? Conserva ambas versiones antes de responder. El objetivo pedagógico es distinguir una discrepancia del entregable de una modificación del encargo, sin atribuir causas que todavía no se han observado.

Una garantía con condiciones visibles

La publicación mantiene como componentes de confianza los modelos de máquina, los enunciados y el comprobador. Ofrece parte de sus pruebas; no hemos auditado esos materiales.

La investigación merece atención por la pregunta que abre para quienes encargan software. En una conversación de compra o desarrollo, pide que la garantía se relacione con una entrega identificable, un requisito acordado y condiciones que las personas puedan revisar. Esa petición es una propuesta editorial para tu proceso, no una evaluación independiente del trabajo anunciado.

Para empezar, elige una operación pequeña y escribe una condición de aceptación. Añade una duda que podría cambiarla y una referencia necesaria para resolverla. La siguiente decisión será más útil si deja visible qué conoces, qué falta y a quién corresponde comprobarlo.