PSI, 애런슨-암바이니스 추측의 기계 검증 증명 보고

Physical Superintelligence는 비공개 Anthropic 모델의 인스턴스를 실행하는 내부 연구 시스템이 2008년부터 미해결 상태였던 양자 컴퓨팅 문제인 Aaronson-Ambainis 추측의 증명을 찾아냈다고 2026년 11월 6일에 발표했다.

이 시스템은 PSI 자체 인프라에서 실행을 시작한 지 사흘째 되는 날 완전한 증명을 내놓았고, Lean 증명 보조기가 이를 승인했습니다. 이후 PSI는 관련 미해결 문제들을 시스템에 맡겼고, 시스템은 결과를 두 차례 개선한 끝에 Lean이 최종 버전을 승인했습니다. 원고와 Lean 4 형식화는 공개되어 있습니다.

추측이 양자 속도 향상에 관해 말하는 것

이 문제는 양자 컴퓨터가 언제 고전 컴퓨터보다 기하급수적으로 빨라질 수 있는지를 다룹니다. 쇼어의 1994년 소인수분해 알고리즘은 입력의 구조에 의존합니다. 입력에 알고리즘이 활용할 수 있는 반복 패턴이 들어 있기 때문입니다. PSI의 결과는 이와 대조적으로, 일반적으로 그런 패턴이 없는 무작위 입력이나 비구조적 입력의 경우를 다룹니다.

질의 모델에서 고전 알고리즘은 질의 한 번에 비트 하나를 읽지만, 양자 질의는 중첩 상태로 여러 입력 위치에 걸쳐 분포할 수 있습니다. PSI의 설명은 이 모델을 다항식과 연결합니다. 양자 질의를 T회 수행한 뒤 알고리즘이 ‘예’라고 답할 확률은 입력 비트의 유계 다항식이며, 그 차수는 최대 2T입니다. 따라서 양자 알고리즘을 시뮬레이션하려면 입력 비트를 기하급수적으로 많이 읽지 않고 해당 다항식을 추정하는 방법을 찾아야 합니다.

두 사람은 최초 논문에서 모든 유계 저차 다항식에 영향력이 매우 큰 변수가 하나 이상 있다고 추측했습니다. 두 사람은 이 추측을 가정하면 모든 T회 질의 양자 알고리즘을 대부분의 입력에서 T에 대한 다항식 개수의 질의를 수행하는 고전 알고리즘으로 시뮬레이션할 수 있음을 증명했습니다. 그 결과, 근사 오차와 제외할 입력의 비율을 각각 고정하면 고전 질의 수는 기하급수적으로 늘어나는 대신 다항식적으로 늘어납니다. 다만 적절한 구조를 갖춘 문제에서 양자가 기하급수적으로 더 빠를 가능성까지 배제하는 것은 아닙니다.

형식적으로 저장소는 차수가 최대 d이고 이산 큐브에서 값이 0과 1 사이에 있는 실수 다항식 p를 다룹니다. 균일 무작위 입력에 대한 분산이 ε 이상이면, 어떤 좌표의 영향력은 (8√15 / (125π⁴)) · ε^(5/2) / d⁶ 이상이며, 따라서 (ε/d)⁷ 이상입니다. 영향력이란 해당 좌표의 비트를 뒤집었을 때 p가 변하는 양의 제곱에 대한 기댓값입니다.

증명의 구성과 검증 방법

이 논증은 분수 인증서와 등위 집합에 기반한 Shachar Lovett와 Jiapeng Zhang의 계획을 따르지만, 그 계획에서 추측으로 남겨 둔 부등식을 새로운 모든 쌍 부등식으로 대체합니다. 행렬식은 입력 설정을 일대일로 짝짓습니다. PSI에 따르면 이 짝짓기는 David Reimer의 더 약한 Butterfly Lemma 짝짓기보다 한발 더 나아갑니다. 짝지어진 설정이 각 좌표에서 서로 일치하는 횟수에도 제한을 두기 때문이며, 이 제한은 새로운 부등식에 필요합니다.

저장소는 기본 증명을 네 부분으로 나눕니다. 행렬식과 전단사 대응으로 모든 쌍 부등식을 도출하고, 이를 등위 집합 전체에 걸쳐 적분하며, 좌표 전체에 대해 평균을 구하고, 점별 민감도 상계를 이용해 행 상계를 확립합니다. 이 단계들을 결합하면 명시적인 영향력 상계를 얻을 수 있습니다.

저장소에 기록된 감사 결과에 따르면 형식화된 전개에는 증명 자리표시자나 추가 공리가 없습니다. 선언들은 Lean의 커널과 Lean 형식 검사기를 독립적으로 구현한 lean4lean을 통해 재생성되었습니다. 샌드박스 실행에서는 nanoda 및 Lean 커널을 사용하는 비교기가 최종 정리 네 개를 모두 승인했습니다. 두 번째 컴퓨터에서는 올바른 작은 해 하나를 승인하고 의도적으로 틀리게 만든 해 네 개를 거부했습니다.

이러한 검증에는 명시적인 한계가 있습니다. 독자는 형식화된 진술이 인쇄된 추측과 일치하는지 여전히 확인해야 합니다. 사람이 읽을 수 있는 논문 자체는 기계 검증된 것이 아니며, Lean의 커널과 컴파일러, Mathlib의 정의, 검증에 사용된 컴퓨터는 여전히 신뢰 기반의 일부로 남습니다.

인간의 역할과 전문가 검토

PSI 기술 직원인 David Turturean은 연구 시스템을 개발하고 실행했으며, 문제의 범위를 정하고 모델에 초안을 작성하도록 지시한 뒤 그 초안을 검토했으며, 논문의 정확성에 책임을 집니다. 저장소에는 수학적 진술과 초안, Lean 형식화를 AI 모델이 생성했다고 공개되어 있습니다. Jim Halverson은 증명을 감사했고, Phiala Shanahan은 형식화에 의견을 제시했습니다.

이번 발표에 앞서 Guy Blanc, Jordan Docter, Carmen Strassle, Li-Yang Tan은 2026년 8월 19일 제출된 논문에서 고전적 시뮬레이션의 결과를 병렬 양자 알고리즘으로 확장해 해결했습니다. 이들은 t회 질의, d라운드 알고리즘을 대부분의 입력에서 t^(O(d²))회의 고전적 질의로 시뮬레이션할 수 있음을 증명했습니다. PSI에 따르면 이 네 사람은 전체 증명을 읽으며 의견을 제시했고, 전문가를 위한 더 짧은 설명을 준비하고 있습니다.

PSI가 발표한 평가에서 연구진은 다음과 같이 썼다. “이는 엄청난 성과입니다. 양자 속도 향상을 허용하는 문제의 본질에 중요한 시사점을 지닌 수십 년 된 추측을 해결합니다. 이 증명은 불 함수 분석과 확률 조합론 분야의 여러 연구 흐름을 바탕으로 삼고 이를 확장합니다. 이 모든 것을 상당히 놀라운 방식으로 하나로 엮어냈습니다.”

당장 검증할 수 있는 기준은 이례적으로 구체적이다. 독립적인 커널은 인코딩된 논증을 다시 실행할 수 있지만, 전문가들은 인코딩된 명제가 Aaronson과 Ambainis의 추측과 일치하는지 여전히 확인하고, Lean 외부에서 작성된 논문의 부분도 평가해야 한다. 이 구분에 따라 기계 검증으로 확립되는 내용과 사람의 수학적 검토가 여전히 필요한 내용이 정해진다.