El artículo de theorem.dev presenta lf-lean, un proyecto innovador que explora el futuro de la ingeniería de software verificada. El problema central que aborda es cómo garantizar la corrección del código generado por la inteligencia artificial (IA), especialmente cuando la capacidad de generación de código de la IA supera la capacidad humana de revisión. La revisión manual tradicional no escala bien, convirtiéndose en un cuello de botella.
La solución propuesta es el uso de 'generadores de especificaciones de nivel de tarea'. En lugar de revisar cada línea de código generado individualmente, se define una especificación de corrección general para una clase entera de tareas (como la traducción de código). Esta especificación se verifica automáticamente en todas las instancias de esa tarea, independientemente del código base. Esto reduce significativamente el esfuerzo humano de supervisión, pasando de una relación lineal (proporcional al número de tareas) a una constante (esencialmente, un esfuerzo fijo).
El proyecto lf-lean demuestra esto traduciendo los 1.276 enunciados del libro de texto 'Logical Foundations' de Rocq a Lean, utilizando IA con una mínima intervención humana (aproximadamente 2 días de trabajo). El equipo estima que esta tarea habría requerido 2,75 años de trabajo manual, mientras que con el enfoque de lf-lean se logró en cuestión de días, representando una aceleración de 350 veces. La herramienta rocq-dove es el prototipo de generador de especificaciones de nivel de tarea utilizado, que automáticamente genera especificaciones de corrección y evalúa las traducciones generadas por la IA.
Este avance sugiere que la ingeniería de software verificada está progresando más rápido de lo esperado, y que la verificación automática de código podría convertirse en una práctica estándar en una era de programación asistida por IA. El artículo destaca que, a medida que la IA genera más código, la verificación automática se vuelve esencial, ya que la revisión humana no puede seguir el ritmo. La clave está en definir especificaciones de corrección genéricas que se apliquen a múltiples casos, lo que permite a la IA iterar hacia soluciones correctas de manera autónoma y reduce drásticamente la carga de trabajo humana.