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

Technische Samenvatting: Formeel Verifieerde Codesynthese voor Gestructureerde Datatranslatie in een Medical Internet of Things

Probleemstelling
De integratie van nieuwe medische apparaten in bestaande Medical Internet of Things (MIoT)-netwerken brengt aanzienlijke uitdagingen met zich mee, vooral wanneer expertise op het gebied van menselijke softwareontwikkeling niet beschikbaar is. Hoewel Large Language Models (LLMs) krachtige mogelijkheden bieden voor codesynthese, zijn ze gevoelig voor hallucinaties en subtiele kwetsbaarheden, wat hen onbetrouwbaar maakt voor veiligheidskritische zorgdomeinen. Het kernprobleem dat wordt aangeporen is de noodzaak om automatisch betrouwbare, betrouwbare translatiecode te genereren die gegevens van apparaatspecifieke formaten (bijv. aangepaste JSON-schema's) converteert naar gestandaardiseerde interoperabiliteitsformaten (bijv. Fast Healthcare Interoperability Resources of FHIR) zonder handmatige verificatie, wat op schaal vaak onhaalbaar is.

Methodologie
De auteurs stellen een neuro-symbolische architectuur voor die LLMs integreert met formele verificatie om correct-door-constructie code te synthetiseren. Het systeem is gebouwd op ShinkaEvolve, een open-source evolutionair framework voor code-optimalisatie. De pipeline werkt als volgt:

1. Evolutionaire Zoektocht met LLMs: Het systeem maakt gebruik van een multi-island evolutionair algoritme waarbij LLMs als operatoren fungeren. In plaats van willekeurige mutaties, stellen LLMs semantisch betekenisvolle programma-edits, herschrijvingen of mutaties voor op basis van een prompt die ouderprogramma's, "inspiratie"-programma's en hun fitnessscores bevat.
2. Formele Verificatie als Fitnessfunctie: Om betrouwbaarheid te garanderen, gebruikt het systeem de Prototype Verification System (PVS), een stellingbewijzer (theorem prover), als evaluator. De LLM krijgt de taak om een translatie-stelling in de PVS Domain-Specific Language (DSL) te genereren die een invoer JSON-schema naar een uitvoer JSON-schema mapt.
   • De fitnessfunctie is binair: een kandidaat-programma ontvangt een score van 1 als de PVS-stelling bewijst dat de translatie correct is (d.w.z. alle geldige inputs naar geldige outputs mappen die voldoen aan het doel-schema), en 0 anders.
   • Om de beperkte bekendheid van de LLM met PVS te mitigeren, bevat de prompt een taalreferentie en in-context voorbeelden van eenvoudige schema-translaties.
3. Codegeneratie: Zodra een stelling formeel is geverifieerd, maakt het systeem gebruik van aanvullende tooling om de geverifieerde PVS-stelling deterministisch te transformeren naar uitvoerbare C-code, geschikt voor implementatie binnen de door middelen beperkte MIoT-omgeving.

Belangrijkste Bijdragen

• Neuro-Symbolische Pipeline: De integratie van een LLM-gestuurde evolutionaire zoektocht met een formele stellingbewijzer (PVS) om te garanderen dat gesynthetiseerde code voldoet aan strikte structurele vereisten.
• MIoT Casestudy: Een praktische demonstratie van de integratie van een pulsoximeter in een voertuig-gebaseerd MIoT-netwerk. Het systeem vertaalt succesvol het aangepaste JSON-schema van het apparaat naar de standaard FHIR Observation resource.
• Lage-Kosten Betrouwbaarheid: De demonstratie dat formeel geverifieerde code consistent kan worden gegenereerd met lage computationele en financiële overhead.

Experimentele Resultaten
De auteurs voerden 10 onafhankelijke experimentele runs uit, elk bestaande uit 20 generaties over twee evolutionaire eilanden, om de integratie van de pulsoximeter te analyseren.

• Succespercentage: Het systeem bereikte een succespercentage van 37,4% ± 22,4% (het deel van de door LLM gegenereerde programma's dat de verificatie passeerde).
• Efficiëntie: De vroegste succesvolle stelling werd gemiddeld gevonden in Generatie 5.0. De gemiddelde tijd om het eerste succesvolle programma te vinden was 10,4 minuten, met een totale wandkloktijd van 42,7 minuten per experiment.
• Kosten: De gemiddelde totale API-kosten per experiment waren $0,87. Cruciaal is dat de kosten die werden gemaakt voordat het eerste succesvolle bewijs werd gevonden, slechts $0,18 bedroegen (ongeveer 20% van het totale budget).
• Modelprestaties: Een ensemble van modellen (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) werd gebruikt met dynamische weging via Thompson sampling. GPT-5 was verantwoordelijk voor 33,7% van de selecties maar genereerde 53,5% van de succesvolle programma's, wat aangeeft dat grotere modellen effectiever waren in het genereren van correcte PVS-stellingen.
• Convergentie: Ondanks variërende LLM-selectiepaden en tussenliggende mislukkingen, convergeerden alle 10 de experimenten naar semantisch identieke oplossingen, wat suggereert dat de formele restricties van het FHIR-schema zeer voorschrijvend zijn.

Betekenis en Claims
Het artikel positioneert dit werk als een "eerste stap" naar de betrouwbare automatische integratie van nieuwe apparaten in bestaande gezondheidszorginfrastructuur. De auteurs beweren dat hun systeem aantoont dat het genereren van formeel geverifieerde translatiecode tegen lage kosten haalbaar is, waardoor wordt gegarandeerd dat de gestructureerde gegevens die door de gegenereerde code worden getranslateerd, altijd voldoen aan het doel-schema.

De betekenis ligt in het adresseren van het veiligheidskritische karakter van gezondheidssystemen door de redeneerkracht van LLMs te funderen in formele verificatie, waardoor de risico's van hallucinaties worden gemitigeerd en betrouwbaarheid wordt gegarandeerd zonder dat er menselijke expertise op het gebied van softwareontwikkeling nodig is. De auteurs geven expliciet aan dat toekomstig werk zal bestaan uit het uitbreiden van de set apparaten, het verifiëren van netwerkcomponenten en het integreren van deze verificatiefase in een volledig agentische pipeline.