Basis Research: verificación de semánticas de LLMs mediante Lean

Basis Research ha desarrollado un método para generar semánticas formales de lenguajes de programación sin ellas mediante agentes de inteligencia artificial, resolviendo así un cuello de botella crítico en la verificación de software. El enfoque, detallado en un artículo técnico, utiliza Lean para demostrar que la semántica generada por un LLM coincide exactamente con el comportamiento de un intérpreter compilado a RISC-V, que actúa como verdad fundamental. Este proceso permite que la semántica sea verificada matemáticamente, evitando errores que podrían pasar pruebas empíricas pero comprometer la seguridad del software. El equipo de investigación, liderado por Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu y Zenna Tavares, aplicó este método a una extensión del lenguaje WHILE, demostrando cómo los LLMs pueden escribir reglas formales que se prueban rigurosamente. La iniciativa busca escalar la verificación de software a infraestructuras críticas, asegurando que los sistemas sean seguros por diseño y mantengan el ritmo con las capacidades crecientes de los atacantes. El proyecto está disponible en GitHub y representa un avance significativo en la automatización de la verificación formal, integrando la capacidad de los LLMs con la precisión de la verificación matemática.