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

Motivation

• Known: LLM 기반 code synthesis와 evolutionary algorithm(예: ShinkaEvolve)을 결합하여 코드 최적화 및 과학적 발견을 수행하는 연구가 활발히 진행되어 왔으며, formal verification은 생성된 코드의 정확성을 검증하는 원칙적 프레임워크로 알려져 있다. 또한 HL7 FHIR와 같은 표준을 통한 헬스케어 데이터 상호운용성 연구도 존재한다.
• Gap: 기존 LLM 기반 code synthesis는 hallucination이나 미묘한 취약점을 유발할 수 있어 safety-critical한 의료 도메인에서 신뢰성이 부족하며, 특히 새로운 의료기기를 MIoT 네트워크에 통합할 때 별도의 인간 소프트웨어 개발 전문성 없이 안전하게 자동화할 수 있는 방법이 부재했다.
• Why: 의료 데이터 변환 코드에 오류가 있으면 임상적으로 수용 불가능하거나 안전하지 않은 결과를 초래할 수 있으므로, LLM이 생성한 코드를 형식적으로 검증하여 신뢰성을 보장하는 것은 안전이 critical한 헬스케어 자동화 확산에 중요한 의미를 가진다.
• Approach: ShinkaEvolve 기반의 LLM-powered evolutionary code synthesis 파이프라인에 Prototype Verification System(PVS) 정리 증명기를 fitness evaluator로 통합하여, 입력/출력 JSON schema 간 변환이 형식적으로 검증된 경우에만 유효한 것으로 판단하는 neuro-symbolic 아키텍처를 제안한다.

Achievement

Figure 2. Selection and success rate of LLMs in the ensemble.

1. Neuro-symbolic 코드 합성 파이프라인 제안: LLM 기반 evolutionary search(ShinkaEvolve)와 PVS 정리 증명기를 결합하여, 생성된 JSON schema 변환 코드가 사전 정의된 requires/ensures 조건을 만족함을 형식적으로 보장하는 시스템을 구축했다.
2. 실제 의료기기 통합 사례 연구: pulse oximeter의 커스텀 JSON schema를 FHIR 표준 포맷으로 변환하는 실제 사례를 통해 시스템의 실용성을 검증했다.
3. 정량적 성능 검증: 10회의 독립 실행(2개 island, 20세대)을 통해 시스템이 낮은 비용으로 일관되게 올바른(형식 검증된) 변환을 생성함을 실험적으로 입증했다.
4. 실행 가능한 코드로의 변환 도구 제공: PVS DSL로 형식 검증된 정리를 MIoT 환경에서 실제로 실행 가능한 C 코드로 결정론적으로 변환하는 추가 툴링을 개발했다.

How

Figure 1. Overview of our proposed system. A user provides an

• ShinkaEvolve의 multi-island evolutionary loop를 사용하여 parent program, LLM ensemble sample, K개의 inspiration program을 선택하고 이를 프롬프트로 제공하여 LLM이 편집/재작성/변이를 통해 새로운 후보 solution을 생성하도록 함.
• PVS를 evaluator로 사용하여 생성된 PVS DSL 변환 이론(theorem)이 requires/ensures 형식의 correctness 조건(Listing 1)을 만족하는지 검증하고, 이를 binary fitness(0 또는 1)로 사용.
• PVS DSL이 LLM에 낯설다는 문제를 완화하기 위해 PVS language reference와 in-context 예제 변환을 프롬프트에 추가로 제공.
• 검증된 PVS theorem을 별도 툴링을 통해 결정론적으로 C 코드로 변환하여 MIoT 환경에서 실제 실행 가능하도록 함.
• pulse oximeter의 JSON schema와 FHIR schema, 초기 skeleton program(빈 JSON dict 반환)을 입력으로 하여 10회의 독립 실험(2 island, 20 generation)을 수행해 성공률 및 자원 비용을 분석.

Originality

• LLM 기반 evolutionary code synthesis에 정리 증명기(PVS)를 fitness function으로 직접 통합하여, post-hoc 필터가 아닌 evolutionary search의 목적함수 자체로 형식 검증을 사용하는 접근이 참신하다.
• JSON schema 간 변환을 PVS DSL(JSON 데이터 라이브러리 jsltlib)로 표현 가능하도록 어댑테이션하여, 기존에 일반 소프트웨어 검증에 쓰이던 정리 증명기를 구조화된 데이터 변환 검증이라는 새로운 응용 영역에 적용했다.
• 실제 임상 IoT 배포 시나리오(차량 기반 모바일 케어를 위한 신규 의료기기 통합)를 사례 연구로 삼아 실용성과 안전성 요구를 동시에 다루는 실제적 문제 설정을 제시했다.

Limitation & Further Study

• 단일 사례 연구(pulse oximeter 하나)만을 다루고 있어, 더 복잡하거나 다양한 종류의 의료기기 스키마 변환에 대한 일반화 가능성이 검증되지 않았다.
• PVS DSL이 LLM에 낯설다는 근본적 한계가 in-context 예제와 language reference 제공만으로 충분히 해결되었는지, 더 복잡한 schema에서도 확장 가능한지 불분명하다.
• binary fitness(0/1)만을 사용하는 방식이 탐색 효율성 측면에서 제한적일 수 있으며, 부분적으로 올바른 후보에 대한 세밀한 guidance가 부족할 수 있다.
• 형식 검증이 requires/ensures 조건의 정의(즉, output_compliant?와 ensures 함수)의 완전성과 정확성에 크게 의존하는데, 이러한 명세 자체의 오류나 불완전성에 대한 논의가 부족하다.
• 후속 연구로 더 복잡한 의료기기·스키마, semantic correctness(단순 syntactic schema 준수를 넘어선 임상적 의미 보존)에 대한 검증 확장이 필요하다.

Evaluation

총평: LLM 기반 evolutionary code synthesis와 formal verification을 결합해 안전이 critical한 의료 IoT 데이터 변환 문제를 실용적으로 해결한 흥미롭고 시의적절한 연구이나, 단일 사례 연구에 기반한 초기 단계의 workshop paper로서 일반화 가능성에 대한 추가 검증이 필요하다.