Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

양자 컴퓨터는 복잡한 암호 해독부터 신소재 시뮬레이션에 이르기까지, 현재 가장 강력한 슈퍼컴퓨터로도 불가능한 문제들을 해결할 것을 약속합니다. 하지만 이 기계들은 믿을 수 없을 정도로 취약합니다. 열이나 진동으로부터 발생하는 아주 작은 방해만으로도 계산이 무너질 수 있습니다. 살아남기 위해 과학자들은 정보를 보호하기 위해 특수한 오류 수정 코드를 사용하는 결함 허용(fault-tolerant) 양자 컴퓨터를 구축하고 있습니다. 데이터를 단 하나의 섬세한 입자에 저장하는 대신, 이 시스템은 정보를 여러 입자에 분산시키고, 끊임없이 실수를 확인하고 수정합니다. 과제는 번역에 있습니다. 어떻게 하면 고수준의 알고리즘을 이 오류 수정 기계가 실제로 수행할 수 있는 특정 저수준 연산으로 변환할 것인가 하는 점입니다.

이러한 미래형 기계들의 표준적인 방법 중 하나는 격자 수술(lattice surgery)이라 불리는 기술을 포함합니다. 컴퓨터의 메모리를 나타내는 커다란 천 조각을 상상해 보십시오. 계산을 수행하기 위해 단순히 스위치를 올리는 것이 아니라, 이 천의 조각들을 정밀한 패턴으로 엮고 떼어내야 합니다. 이 바느질은 물리적인 실이 아니라 입자 집단들의 공동 측정입니다. 컴퓨터는 이 집단들이 서로 어떻게 관계를 맺는지 측정하고, 그 결과를 단순한 비트 데이터로 기록한 다음, 그 데이터를 사용하여 다음 행동을 결정합니다. '파울리 곱 측정(Pauli-product measurement)'이라고 알려진 이 과정은 이러한 미래 기계들의 근본적인 언어입니다. 문제는 인간이 설계한 알고리즘을 이 언어로 번역하는 데 사용되는 소프트웨어 도구들이 검증되지 않았다는 점입니다. 만약 컴파일러가 번역 과정에서 실수를 한다면 전체 계산이 실패할 수 있으며, 과정이 매우 복잡하기 때문에 어디에서 오류가 발생했는지 알기가 어렵습니다.

캘리포니아 대학교 로스앤젤레스(UCLA)의 연구팀은 수학적으로 번역이 올바름을 증명하는 시스템을 개발함으로써 이 간극을 해결했습니다. 그들은 측정 기반 프로그램을 위한 새로운 언어를 특별히 개발했으며, 표준 양자 회로를 이 언어로 번환하는 컴파일러를 구축했습니다. 결정적으로, 그들은 단순히 코드를 작성한 것이 아니라, '린(Lean)'이라는 형식 검증 도구를 사용하여 자신들의 컴파일러가 원래의 알고리즘의 동작을 보존한다는 엄격한 수학적 증명을 구축했습니다. 이는 컴파일러가 수행하는 모든 단계마다, 출력이 입력이 의도했던 결과와 정확히 일치함을 보장하는 인증서가 존재함을 의미하며, 이는 결과의 특정 확률까지도 포함합니다.

연구진은 '로어링(lowering, 하향 변환)'과 '최적화'라는 두 가지 주요 과제에 집중했습니다. 로어링은 회전이나 논리 게이트와 같은 표준 양자 게이트를 가져와, 격자 수술 하드웨어가 요구하는 측정 및 수정의 순서로 세분화하는 과정입니다. 최적화는 이 과정을 더 빠르고 효율적으로 만들기 위해 측정을 재배열하는 것을 포함합니다. 그들은 자신들의 컴파일러가 회로를 가져와 측정 명령어로 번역한 다음, 최종 결과에 영향을 주지 않으면서 해당 명령어들을 융합하고 재정렬하는 규칙을 적용할 수 있음을 증명했습니다. 또한, 그들은 컴파일러가 특정 유형의 계산에 필요한 특수 자원인 '매직 상태(magic states)'를 올바르게 처리하는지, 그리고 외부 세계로부터 개인적인 측정 결과는 숨기면서 공적인 결과는 접근 가능하도록 유지하는지를 검증했습니다.

연구팀이 35개의 작은 양자 회로 세트에 대해 이 시스템을 테스트했을 때, 결과는 구체적이고 측정 가능했습니다. 검증된 컴파일러는 모든 유효한 입력을 성공적으로 번역하여 번역이 올바름을 확인하는 인증서를 생성했습니다. 성능 측면에서, 그들이 검증한 최적화 기술은 이 회로들을 실행하는 데 필요한 논리적 측정 라운드 수를 중간값 기준으로 17.9% 감소시켰습니다. 특정 회로의 경우 그 감소 폭은 거의 29%에 달할 정도로 더 높았습니다. 이러한 감소는 중요한데, 왜냐로 인해 이 결함 허용 시스템에서는 모든 측정 라운드가 시간과 자원을 소모하기 때문입니다. 라운드 수를 줄이는 것은 곧 더 빠르고 효율적인 컴퓨터로 직결됩니다.

연구팀은 또한 완벽한 수학적 회전을 정확하게 구축할 수 없을 때 필요한 근사 계산을 처리하는 방법도 보여주었습니다. 그들은 이러한 근사로 인해 발생하는 오차를 제한하는 방법을 만들어, 최종 결과가 사용자가 정의한 한계 내에 머물도록 보장했습니다. 그들은 목록에 있는 후보들 중에서 최선의 버전의 회로를 선택하여, 오차 한계를 준수하면서도 가장 적은 자원을 사용하는 회로를 선택할 수 있음을 보여주었습니다. 이 선택 과정 역시 검증되었으며, 이는 컴퓨터가 실수로 너무 부정확하거나 너무 느린 회로를 선택하지 않도록 함을 의미합니다.

이 연구는 컴파일러가 작동하기를 바라는 것에서, 컴파일러가 작동한다는 것을 아는 것으로의 전환을 의미합니다. 전체 컴파일 파이프라인에 대한 기계 검증된 증명을 구축함으로써, 연구진은 대규모 양자 컴퓨팅으로 가는 경로에서 주요 불확실성의 원인을 제거했습니다. 그들은 복잡한 알고리즘을 가져와 오류 수정 하드웨어의 특정 언어로 번역하고, 논리가 그대로 유지된다는 수학적 보장을 유지하면서 속도를 위해 최적화하는 것이 가능하다는 것을 보여주었습니다. 이 시스템은 최대 433개의 큐비트를 가진 회로를 성공적으로 처리하며, 이러한 수준의 검증이 상당한 규모의 문제로 확장될 수 있음을 입증했습니다. 비록 이 회로들을 실행할 물리적 하드웨어는 여전히 개발 중이지만, 이 소프트웨어 기초는 기계가 도착했을 때 전달될 명령어가 신뢰할 수 있음을 보장합니다.