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

Sintesi Tecnica: Sintesi di Codice Formalmente Verificato per la Traduzione di Dati Strutturati in un Medical Internet of Things

Definizione del Problema
L'integrazione di nuovi dispositivi medici in reti Medical Internet of Things (MIoT) esistenti presenta sfide significative, in particolare quando non è disponibile l'esperienza di sviluppo software umana. Sebbene i Large Language Models (LLM) offrano potenti capacità di sintesi del codice, essi sono soggetti ad allucinazioni e vulnerabilità sottili, il che li rende inaffidabili per i domini sanitari critici per la sicurezza. Il problema centrale affrontato è la necessità di generare automaticamente codice di traduzione affidabile e fidato che converta i dati da formati specifici del dispositivo (ad esempio, schemi JSON personalizzati) in formati di interoperabilità standardizzati (ad esempio, Fast Healthcare Interoperability Resources o FHIR) senza verifica manuale, che è spesso intrattabile su larga scala.

Metodologia
Gli autori propongono un'architettura neuro-simbolica che integra gli LLM con la verifica formale per sintetizzare codice corretto per costruzione (correct-by-construction). Il sistema si basa su ShinkaEvolve, un framework open-source di ottimizzazione evolutiva del codice. La pipeline opera come segue:

1. Ricerca Evolutiva con LLM: Il sistema impiega un algoritmo evolutivo multi-isola in cui gli LLM agiscono come operatori. Invece di mutazioni casuali, gli LLM propongono modifiche, riscritture o mutazioni semantiche del programma basate su un prompt contenente programmi genitori, programmi di "ispirazione" e i loro punteggi di idoneità (fitness scores).
2. Verifica Formale come Funzione di Idoneità: Per garantire l'affidabilità, il sistema utilizza il Prototype Verification System (PVS), un dimostratore di teoremi, come valutatore. L'LLM ha il compito di generare un teorema di traduzione nel linguaggio DSL del PVS che mappi uno schema JSON di input in uno schema JSON di output.
   • La funzione di idoneità è binaria: un programma candidato riceve un punteggio di 1 se il dimostratore di teoremi PVS verifica che la traduzione sia corretta (ovvero, tutti gli input validi mappano in output validi che soddisfano il target dello schema), e 0 altrimenti.
   • Per mitigare la limitata familiarità dell'LLM con il PVS, il prompt include un riferimento al linguaggio ed esempi contestuali di traduzioni di schemi semplici.
3. Generazione del Codice: Una volta che un teorema è formalmente verificato, il sistema utilizza ulteriori strumenti per trasformare deterministicamente il teorema PVS verificato in codice C eseguibile, adatto per l'implementazione all'interno dell'ambiente MIoT con risorse limitate.

Contributi Chiave

• Pipeline Neuro-Simbolica: L'integrazione di una ricerca evolutiva guidata da LLM con un dimostratore di teoremi formale (PVS) per garantire che il codice sintetizzato soddisfi rigorosi requisiti strutturali.
• Caso di Studio MIoT: Una dimostrazione pratica dell'integrazione di un pulsossimetro in una rete MIoT basata su veicolo. Il sistema traduce con successo lo schema JSON personalizzato del dispositivo nel formato della risorsa FHIR Observation standard.
• Affidabilità a Basso Costo: La dimostrazione che il codice formalmente verificato può essere generato costantemente con un overhead computazionale e finanziario ridotto.

Risultati Sperimentali
Gli autori hanno condotto 10 sessioni sperimentali indipendenti, ciascuna composta da 20 generazioni su due isole evolutive, per analizzare l'integrazione del pulsossimetro.

• Tasso di Successo: Il sistema ha raggiunto un tasso di successo del 37,4% ± 22,4% (la frazione di programmi generati dall'LLM che hanno superato la verifica).
• Efficienza: Il primo teorema di successo è stato trovato in media alla Generazione 5.0. Il tempo medio per trovare il primo programma di successo è stato di 10,4 minuti, con un tempo totale di esecuzione (wall-clock time) di 42,7 minuti per esperimento.
• Costo: Il costo medio totale delle API per esperimento è stato di $0,87. Fondamentalmente, il costo sostenuto prima di trovare la prima prova di successo era solo di $0,18 (circa il 20% del budget totale).
• Prestazioni del Modello: Un ensemble di modelli (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) è stato utilizzato con pesatura dinamica tramite campionamento di Thompson. GPT-5 ha rappresentato il 33,7% delle selezioni ma ha generato il 53,5% dei programmi di successo, indicando che i modelli più grandi erano più efficaci nel generare teoremi PVS corretti.
• Convergenza: Nonostante i vari percorsi di selezione degli LLM e i fallimenti intermedi, tutti i 10 esperimenti sono confluiti in soluzioni semanticamente identiche, suggerendo che i vincoli formali dello schema FHIR siano altamente prescrittivi.

Significatività e Rivendicazioni
Il documento posiziona questo lavoro come un "primo passo" verso l'integrazione affidabile di nuovi dispositivi nelle infrastrutture sanitarie esistenti. Gli autori affermano che il loro sistema dimostra la fattibilità della generazione di codice di traduzione formalmente verificato a basso costo, garantendo che i dati strutturati tradotti dal codice generato conformino sempre al target dello schema di output.

La significatività risiede nel rispondere alla natura critica per la sicurezza dei sistemi sanitari, ancorando il potere di ragionamento degli LLM alla verifica formale, mitigando così i rischi di allucinazione e garantendo l'affidabilità senza richiedere l'esperienza di sviluppatori software umani. Gli autori dichiarano esplicitamente che il lavoro futuro comporterà l'espansione del set di dispositivi, la verifica dei componenti di rete e l'integrazione di questa fase di verifica in una pipeline completamente agentica.