Informal Systems ha desarrollado una herramienta llamada Quint para mejorar la fiabilidad del código generado por modelos de lenguaje grandes (LLMs). La herramienta surge de la preocupación por la creciente dependencia de la IA en la programación y la dificultad de validar la corrección del código generado, a menudo con resultados engañosos. Quint actúa como un puente entre el lenguaje natural y el código, permitiendo una validación más abstracta y ejecutable. La empresa utilizó Quint para realizar una modificación significativa en Malachite, un motor de consenso BFT (Byzantine Fault Tolerance) adquirido por Circle para su blockchain Arc, que normalmente llevaría meses, en tan solo una semana. El proceso involucró la creación de una especificación inicial en Quint, la modificación de esta especificación con la ayuda de IA, y la validación exhaustiva a través de pruebas de escenarios y verificación de propiedades. Quint facilita la detección temprana de errores, la validación del comportamiento y la generación de código más fiable, incluso permitiendo la validación del código con pruebas basadas en modelos y la verificación de trazas en entornos reales. La empresa enfatiza que Quint no reemplaza el diseño de protocolos por IA, sino que complementa el trabajo de los expertos humanos.
Noticias agregadas con IA