Leanstral: Agente de Código para Verificación Formal en Lean 4

El problema fundamental que Leanstral aborda es la escalabilidad de la verificación humana en el desarrollo de software y matemáticas formales, especialmente cuando se utilizan modelos de lenguaje grandes (LLMs) para la generación de código. A medida que los LLMs se vuelven más capaces en la producción de código, la verificación manual de su corrección se convierte en un cuello de botella significativo, requiriendo tiempo y experiencia especializada que impiden la velocidad de ingeniería.

Leanstral propone una solución al integrar la generación de código con la verificación formal. En lugar de que los humanos depuren la lógica generada por máquinas, el sistema permite a los ingenieros especificar lo que quieren y el agente se encarga de generar el código y, crucialmente, de probar formalmente su implementación contra esas especificaciones. Esto es particularmente relevante en dominios de alto riesgo, como las matemáticas de investigación o el software de misión crítica, donde los errores pueden tener consecuencias severas. La elección de Lean 4 como plataforma subraya este enfoque, ya que Lean es un asistente de pruebas diseñado para la expresión de objetos matemáticos complejos y especificaciones de software rigurosas.

Arquitectura del Sistema

Leanstral se implementa como un agente de código con una arquitectura altamente dispersa, optimizada para tareas de ingeniería de pruebas dentro del ecosistema Lean 4. Aunque el artículo no detalla la arquitectura interna del modelo de lenguaje subyacente, menciona que opera con 6B parámetros activos, lo que sugiere un diseño eficiente en comparación con modelos generalistas mucho más grandes. La eficiencia se logra mediante la inferencia paralela, utilizando Lean como un 'verificador perfecto'. Esto implica que, mientras el agente genera código o pruebas, Lean 4 evalúa y valida la corrección de las proposiciones y definiciones.

La integración con Lean 4 es clave. Leanstral está entrenado para operar en repositorios formales realistas, lo que implica una comprensión profunda de la sintaxis, semántica y las tácticas de prueba de Lean. Soporta 'arbitrary MCPs' (Meta-Programming Commands) a través de Mistral Vibe, y está específicamente entrenado para maximizar el rendimiento con 'lean-lsp-mcp', lo que sugiere una interacción profunda con el Language Server Protocol (LSP) de Lean para obtener información contextual y realizar manipulaciones de código y pruebas. El flujo de trabajo implica que Leanstral genera propuestas de código o pruebas, y Lean 4 las verifica, proporcionando retroalimentación que el agente puede usar para refinar sus resultados, en un ciclo iterativo de 'generación y verificación'.

inductive ceval : com → state → state → Prop where
| E_Skip (st : state) : ceval .CSkip st st
| E_Ass (st : state) (a1 : aexp) (n : Nat) (l : ident) (h : aeval a1 st = n) :
  ceval (.CAss l a1) st (update st l n)
| E_Seq (c1 c2 : com) (st st' st'' : state) (h1 : ceval c1 st st') (h2 : ceval c2 st' st'') :
  ceval (.CSeq c1 c2) st st''
| E_IfTrue (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = true) (h1 : ceval c1 st st') :
  ceval (.CIf b1 c1 c2) st st'
| E_IfFalse (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = false) (h1 : ceval c2 st st') :
  ceval (.CIf b1 c1 c2) st st'
| E_WhileEnd (b1 : bexp) (st : state) (c1 : com) (h : beval b1 st = false) :
  ceval (.CWhile b1 c1) st st
| E_WhileLoop (st st' st'' : state) (b1 : bexp) (c1 : com) (h1 : beval b1 st = true) (h2 : ceval c1 st st') (h3 : ceval (.CWhile b1 c1) st' st'') :
  ceval (.CWhile b1 c1) st' st''
-- Notation for command evaluation
notation:50 c " / " st " ⇒ " st' => ceval c st st'

-- Example command: adds 2 to variable X
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- Theorem: The plus2 command correctly adds 2 to variable X
-- Intuition: If X has value n in the initial state, after executing plus2,
-- X will have value n+2 in the final state
-- This specifies the behavior of the plus2 command
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') :
st' "X" = n + 2 := by
-- plus2 is defined as .CAss "X" (.APlus (.AId "X") (.ANum 2))
-- Use equation compiler to unfold it
change ceval (.CAss "X" (.APlus (.AId "X") (.ANum 2))) st st' at h2
cases h2 with
| E_Ass _ _ n l h =>
have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h
simp only [aeval] at this
rw [update]
simp [← this, h1]

Fundamentos Teóricos

El concepto de verificación formal de software tiene raíces profundas en la informática teórica, remontándose a trabajos pioneros como el de C.A.R. Hoare sobre la lógica de Hoare (1969) para razonar sobre la corrección de programas. La idea de que un programa debe satisfacer una especificación formal es central en este campo. Los asistentes de pruebas como Lean, Coq o Isabelle/HOL son la culminación de décadas de investigación en lógica matemática, teoría de tipos y sistemas de reescritura.

La aplicación de modelos de lenguaje grandes para la generación de código y pruebas se conecta con la investigación reciente en IA para la automatización de la demostración de teoremas y la síntesis de programas. Trabajos como 'Deep Learning for Code Synthesis' o 'Learning to Prove Theorems by Learning to Generate Proofs' exploran cómo los modelos neuronales pueden aprender patrones en el código y las pruebas formales para asistir o incluso automatizar estas tareas. Leanstral se sitúa en la intersección de estas dos áreas, buscando combinar la capacidad generativa de los LLMs con la rigurosidad de la verificación formal, un desafío que ha sido objeto de estudio en la comunidad de lenguajes de programación y lógica durante mucho tiempo.