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

Resumo Técnico: Síntese de Código Formalmente Verificado para Tradução de Dados Estruturados em uma Internet das Coisas Médica

Declaração do Problema
A integração de novos dispositivos médicos em redes existentes de Internet das Coisas Médicas (MIoT) apresenta desafios significativos, particularmente quando a expertise humana em desenvolvimento de software não está disponível. Embora os Grandes Modelos de Linguagem (LLMs) ofereçam capacidades poderosas de síntese de código, eles são propensos a alucinações e vulnerabilidades sutis, tornando-os pouco confiáveis para domínios de saúde críticos para a segurança. O problema central abordado é a necessidade de gerar automaticamente código de tradução confiável e íntegro que converta dados de formatos específicos de dispositivos (ex: esquemas JSON customizados) em formatos de interoperabilidade padronizados (ex: Fast Healthcare Interoperability Resources ou FHIR) sem verificação manual, o que é frequentemente intratável em escala.

Metodologia
Os autores propõem uma arquitetura neuro-simbólica que integra LLMs com verificação formal para sintetizar código correto por construção (correct-by-construction). O sistema é construído sobre o ShinkaEvolve, um framework de otimização de código evolutivo de código aberto. O pipeline opera da seguinte forma:

1. Busca Evolutiva com LLMs: O sistema emprega um algoritmo evolutivo de múltiplas ilhas onde os LLMs atuam como operadores. Em vez de mutações aleatórias, os LLMs propõem edições, reescritas ou mutações de programas semanticamente significativas baseadas em um prompt contendo programas pais, programas de "inspiração" e seus respectivos escores de aptidão (fitness scores).
2. Verificação Formal como Função de Aptidão: Para garantir a confiabilidade, o sistema utiliza o Prototype Verification System (PVS), um provador de teoremas, como o avaliador. O LLM é incumbido de gerar um teorema de tradução na Linguagem de Domínio Específico (DSL) do PVS que mapeia um esquema JSON de entrada para um esquema JSON de saída.
   • A função de aptidão é binária: um programa candidato recebe um escore de 1 se o provador de teoremas PVS verificar que a tradução é correta (ou seja, todos os inputs válidos mapeiam para outputs válidos que satisfazem o esquema alvo) e 0 caso contrário.
   • Para mitigar a familiaridade limitada do LLM com o PVS, o prompt inclui uma referência de linguagem e exemplos contextuais de traduções de esquemas simples.
3. Geração de Código: Uma vez que um teorema é formalmente verificado, o sistema utiliza ferramentas adicionais para transformar deterministicamente o teorema PVS verificado em código C executável, adequado para implantação no ambiente de recursos limitados da MIoT.

Principais Contribuições

• Pipeline Neuro-Simbólico: A integração de uma busca evolutiva impulsionada por LLM com um provador de teoremas formal (PVS) para garantir que o código sintetizado satisfaça requisitos estruturais estritos.
• Estudo de Caso MIoT: Uma demonstração prática da integração de um oxímetro de pulso em uma rede MIoT baseada em veículo. O sistema traduz com sucesso o esquema JSON customizado do dispositivo para o formato de recurso Observation do padrão FHIR.
• Confiabilidade de Baixo Custo: A demonstração de que o código formalmente verificado pode ser gerado consistentemente com baixo overhead computacional e financeiro.

Resultados Experimentais
Os autores conduziram 10 execuções experimentais independentes, cada uma consistindo em 20 gerações através de duas ilhas evolutivas, para analisar a integração do oxímetro de pulso.

• Taxa de Sucesso: O sistema alcançou uma taxa de sucesso de 37,4% ± 22,4% (a fração de programas gerados por LLM que passaram na verificação).
• Eficiência: O teorema bem-sucedido mais precoce foi encontrado, em média, na Geração 5.0. O tempo médio para encontrar o primeiro programa bem-sucedido foi de 10,4 minutos, com um tempo total de execução (wall-clock time) de 42,7 minutos por experimento.
• Custo: O custo médio total de API por experimento foi de US$ 0,87. Crucialmente, o custo incorrido antes de encontrar a primeira prova bem-sucedida foi de apenas US$ 0,18 (aprox. 20% do orçamento total).
• Desempenho do Modelo: Um ensemble de modelos (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) foi utilizado com ponderação dinâmica via amostragem de Thompson. O GPT-5 respondeu por 33,7% das seleções, mas gerou 53,5% dos programas bem-sucedidos, indicando que modelos maiores foram mais eficazes na geração de teoremas PVS corretos.
• Convergência: Apesar de caminhos de seleção de LLM e falhas intermediárias variáveis, todos os 10 experimentos convergiram para soluções semanticamente idênticas, sugerindo que as restrições formais do esquema FHIR são altamente prescritivas.

Significância e Alegações
O artigo posiciona este trabalho como um "primeiro passo" em direção à integração confiável de novos dispositivos em infraestruturas de saúde existentes. Os autores afirmam que seu sistema demonstra a viabilidade de gerar código de tradução formalmente verificado a um baixo custo, garantindo que os dados estruturados traduzidos pelo código gerado sempre conformem ao esquema de saída alvo.

A significância reside em abordar a natureza crítica para a segurança dos sistemas de saúde ao fundamentar o poder de raciocínio dos LLMs na verificação formal, mitigando assim os riscos de alucinação e garantindo a confiabilidade sem exigir expertise humana em desenvolvimento de software. Os autores declaram explicitamente que o trabalho futuro envolverá a expansão do conjunto de dispositivos, a verificação de componentes de rede e a integração desta etapa de verificação em um pipeline totalmente agêntico.