애런슨, AI 증명 옳다고 믿어…쇼어 알고리즘엔 영향 없어

스콧 애런슨(Scott Aaronson) 애런슨·암바이니스 추측 공동 제안자는 인공지능(AI) 연구 시스템이 만든 증명에 신뢰를 표했다. 다만 증명 전체를 아직 완전히 이해하지는 못했다고 밝혔다.

애런슨은 8일 자신의 블로그에서 “증명이 옳다고 믿는다”고 말했다. 그는 신뢰의 근거로 증명의 각 단계를 검사한 Lean 인증서와 내용을 살펴본 연구자들을 들었다.

AI 연구기업 Physical Superintelligence(PSI)는 6일 자체 연구 시스템이 비공개 앤스로픽(Anthropic) 모델을 활용해 증명을 만들었다고 발표했다. 시스템은 실행 셋째 날 전체 증명을 완성했고, PSI는 이후 하한을 두 차례 개선했다고 밝혔다. 본지는 앞서 PSI의 애런슨·암바이니스 추측 증명 발표를 전했다.

모델의 구체적인 이름은 공개되지 않았다. 애런슨은 AI 연구 시스템과 그 안에서 사용된 모델이 각각 증명에 얼마나 기여했는지 알지 못한다고 밝혔다.

애런슨·암바이니스 추측은 특별한 규칙이 없는 무작위 입력에서 양자 알고리즘과 일반 알고리즘의 입력 조회 횟수를 비교한다. 연구가 다루는 것은 양자 알고리즘의 ‘예·아니오’ 답변 확률을 일반 알고리즘이 얼마나 적은 조회로 근사할 수 있는지다.

문제의 시작 시점과 논문 공개 시점은 구분해야 한다. PSI는 이 추측을 2008년부터 열린 문제로 소개했지만, 애런슨과 안드리스 암바이니스(Andris Ambainis)의 원논문은 2009년 11월 5일 arXiv에 처음 게시됐다.

PSI의 연구 설명에는 분산이 ε 이상인 차수 d의 유계 다항식에 영향력이 큰 변수가 적어도 하나 있다는 정리가 실렸다. 그 영향력의 하한은 (8√15/(125π⁴))·ε^(5/2)/d⁶이며, 더 간단한 하한으로 (ε/d)^7도 제시됐다.

여기서 변수의 영향력은 입력 비트 하나를 바꿨을 때 다항식의 출력이 얼마나 달라지는지를 뜻한다. 이 정리는 임의의 계산에서 양자컴퓨터가 일반 컴퓨터보다 빠른지를 다루는 것이 아니라, 특정한 입력과 조회 복잡도 조건을 대상으로 한다.

Lean은 수학 명제와 증명을 형식 언어로 작성해 논리 규칙에 맞는지 컴퓨터로 검사하는 도구다. PSI의 공개 저장소는 Lean이 형식화된 명제와 증명을 검사했다고 설명한다.

다만 형식 명제가 원래 추측을 정확히 나타내는지는 독자가 별도로 대조해야 한다고 저장소는 밝히고 있다. 따라서 Lean의 검사는 입력된 명제와 증명의 논리적 연결을 확인하는 절차이며, 문제를 형식 언어로 옮긴 과정까지 자동으로 보증하는 것은 아니다.

MIT 연구자 가이 블랑(Guy Blanc)과 스탠퍼드대 연구자 조던 독터(Jordan Docter)·카르멘 스트라슬(Carmen Strassle)·리양 탄(Li-Yang Tan)은 7일 증명의 논리를 설명하는 해설문을 공개했다. 네 사람은 PSI에서 증명을 전달받아 검토하고 해설문을 작성했다고 밝혔다.

이들은 해설문을 작성하는 과정에서 앤스로픽의 공개 모델도 사용했다고 적었다. PSI나 앤스로픽에서 금전적 보상을 받지 않았다고도 밝혔다.

해설문은 학술대회나 학술지에 제출할 계획이 없다고 연구자들은 밝혔다. 해설문이 공개됐다는 사실이 증명에 대한 동료심사를 통과했다는 뜻은 아니다.

애런슨은 이번 결과를 양자 우위 전반이 사라졌다는 주장으로 넓혀서는 안 된다고 강조했다. 이번 연구는 무작위 입력을 다루는 특정 판정 문제와 양자 질의 복잡도에 관한 것이다.

그는 소인수분해에 쓰이는 쇼어 알고리즘이나 양자 물리·화학 시뮬레이션에는 이번 결과가 영향을 주지 않는다고 설명했다. 공개 연구는 가상자산 암호 기술의 안전성도 평가하지 않았다.

연구가 다룬 범위는 특정 수학적 추측의 증명과 형식화 검증이다. 반도체 산업과의 직접적인 연결도 제시되지 않았다.