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

기술 요약: 의료 사물 인터넷(MIoT) 내 구조화된 데이터 변환을 위한 형식 검증 기반 코드 합성

문제 정의
새로운 의료 기기를 기존 의료 사물 인터넷(MIoT) 네트워크에 통합하는 과정은, 특히 인간의 소프트웨어 개발 전문 지식을 활용할 수 없는 상황에서 상당한 어려움을 초래한다. 대규모 언어 모델(LLM)은 강력한 코드 합성 능력을 제공하지만, 환각(hallucination) 현상과 미묘한 취약점에 노-출되기 쉬워 안전이 필수적인 의료 분야에서는 신뢰하기 어렵다. 본 연구가 다루는 핵심 문제는, 수동 검증이 규모 면에서 불가능한 상황에서 장치 특화 형식(예: 커스텀 JSON 스키마)을 표준 상호운용성 형식(예: FHIR - Fast Healthcare Interoperability Resources)으로 변환하는 신뢰할 수 있는 변환 코드를 자동으로 생성해야 할 필요성이다.

방법론
저자들은 LLM과 형식 검증(formal verification)을 결격하여 '올바름이 설계 단계부터 보장되는(correct-by-construction)' 코드를 합성하는 뉴로-심볼릭(neuro-symbolic) 아키텍처를 제안한다. 이 시스템은 오픈 소스 진화적 코드 최적화 프레임워크인 ShinkaEvolve를 기반으로 구축되었다. 파이프라인의 작동 방식은 다음과 같다:

1. LLM을 이용한 진화적 탐색: 시스템은 LLM이 연산자(operator) 역할을 수행하는 멀티 아일랜드 진화 알고리즘을 채택한다. 무작위 변이 대신, LLM은 부모 프로그램, "영감을 주는(inspiration)" 프로그램, 그리고 해당 프로그램들의 적합도 점수를 포함한 프롬프트를 바탕으로 의미 있는 프로그램 편집, 재작성 또는 변이를 제안한다.
2. 적합도 함수로서의 형식 검증: 신뢰성을 보장하기 위해, 시스템은 평가기로서 **PVS(Prototype Verification System)**라는 정리 증명기(theorem prover)를 사용한다. LLM은 입력 JSON 스키마를 출력 JSON 스키마로 매핑하는 PVS의 도메인 특화 언어(DSL)로 변환 정리를 생성하는 과업을 수행한다.
   • 적합도 함수는 이진(binary) 형태이다. 후보 프로그램이 변환의 정확성을 검증(즉, 모든 유효한 입력이 타겟 스키마를 만족하는 유효한 출력으로 매핑됨)하는 PVS 정리를 통과하면 1점을 받고, 그렇지 않으면 0점을 받는다.
   • LLM의 제한된 PVS 숙련도를 완화하기 위해, 프롬프트에는 언어 참조 자료와 간단한 스키마 변환에 대한 인컨텍스트(in-context) 예시가 포함된다.
3. 코드 생성: 정리가 형식적으로 검증되면, 시스템은 추가적인 도구를 사용하여 검증된 PVM 정리를 자원 제약이 있는 MIoT 환경에 배포 가능한 실행 가능한 C 코드로 결정론적으로 변환한다.

주요 기여

• 뉴로-심볼릭 파이프라인: 합성된 코드가 엄격한 구조적 요구 사항을 충족함을 보장하기 위해 LLM 기반 진화 탐색과 형식 정리 증명기(PVS)를 통합하였다.
• MIoT 사례 연구: 차량 기반 MIoT 네트워크에 맥박 산소 측정기를 통합하는 실질적인 시연을 수행하였다. 시스템은 해당 장치의 커스텀 JSON 스키마를 표준 FHIR Observation 리소스로 성공적으로 변환하였다.
• 저비용 신뢰성: 형식적으로 검증된 코드가 낮은 계산 비용 및 재정적 오버헤드로 일관되게 생성될 수 있음을 입증하였다.

실험 결과
저자들은 맥박 산소 측정기 통합을 분석하기 위해, 2개의 진화 아일랜드에서 20세대를 수행하는 10회의 독립적인 실험 실행을 실시하였다.

• 성공률: 시스템은 **37.4% ± 22.4%**의 성공률(검증을 통과한 LLM 생성 프로그램의 비율)을 달了했다.
• 효율성: 가장 빠른 성공적인 정리는 평균 5.0세대에서 발견되었다. 첫 번째 성공적인 프로그램을 찾는 데 걸린 평균 시간은 10.4분이었으며, 실험당 총 실제 실행 시간(wall-clock time)은 42.7분이었다.
• 비용: 실험당 평균 총 API 비용은 $0.87**였다. 결정적으로, 첫 번째 성공적인 증명을 찾기 전까지 발생한 비용은 **$0.18(전체 예산의 약 20%)에 불과했다.
• 모델 성능: 톰슨 샘플링(Thompson sampling)을 통한 동적 가중치 부여를 통해 앙상블 모델(GPT-5, GPT-5-mini, o4-mini, GPT-5-nano)을 사용하였다. GPT-5는 선택 비중이 33.7%였으나 **53.5%**의 성공적인 프로그램을 생성하였는데, 이는 더 큰 모델이 올바른 PVS 정리를 생성하는 데 더 효과적임을 나타낸다.
• 수렴성: LLM 선택 경로와 중간 실패에도 불구하고, 10개의 실험 모두 의미론적으로 동일한 솔루션으로 수렴하였다. 이는 FHIR 스키마의 형식적 제약 조건이 매우 규범적임을 시사한다.

의의 및 주장
본 논문은 이 연구를 기존 의료 인프라에 새로운 장치를 신뢰할 수 있게 자동 통합하기 위한 "첫 단계"로 규정한다. 저자들은 자신들의 시스템이 낮은 비용으로 형식 검증된 변환 코드를 생성할 수 있음을 보여주며, 이를 통해 생성된 코드가 항상 타겟 출력 스키마를 준수하도록 보장한다고 주장한다.

이 연구의 의의는 LLM의 추론 능력을 형식 검증에 결합함으로써 환각의 위험을 완화하고, 인간의 소프트웨어 개발 전문 지식 없이도 신뢰성을 확보하여 의료 시스템의 안전 필수적 특성을 해결하는 데 있다. 저자들은 향arian 작업으로 장치 세트의 확장, 네트워킹 구성 요소의 검증, 그리고 이 검증 단계를 완전한 에이전트 기반 파이프라인으로 통합하는 것을 명시하였다.