Para garantizar que el software sea seguro por diseño, los investigadores a menudo utilizan la verificación formal, un proceso que emplea pruebas matemáticas para descartar clases enteras de errores. Un obstáculo principal en este campo es el problema de la 'especificación': para demostrar que un programa es correcto, primero se debe definir una semántica formal (una descripción matemática precisa de cómo se comporta cada sentencia y bucle). Si bien algunos lenguajes como WebAssembly o C tienen semánticas establecidas, muchos otros no las tienen. Sin una especificación precisa, no existe una verdad fundamental contra la cual demostrar la seguridad de un programa.
Los investigadores de Basis abordaron esto utilizando Modelos de Lenguaje de Gran Escala (LLMs) para generar estas semánticas para un pequeño lenguaje imperativo llamado WHILE. Sin embargo, debido a que los LLMs pueden cometer errores, una semántica defectuosa invalidaría cualquier prueba posterior. Para resolver esto, el equipo propuso un enfoque 'radical': tratar el intérprete existente —el programa real que ejecuta el código— como la verdad fundamental. Compilaron el intérprete basado en C a código de máquina RISC-V, el cual tiene un conjunto de instrucciones definido formalmente. Luego, encargaron a un LLM la tarea de escribir un conjunto de reglas legibles (la semántica) y una prueba matemática en Lean (un asistente de pruebas) para demostrar que estas reglas predicen perfectamente el comportamiento del binario compilado.
El diagrama ilustra el enfoque 'radical' de utilizar el intérprete compilado como la verdad fundamental para depurar y refinar la semántica de alto nivel.
Este método obligó al LLM a tener en cuenta detalles de implementación sutiles que a menudo se omiten en las especificaciones escritas por humanos. Por ejemplo, la prueba falló inicialmente porque la semántica del LLM no contemplaba un límite de 63 bytes sobre cómo el intérprete en C renderiza los nombres de las funciones en cadenas. La prueba solo se 'cerró' una vez que la semántica se corrigió para coincidir con el comportamiento real del binario. Al utilizar el intérprete compilado como ancla, los investigadores crearon un sistema donde el propio proceso de prueba actúa como un depurador para la semántica. Si la prueba falla, indica una discrepancia entre las reglas de alto nivel y la ejecución de bajo nivel, obligando al modelo a refinar las reglas hasta que se alineen perfectamente con el código de máquina.
Esta visualización explica la división estructural del proyecto entre los anclajes de hardware/software fijos y los componentes generados por el LLM.