양자 증명 시스템과 호어 논리 연결

요약

양자 프로그램의 형식적 검증은 전문적인 증명 시스템 때문에 큰 어려움이 있습니다. 본 연구는 Qafny 양자 증명 시스템을 호어 논리로 완전히/건전하게 번역하는 임베딩 방법을 제시합니다. 이를 통해 기존 클래식 자동 검증기(Dafny 등)를 활용하여 전용 양자 증명 인프라의 필요성을 제거할 수 있습니다.

핵심 포인트

• 양자 프로그램은 런타임 테스트가 불가능해 형식적 검증이 필수입니다.
• Qafny 시스템을 호어 논리로 완전히/건전하게 번역하는 임베딩 방법을 제시했습니다.
• 기존 클래식 자동 검증기를 양자 코드에 노출시켜 전용 인프라 필요성을 제거합니다.
• 이 방법은 기존 Qafny-Dafny 컴파일 과정의 정확성 논증을 보완합니다.