Formally Verified Code Synthesis for Structured Data Translation in a Medical Internet of Things

Resumen Técnico: Síntesis de Código Formalmente Verificado para la Traducción de Datos Estructurados en un Internet de las Cosas Médicas

Planteamiento del Problema
La integración de nuevos dispositivos médicos en redes existentes de Internet de las Cosas Médicas (MIoT) presenta desafíos significativos, particularmente cuando no se dispone de la experiencia humana en desarrollo de software. Si bien los Modelos de Lenguaje de Gran Escala (LLMs) ofrecen potentes capacidades de síntesis de código, son propensos a las alucinaciones y a vulnerabilidades sutiles, lo que los hace poco fiables para dominios de atención médica con importancia crítica para la seguridad. El problema central abordado es la necesidad de generar automáticamente código de traducción confiable y fidedigno que convierta datos de formatos específicos de dispositivos (por ejemplo, esquemas JSON personalizados) en formatos de interoperabilidad estandarizados (por ejemplo, Fast Healthcare Interoperability Resources o FHIR) sin verificación manual, la cual suele ser intratable a escala.

Metodología
Los autores proponen una arquitectura neuro-simbólica que integra LLMs con verificación formal para sintetizar código correcto por construcción. El sistema se basa en ShinkaEvolve, un marco de optimización de código evolutivo de código abierto. El flujo de trabajo opera de la siguiente manera:

1. Búsqueda Evolutiva con LLMs: El sistema emplea un algoritmo evolutivo de múltiples islas donde los LLMs actúan como operadores. En lugar de mutaciones aleatorias, los LLMs proponen ediciones, reescrituras o mutaciones de programas semánticamente significativas basadas en un prompt que contiene programas padres, programas de "inspiración" y sus puntuaciones de aptitud (fitness scores).
2. Verificación Formal como Función de Aptitud: Para garantizar la fiabilidad, el sistema utiliza el Sistema de Verificación de Prototipos (PVS), un demostrador de teoremas, como evaluador. Se le encarga al LLM generar un teorema de traducción en el Lenguaje de Dominio Específico (DSL) de PVS que mapee un esquema JSON de entrada a un esquema JSON de salida.
   • La función de aptitud es binaria: un programa candidato recibe una puntuación de 1 si el demostrador de teoremas PVS verifica que la traducción es correcta (es decir, todos los inputs válidos mapean a outputs válidos que satisfacen el esquema objetivo), y 0 en caso contrario.
   • Para mitigar la limitada familiaridad del LLM con PVS, el prompt incluye una referencia de lenguaje y ejemplos contextuales de traducciones de esquemas simples.
3. Generación de Código: Una vez que un teorema es formalmente verificado, el sistema utiliza herramientas adicionales para transformar de manera determinista el teorema PVS verificado en código C ejecutable, adecuado para su despliegue dentro del entorno con recursos limitados de la MIoT.

Contribuciones Clave

• Pipeline Neuro-Simbólico: La integración de una búsqueda evolutiva impulsada por LLM con un demostrador formal de teoremas (PVS) para garantizar que el código sintetizado satisfaga requisitos estructurales estrictos.
• Caso de Estudio de MIoT: Una demostración práctica de la integración de un pulsioxímetro en una red MIoT basada en vehículos. El sistema traduce con éxito el esquema JSON personalizado del dispositivo al formato de recurso de Observación de FHIR estándar.
• Fiabilidad de Bajo Costo: La demostración de que el código formalmente verificado puede generarse de manera consistente con una sobrecarga computacional y financiera baja.

Resultados Experimentales
Los autores realizaron 10 ejecuciones experimentales independientes, cada una consistiendo en 20 generaciones a través de dos islas evolutivas, para analizar la integración del pulsioxímetro.

• Tasa de Éxito: El sistema alcanzó una tasa de éxito del 37.4% ± 22.4% (la fracción de programas generados por el LLM que pasaron la verificación).
• Eficiencia: El primer teorema exitoso se encontró, en promedio, en la Generación 5.0. El tiempo promedio para encontrar el primer programa exitoso fue de 10.4 minutos, con un tiempo total de ejecución (wall-clock time) de 42.7 minutos por experimento.
• Costo: El costo promedio de la API por experimento fue de $0.87. Crucialmente, el costo incurrido antes de encontrar la primera prueba exitosa fue solo de $0.18 (aproximadamente el 20% del presupuesto total).
• Rendimiento del Modelo: Se utilizó un ensamble de modelos (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) con ponderación dinámica mediante muestreo de Thompson. GPT-5 representó el 33.7% de las selecciones pero generó el 53.5% de los programas exitosos, lo que indica que los modelos más grandes fueron más efectivos para generar teoremas de PVS correctos.
• Convergencia: A pesar de las variaciones en las rutas de selección de los LLM y los fallos intermedios, los 10 experimentos convergieron a soluciones semánticamente idénticas, lo que sugiere que las restricciones formales del esquema FHIR son altamente prescriptivas.

Significancia y Reivindicaciones
El artículo posiciona este trabajo como un "primer paso" hacia la integración confiable de nuevos dispositivos en la infraestructura de atención médica existente. Los autores afirman que su sistema demuestra la viabilidad de generar código de traducción formalmente verificado a un bajo costo, asegurando que los datos estructurados traducidos por el código generado siempre se ajusten al esquema de salida objetivo.

La significancia radica en abordar la naturaleza crítica para la seguridad de los sistemas de salud al fundamentar la capacidad de razonamiento de los LLM en la verificación formal, mitigando así los riesgos de alucinación y garantizando la fiabilidad sin requerir la experiencia de un desarrollador de software humano. Los autores declaran explícitamente que el trabajo futuro implicará la expansión del conjunto de dispositivos, la verificación de componentes de red e la integración de esta etapa de verificación en un flujo de trabajo totalmente agéntico.