Los investigadores proponen una arquitectura neural consistente en ciclo que genera explicaciones en lenguaje natural fieles para certificados de verificación formal, abordando la opacidad de estas pruebas verificables por máquina para no especialistas. El sistema alcanza una solidez verificada en ciclo del 90.0% en datos de prueba de un dominio de cumplimiento financiero, superando significativamente a las líneas base multi-LLM tanto en precisión como en velocidad de inferencia.
- La arquitectura utiliza una red directa (NN1) para mapear certificados a explicaciones y una red inversa (NN2) para reconstruir certificados, con un verificador simbólico cerrando el bucle para una fiabilidad diferenciable.
- Un mecanismo de generador-puntero asegura la fundamentación léxica copiando directamente los nombres de estado desde el certificado, evaluado en 420 certificados de prueba que abarcan seis métodos de verificación.
- El modelo alcanza una solidez verificada en ciclo del 90.0%, superando la mejor línea base few-shot multi-LLM del 76.1% por 13.9 puntos porcentuales.
- Gana en 10 de las 12 categorías de veredicto/tipo, con tres categorías alcanzando una solidez del 100%.
- El sistema ofrece una inferencia 860x más rápida (185 ms vs. 160 s), operación sin conexión, salidas deterministas y costo cero por inferencia en comparación con LLMs basados en la nube.
Este enfoque demuestra que la especialización entrenada supera a la indicación de LLM de propósito general para la explicación estructurada de certificados mientras elimina las restricciones de implementación asociadas con la inferencia basada en la nube.