用于医疗物联网中结构化数据翻译的形式化验证代码合成
用于医疗物联网中结构化数据翻译的形式化验证代码合成
摘要： 本文提出了一种基于 LLM（大语言模型）的进化式代码合成系统，用于医疗物联网场景中的结构化数据翻译。该领域的一个关键挑战是确保合成代码的可靠性与可信度。为此，我们在代码合成流程中集成了一个形式化验证步骤，以保证任何生成的代码都必定满足预定义需求。具体而言，我们通过一个案例研究展示如何将新型设备（脉搏血氧仪）集成到现有设备网络中。我们的系统生成一个经过形式化验证的翻译器，用于在该设备的 JSON 模式与整个系统使用的 FHIR（快速医疗互操作性资源）格式之间进行转换。这一形式化验证阶段确保由生成代码翻译的结构化数据始终符合目标输出模式。我们提供了一系列实验结果，表明我们的系统能够以低成本持续生成正确的翻译。