11월 6일 스타트업 PSI(Physical Superintelligence)는 미공개 Anthropic 모델을 구동하는 사내 연구 시스템이 18년간 미해결이던 Aaronson-Ambainis 추측을 증명했다고 발표했다. 완전한 증명은 실행 3일째에 작성됐고, 증명 보조 도구 Lean의 단계별 검증을 통과했다. AI가 어려운 수학 문제에 도전한다는 점에서 상징적인 주장이지만, 아직은 한 회사의 주장에 불과하다. 논문은 동료 심사를 거치지 않았다.
이 추측은 무엇을 묻는가
Aaronson-Ambainis 추측이 묻는 것은 비구조화 데이터에 대해 양자 컴퓨터가 고전 컴퓨터보다 얼마나 빨라질 수 있는가이다. 비구조화 입력에서는 양자 알고리즘이 지수적 속도 향상을 이룰 수 없다고 주장한다. 2008년 제기된 이후 미해결로 남아 있었다. 올해 8월 스탠퍼드대 팀이 특수한 경우를 먼저 증명했고, PSI에 따르면 자사 시스템이 이를 완전한 경우로 확장했다. 증명이 버텨낸다면 양자 컴퓨팅 능력의 경계에 분명한 선이 그어진다.
기계는 어떻게 증명했고, 몇 번이나 검증했나
PSI에 따르면 연구 시스템은 회사 자체 인프라에서 연속 가동돼 3일째에 완전한 증명을 작성했고, 이후 관련 문제에서 결과를 두 차례 개선했으며, Lean은 매번 최종 버전을 받아들였다. PSI는 논문과 Lean 4 형식화 증명을 GitHub에 함께 공개했다. 기계 검증된 정리는 648개, 빈 증명 단계도 없고 추가로 도입한 공리도 없다. 명제는 Lean 커널과 독립 구현인 lean4lean으로도 다시 실행됐다. 논문의 정확성은 PSI 기술 직원 David Turturean이 책임지고, 수학자들이 증명을 감사했다.
교과서에 싣기는 아직 이르다
기계 검증을 통과했다고 수학계가 받아들인 것은 아니다. Lean이 보장하는 것은 각 단계가 규칙을 따랐다는 것뿐이며, 형식화된 명제가 Aaronson과 Ambainis가 원래 제시한 추측과 완전히 일치하는지는 확인할 수 없다. 그 점은 전문가의 수작업 대조가 아직 필요하다. 사람이 읽는 논문 본문 자체도 기계 검증을 거치지 않았다. 증명이 세는 것은 쿼리 횟수이지 총 계산 시간이 아니다. 사용된 모델도 공개되지 않았고 Anthropic은 논평을 거부했다. 같은 11월 6일 구글 DeepMind는 AI 에이전트가 1024비트 RSA 암호의 새로운 약점 두 가지를 찾았다고 발표했다. AI는 수학과 암호학 두 방향에서 동시에 전진하고 있다. PSI의 증명이 동료 검증을 견뎌낼지, 앞으로 수 주간의 전문가 검토가 답을 줄 것이다.
