구글 딥마인드, 정리증명기로 검증한 양자 프로그램 자동 발견 공개

왜 지금 이 주제인가

구글 딥마인드와 구글 퀀텀 AI 소속 연구진이 11월 6일, LLM(거대언어모델) 에이전트가 양자 프로그램을 설계하고 그 정확성과 비용까지 정리증명기로 검증하는 연구를 arXiv에 공개했습니다. 기존에는 양자 알고리즘을 고전 컴퓨터로 검증하려면 큐비트 수가 작은 인스턴스로 제한해야 했고, 이 때문에 설계 공간 탐색과 새로운 발견의 규모가 좁았습니다. 이번 연구는 그 제약을 형식 증명으로 우회해, 핵융합이나 신약대사처럼 수천 큐비트가 필요한 실제 과학 응용에서 구체적인 자원 절감 수치를 제시했다는 점에서 눈여겨볼 만합니다.

핵심 내용

연구팀은 정리증명기 Lean 위에 양자 호어 논리(Quantum Hoare Logic) 기반 검증 라이브러리를 구축했습니다. 프로그램 사양은 전제조건·프로그램·후제조건으로 이뤄진 호어 삼중항으로 기술하고, 비용은 논리 큐비트 수(Q)와 T 게이트 수(𝒯)의 곱으로 정의합니다.

작업 방식은 이렇습니다. 연구자가 목표로 하는 정확성·비용 정리를 Lean 파일에 적어 두고 증명 자리에 임시 표시(sorry)를 남기면, LLM 에이전트 팀이 후보 프로그램과 증명을 반복적으로 개선합니다. 팀 구성은 자유로워서 단일 에이전트부터 하위 서브루틴마다 역할을 나눈 계층형 팀까지 선택할 수 있습니다. 검증된 최고 성능 해법과 재사용 가능한 보조정리는 공유 위키에 축적되고, 정기적으로 열리는 가상 학술회의에서는 아직 검증되지 않은 제안과 비판을 논의합니다. 다만 결과는 반드시 검증을 통과해야 공식으로 인정됩니다. 모든 제출물은 독립된 검증기가 목표 정리·기본 정의·허용 공리가 바뀌지 않았는지 동결된 사양과 대조해 확인합니다.

성과는 다섯 가지 과제에서 수치로 제시됐습니다.

• 병렬 Grover 탐색: 기존 최강 기준 대비 1.22배에서 1.41배 개선됐으며, 네 가지 표준 설정에서 단일 원소를 찾는 100/121개 격자점과 모든 k개 원소를 찾는 110/121개 격자점에서 더 나은 성능을 보였습니다.
• 고정소수점 arcsin 계산(25비트 입력, 오차 1.25×10⁻⁷ 이하): 비용이 1.08×10⁸에서 3.70×10⁵(Q·𝒯)로 줄어 290배 개선됐습니다.
• 핵융합 정지력(stopping power) 시뮬레이션: 5,650 논리 큐비트·5.42×10¹⁵(Q·𝒯)에서 4,374 논리 큐비트·4.98×10¹⁴(Q·𝒯)로 10.9배 개선됐습니다. 전자를 실공간 격자로 바꿔 파울리 배제 원리를 활용한 것이 핵심이었습니다.
• 비(非)보른-오펜하이머 동역학 시뮬레이션(분자 C₂₃H₂₀N₃O): 4.98×10¹⁵(Q·𝒯)에서 6,057 시스템 큐비트·6.16×10¹⁴(Q·𝒯)로 8.08배 개선됐습니다.
• 약물대사 관련 Cytochrome P450 Compound I 시뮬레이션: 481 논리 큐비트·1.09×10¹²(Q·𝒯)에서 333 논리 큐비트·4.37×10¹¹(Q·𝒯)로 2.49배 개선됐습니다.

연구팀은 비보른-오펜하이머 사례에서 개선분의 기여를 분해했는데, 팀 내부 아이디어가 61퍼센트, 다른 팀과의 위키 공유가 15퍼센트, 학술회의에서의 교환이 24퍼센트를 차지했습니다. Cytochrome P450 사례에서는 다른 팀 기여 비중이 63퍼센트로 더 높았습니다.

의미와 한계

이 연구는 양자 알고리즘 설계에서 사람이 수천 년치 협업으로 해내던 최적화 작업 일부를, 형식 검증이 보장된 상태로 에이전트 팀에 맡길 수 있음을 보여줍니다. 특히 증명이 자동으로 따라붙기 때문에 결과를 신뢰할 수 있다는 점이 기존의 휴리스틱 기반 탐색과 다릅니다.

다만 연구팀 스스로 분명한 한계를 짚었습니다. 이번에 도달한 시뮬레이션도 여전히 초기 내결함 양자컴퓨터가 가질 것으로 예상되는 자원보다 훨씬 많은 자원을 요구하며, 실제 하드웨어에 닿으려면 추가로 자릿수 단위의 개선이 더 필요합니다. 또한 에이전트는 주어진 사양을 벗어나 최적화할 수 없으므로, 좋은 사양을 고르는 일 자체는 여전히 사람의 몫으로 남습니다. 예를 들어 비보른-오펜하이머 사례의 사양은 교환 대칭을 위반하는, 물리적으로 불가능한 입력 상태에 대해서도 정확성을 요구하도록 짜여 있어 개선 여지가 있고, Cytochrome P450 사례는 특정 인수분해 방식을 고정해 더 발전된 표현 방법을 배제하고 있습니다. 연구팀은 향후 오류 정정 코드와 큐비트 라우팅, 물리적 배치까지 형식 사양을 확장하고, 큐비트 수가 더 제약이 큰 초기 머신 사정에 맞춰 T 게이트 비용과 큐비트 수를 다르게 최적화하는 과제를 남겨 뒀습니다.

한 줄 정리

구글 딥마인드가 LLM 에이전트와 정리증명기를 결합해 핵융합·신약대사용 양자 프로그램의 자원 소모를 최대 290배까지 줄이면서 정확성까지 자동으로 증명해 냈습니다.