앤트로픽, 비공개 AI로 18년 묵은 양자컴퓨터 난제 증명

AI 물리학 스타트업 PSI(Physical Superintelligence)가 11월 6일 2008년부터 풀리지 않던 양자컴퓨팅 난제 아론슨-암바이니스 추측(Aaronson-Ambainis conjecture)을 증명했다고 발표했다. 증명에는 앤트로픽(Anthropic)의 비공개 AI 모델을 넣은 연구 시스템을 썼다. 수학 증명을 컴퓨터로 검증하는 린(Lean)으로 확인도 마쳤다고 PSI는 밝혔다.

양자컴퓨터는 양자역학 성질을 이용해 기존 컴퓨터로는 시간이 엄청나게 걸리는 계산을 빠르게 처리할 것으로 기대를 모은다. 수학자 피터 쇼어(Peter Shor)가 1994년 고안한 쇼어 알고리즘이 대표적이다. 큰 정수의 소인수분해를 기존 방법보다 훨씬 빠르게 해내는 양자 알고리즘이다.

다만 양자컴퓨터가 압도적인 성능을 내려면 풀려는 문제에 특정한 규칙성이나 구조가 있어야 하는지는 의문으로 남아 있었다. 쇼어 알고리즘도 숫자에 숨은 주기적 규칙성을 활용한다.

◇ 양자 가속에 규칙성 필요한지 가리는 추측=계산기 과학자 스콧 아론슨(Scott Aaronson)과 안드리스 암바이니스(Andris Ambainis)가 2008년 내놓은 아론슨-암바이니스 추측은 이 물음을 수학적으로 밝히려는 추측이다. 추측이 맞다면 무작위 입력 대부분에서 양자컴퓨터는 기존 컴퓨터보다 데이터 조회 횟수를 지수적으로 줄여 계산을 끝낼 수 없다. 양자컴퓨터로 극적인 속도 향상을 얻으려면 문제에 숨은 특별한 규칙성이 있어야 한다는 뜻이다.

PSI는 자체 개발한 AI 연구 시스템으로 이 추측에 도전했다. 시스템에는 앤트로픽이 만든 비공개 AI 모델이 들어 있다. PSI 연구진이 문제를 설정하고 자체 연산 환경에서 돌렸다.

PSI에 따르면 AI 연구 시스템은 가동 사흘째에 추측의 완전한 증명을 찾아냈다. 이후 관련 수학 문제를 연구하며 증명을 2번 다듬어 최종 증명을 완성했다.

◇ 린으로 검증 마쳐=수학 증명은 결론이 맞는지뿐 아니라 결론에 이르는 논리에 오류가 없는지도 따져야 한다. AI가 쓴 복잡한 증명은 그럴듯한 설명 속에 오류가 숨어 있을 수 있어 엄밀한 검증이 더 중요하다.

PSI는 정리 증명 보조 시스템 린 4로 증명을 컴퓨터가 확인할 수 있는 형식으로 옮겼다. PSI가 공개한 자료를 보면 린 증명은 미완성 부분이나 새 공리 추가 없이 완성됐다. 서로 독립된 검증 프로그램 2종으로도 확인했다. PSI는 깃허브(GitHub)에 논문과 린 소스코드, 검증 절차와 결과 기록을 공개했다.

전문가 반응도 나왔다. 양자계산을 연구하는 헨리 유엔(Henry Yuen)은 양자컴퓨터의 지수적 가속에 규칙성이 필요한지라는 아름다운 문제가 풀렸다고 소개했다. 수학자 파타 이바니슈빌리(Paata Ivanisvili)는 증명이 맞다면 큰 성과라고 평가했다.

PSI에 따르면 2026년 8월 이 추측의 특수한 경우를 푼 스탠퍼드대(Stanford University) 연구진도 이번 증명을 확인했다. 연구진은 전문가용으로 내용을 간추린 해설을 쓰고 있다. PSI는 양자컴퓨팅에는 아직 많은 수수께끼가 남아 있지만 이제 하나가 줄었다고 밝혔다. 관련 내용은 이곳에서 확인할 수 있다.