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

技術要約：医療IoTにおける構造化データ変換のための形式検証済みコード合成

問題提起
新規の医療機器を既存の医療IoT（MIoT）ネットワークに統合する際には、人間のソフトウェア開発の専門知識が利用できない場合、特に大きな課題が生じる。大規模言語モデル（LLM）は強力なコード合成能力を提供する一方で、ハルシネーション（幻覚）や微細な脆弱性を引き起こす可能性があり、安全性に敏感なヘルスケア領域においては信頼性に欠ける。本研究が取り組む核心的な問題は、人間による検証（スケール化の観点から困難な場合が多い）を介することなく、デバイス固有のフォーマット（例：カスタムJSONスキーマ）を標準的な相互運用フォーマット（例：FHIR：Fast Healthcare Interoperability Resources）へと変換する、信頼できる翻訳コードを自動生成する必要性である。

手法
著者らは、LLMと形式検証を統合して「正当性による構成（correct-by-construction）」のコードを合成するニューロ・シンボリック・アーキテクチャを提案している。このシステムは、オープンソースの進化型コード最適化フレームワークであるShinkaEvolveに基づいている。パイプラインは以下のように動作する：

1. LLMを用いた進化論的探索： システムは、LLMをオペレータとして用いるマルチアイランド進化アルゴリズムを採用している。ランダムな変異の代わりに、LLMは親プログラム、インスピレーションとなるプログラム、およびそれらの適合度（fitness score）を含むプロンプトに基づき、意味のあるプログラムの編集、書き換え、または変異を提案する。
2. 適合度関数としての形式検証： 信頼性を確保するため、システムは評価器として定理証明器である**Prototype Verification System (PVS)**を使用する。LLMは、入力JSONスキーマから出力JSONスキーマへのマッピングを定義するPVSのドメイン固有言語（DSL）を用いた翻訳定理を生成するよう求められる。
   • 適合度はバイナリ（二値）である。候補となるプログラムは、すべての有効な入力が有効な出力（ターゲットとなるスキーマを満たすもの）にマッピングされることがPVS定理証明器によって検証された場合にのみ、スコア1を受け取り、そうでなければ0となる。
   • PVSに対するLLMの習熟度の低さを軽減するため、プロンプトには言語のリファレンスと、単純なスキーマ変換のインコンテキストな例が含まれる。
3. コード生成： 形式検証された定理が得られた後、システムは追加のツールを用いて、検証済みのPVS定理を、リソース制約のあるMIoT環境へのデプロイに適した実行可能なC言語コードへと決定論的に変換する。

主な貢献

• ニューロ・シンボリック・パイプライン： LLM駆動の進化論的探索と形式定理証明器（PVS）を統合し、合成されたコードが厳格な構造的要件を満たすことを保証する。
• MIoTケーススタディ： パルスオキシメータを車両ベースのMIoTネットワークに統合する実用的なデモンストレーション。システムは、デバイスのカスタムJSONスキーマを標準のFHIR Observationリソース形式へと正常に変換した。
• 低コストな信頼性： 形式検証されたコードが、低い計算コストおよび財務的オーバーヘッドで一貫して生成可能であることを示した。

実験結果
著者らは、パルスオキシメータの統合を分析するために、2つの進化アイランドにわたる20世代からなる10回の独立した実験を実施した。

• 成功率： システムは37.4% ± 22.4%（検証を通過したLLM生成プログラムの割合）の成功率を達成した。
• 効率性： 最初の成功した定理は平均して第5世代で見つかった。最初の成功プログラムが見つかるまでの平均時間は10.4分であり、実験あたりの総実時間は42.7分であった。
• コスト： 実験あたりの平均総APIコストは0.87ドルであった。極めて重要な点として、最初の証明が見つかるまでに発生したコストはわずか0.18ドル（総予算の約20%）であった。
• モデルの性能： Thompsonサンプリングによる動的な重み付けを用いて、アンサンブルモデル（GPT-5, GPT-5-mini, o4-mini, GPT-5-nano）が使用された。GPT-5は選択の33.7%を占めたが、成功したプログラムの**53.5%**を生成しており、より大規模なモデルが正しいPVS定理の生成においてより効果的であることを示している。
• 収束性： LLMの選択経路や中間段階での失敗の差異にもかかわらず、10個の実験すべてが意味的に同一の解に収束した。これは、FHIRスキーマの形式的制約が非常に規定的な性質を持っていることを示唆している。

意義と主張
本論文は、この研究を、既存のヘルスケア・インフラストラクチャへの新規デバイスの信頼できる自動統合に向けた「第一歩」と位置づけている。著者らは、本システムが、低コストで形式検証された翻訳コードを生成できることを実証しており、これにより、生成されたコードによって翻訳される構造化データが常にターゲットとなる出力スキーマに適合することを保証できると主張している。

その意義は、LLMの推論能力を形式検証によって接地（グラウンディング）させることで、ハルシネーションのリスクを軽減し、人間のソフトウェア開発の専門知識を必要とせずに信頼性を確保するという、ヘルスケアシステムの安全性が極めて高い性質に対処している点にある。著者らは、今後の課題として、デバイスセットの拡張、ネットワークコンポーネントの検証、およびこの検証ステージを完全なエージェンティック・パイプラインへと統合することを明言している。