본 논문은 의료 데이터의 디지털화 과정에서 발생하는 복잡성, 방대한 데이터 생성, 개인 맞춤형 치료 계획의 필요성 등의 문제점을 지적하며, 이러한 문제 해결에 양자 컴퓨팅(QC)과 양자 머신러닝(QML)이 혁신적인 발전을 가져올 수 있음을 제시합니다. QC는 더 빠르고 정확한 진단, 개인 맞춤형 치료, 향상된 신약 개발 과정을 가능하게 하여 의학 혁신을 이끌 수 있습니다. 하지만 양자 기술을 정밀 의료에 통합하는 과정에는 알고리즘 오류 및 높은 비용과 같은 어려움이 존재합니다. 본 논문에서는 형식적 방법론(formal methods)을 통해 양자 컴퓨팅의 신뢰성과 정확성을 높일 수 있음을 주장합니다. 형식적 방법론은 수학적 틀을 제공하여 양자 알고리즘의 사양, 개발, 검증을 정밀하게 수행할 수 있게 합니다. 특히 유전체 데이터 분석 분야에서 형식적 사양 언어를 활용하여 질병 관련 유전자 마커를 식별하는 양자 알고리즘의 동작과 속성을 정의하고, 모델 검증 도구를 통해 모든 가능한 상태를 체계적으로 탐색하여 알고리즘의 정확성을 검증하며, 정리 증명 기법을 통해 알고리즘이 명시된 속성을 충족함을 수학적으로 증명하고, 형식적 최적화 기법을 통해 양자 알고리즘의 효율성과 성능을 향상시킬 수 있음을 보여줍니다.
