医疗物联网中结构化数据翻译的正式验证代码合成

在这项工作中，我们提出了一个 LLM 支持的进化代码合成系统，用于医疗物联网设置中的结构化数据转换。该领域的一个关键挑战是确保合成的代码是值得信赖和可靠的。为此，我们将形式验证步骤集成到代码合成管道中，以确保任何生成的代码都满足预定义的要求。我们特别介绍了将新型设备（脉搏血氧计）集成到现有设备网络中的案例研究。我们的系统在设备的 JSON 模式和更广泛的系统使用的快速医疗互操作性资源 (FHIR) 格式之间生成经过正式验证的转换。此形式验证阶段可确保由生成的代码转换的结构化数据始终位于目标输出模式中。我们提供了一组实验结果，证明我们的系统能够以低成本持续生成正确的翻译。