用形式化验证确保医疗物联网数据翻译代码可靠
Formally Verified Code Synthesis for Structured Data Translation in a Medical Internet of Things
- LLM结合进化算法生成代码，再通过形式化验证保证正确性
- 成功将血氧仪JSON数据转为FHIR格式，且转换结果始终符合目标结构
- 适合医疗系统开发者与需要高可信代码的场景
本文提出一种基于大语言模型的进化式代码生成系统，用于医疗物联网中的结构化数据翻译。该领域关键挑战在于确保生成代码的可信与可靠。为此，我们在代码生成流程中引入形式化验证环节，确保生成代码始终满足预设需求。以新型血氧仪设备接入现有系统为例，系统自动生成从其JSON schema到广义医疗互操作性资源（FHIR）格式的转换代码，并通过形式化验证保证翻译后的结构化数据始终符合目标输出模式。实验结果表明，该系统能以低成本持续生成正确代码。
原文摘要 · Abstract (English)
In this work we present a LLM powered, evolutionary code synthesis system for structured data translation in a Medical Internet of Things settings. A key challenge in this domain is ensuring that the synthesized code is trustworthy and reliable. To this end, we integrate a formal verification step into our code synthesis pipeline to ensure that any generated code is guaranteed to satisfy predefined requirements. In particular, we present a case study of integrating a novel device (a pulse oximeter) into the existing network of devices. Our system generates a formally verified translation between the device's JSON schema and the Fast Healthcare Interoperability Resources (FHIR) format used by the wider system. This formal verification stage ensures structured data translated by the generated code will always be in the target output schema. We provide a set of experimental results which demonstrate that our system is able to consistently generate correct translation at low cost.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。