2008년부터 풀리지 않던 양자 컴퓨팅 이론 문제를 AI가 증명했다는 발표가 공개됐다. 미국 AI 연구 기업 PSI(Physical Superintelligence)는 11월 6일 연구 페이지에서 자체 연구 시스템이 공개되지 않은 앤트로픽 모델을 이용해 ‘아론슨-암바이니스 추측’을 증명했다고 밝혔다. 이 추측은 양자 컴퓨터가 무작위로 주어진 입력 문제에서 기존 컴퓨터보다 얼마나 빨라질 수 있는지와 관련된 이론 문제다. AI가 수학 증명과 논문 초안, 형식 검증까지 맡은 사례라는 점에서 연구 현장의 AI 활용 범위를 보여 준다.

2008년부터 미해결, 실행 3일째 완성된 증명

PSI는 연구 페이지 첫 문장에서 “아론슨-암바이니스 추측은 이제 증명된 명제가 됐다(The Aaronson-Ambainis conjecture is now a theorem)”고 밝혔다. 이 추측은 컴퓨터과학자 스콧 아론슨과 안드리스 암바이니스가 제기한 뒤 2008년부터 풀리지 않은 문제다.

PSI에 따르면, 연구 시스템은 실행 3일째에 완전한 증명을 완성했다. 시스템은 이후 결과를 두 차례 개선했고, 수학 증명을 컴퓨터로 검사하는 도구 린(Lean)이 최종 증명을 통과시켰다. 증명은 결과를 크게 좌우하는 입력 비트가 적어도 하나 존재하며, 그 영향력이 일정 크기 이상이라는 것을 구체적인 식으로 보였다.

비공개 앤트로픽 모델과 연구자의 역할

PSI는 이번 실행에 “공개되지 않은 앤트로픽 모델(a non-public Anthropic model)”을 썼다고 밝혔다. 모델 이름과 PSI가 이 모델을 쓰게 된 경위는 공개하지 않았다.

연구는 PSI의 기술 연구원 데이비드 터투리언(David Turturean)이 이끌었다. 그는 연구 시스템을 개발하고 문제 범위를 정해 실행했으며, 모델이 쓴 논문 초안을 검토했다. PSI는 터투리언이 논문의 정확성에 책임을 진다고 밝혔다. 자문위원 짐 핼버슨은 증명을 감사했고, 자문위원 피알라 샤나한은 린 형식화에 의견을 냈다. 증명과 논문, 형식화 코드는 모두 AI 모델이 작성했다.

린 검증 명제 4개와 남은 조건

깃허브 저장소 설명에 따르면, 린 4.33.0으로 명제 4개를 임시 값이나 추가 공리 없이 증명했다. 이 가운데 하나는 아직 형식화되지 않은 아가르왈과 벤데이비드의 기존 결과를 전제로 한 조건부 명제다.

저장소 설명에 따르면, 논문 자체는 기계 검증 대상이 아니며 형식화한 명제가 원래 추측과 같은 뜻인지는 독자의 확인 몫으로 남겨 뒀다. 증명이 린을 통과했다는 사실과 원래 추측이 완전히 해결됐다는 판단 사이에는 사람 전문가의 확인이 아직 필요하다.

스탠퍼드 연구진 평가와 선행 연구

PSI가 공개한 논평에서 스탠퍼드대의 가이 블랑, 조던 닥터, 카먼 스트라슬, 리양 탄은 “엄청난 결과(This is a huge result)”라며 “양자 속도 향상이 가능한 문제의 성격에 중요한 함의를 가진 수십 년 된 추측을 해결했다”고 평가했다. 이들은 전문가용 해설을 집필하고 있다고 밝혔다.

같은 스탠퍼드 연구진은 지난 8월 아카이브에 공개한 논문에서 입력을 정해진 횟수의 병렬 단계로 읽는 알고리즘이라는 특수한 경우에 한해 이 문제를 증명했다. PSI의 이번 결과는 이 제한을 없앤 일반적인 경우의 증명이다.

무작위 입력에서 양자 우위는 다항식 수준

PSI에 따르면, 이번 증명은 무작위로 주어진 입력에서 양자 컴퓨터가 기존 컴퓨터보다 앞서는 정도가 다항식 수준에 그친다는 의미를 가진다. 다항식 수준이란 문제 크기가 커질 때 속도 차이가 제곱이나 세제곱처럼 일정한 거듭제곱 정도로만 벌어진다는 뜻이다. 양자 컴퓨터가 압도적인 속도 차이를 내려면 문제 자체에 특별한 구조가 있어야 한다는 기존 연구 결과와도 이어진다.

PSI는 공익법인으로 등록된 AI 연구 기업으로, 매슈 파인스가 최고경영자를, 알렉스 위스너그로스가 최고과학책임자를 맡고 있다. PSI는 브레이크스루 에너지 벤처스 주도로 5,800만 달러(약 778억 원) 이상을 투자받았다고 밝혔다.

FAQ( ※ 이 FAQ는 본지가 리포트를 참고해 자체 작성한 내용입니다.)

Q1. 아론슨-암바이니스 추측은 무엇인가요?
스콧 아론슨과 안드리스 암바이니스가 제기한 양자 컴퓨팅 이론 문제로, 2008년부터 풀리지 않았습니다. PSI는 이 추측의 증명이 무작위 입력에서 양자 컴퓨터의 우위가 다항식 수준에 그친다는 의미를 가진다고 설명했습니다.

Q2. 어떤 AI 모델이 증명했나요?
PSI는 자체 연구 시스템이 공개되지 않은 앤트로픽 모델을 이용했다고 밝혔습니다. 모델 이름은 공개하지 않았으며, 증명과 논문, 형식화 코드는 모두 AI 모델이 작성했다고 설명했습니다.

Q3. 증명은 완전히 검증됐나요?
린 4.33.0으로 명제 4개를 검증했지만, 그중 하나는 아직 형식화되지 않은 기존 결과를 전제로 합니다. 논문 자체는 기계 검증 대상이 아니며, 형식화한 명제가 원래 추측과 같은지는 독자가 확인할 부분으로 남아 있다고 PSI는 밝혔습니다.

기사에 인용된 리포트 원문은 PSI에서 확인할 수 있다.
리포트명: A proof of the Aaronson-Ambainis conjecture (PSI Research, 2026년 11월)
이미지 출처: 앤트로픽
해당 기사는 클로드를 활용해 작성되었습니다.