AI로 양자컴퓨팅 18년 난제 증명 발표…PSI, 검증 코드 공개

피지컬 슈퍼인텔리전스(PSI)가 11월 6일 양자컴퓨팅 이론의 미해결 문제인 에런슨–암바이니스 추측을 AI 연구 시스템으로 증명했다고 발표했다. 회사는 비공개 앤트로픽 모델을 사용했으며, 논문과 Lean 4 증명 코드를 함께 공개했다. 2008년 제기된 이 문제는 양자컴퓨터의 계산 이점이 생기는 조건을 다룬다.

연구자는 원래 추측과 기계가 검사하는 명제를 대조하고, 공개된 코드·실행 기록으로 검사 과정을 재현할 자료를 얻었다. 증명 코드와 문서는 아파치 2.0 라이선스이며 논문 저작권은 저자에게 남는다. 원래 문제를 코드로 정확히 옮겼는지는 사람이 읽고 판단해야 한다는 검증 범위도 함께 제시됐다.

추측이 다루는 것은 입력을 읽는 횟수인 ‘질의 복잡도’다. 에런슨과 암바이니스의 원래 논문은 이 추측이 참이면 T번 입력을 읽는 양자 알고리즘의 응답 확률을, 대부분의 입력에서 일반 컴퓨터가 T의 고정된 거듭제곱에 비례하는 횟수로 근사할 수 있다고 설명했다. 원래 논문은 근사 오차와 예외가 되는 입력의 비율을 함께 조건으로 둔다. 두 값을 고정했을 때 비교하는 대상은 입력 접근 횟수이며, 전체 실행 시간이나 모든 양자 계산의 우열을 판정하는 명제와는 범위가 다르다.

수학적으로는 0과 1로 구성된 입력에서 값의 범위가 제한된 낮은 차수의 다항식에 관한 문제다. 출력에 일정한 변동이 있다면, 적어도 한 입력 비트의 ‘영향력’은 일정 수준 이상이어야 한다. 영향력은 그 비트를 뒤집었을 때 생기는 출력 변화의 제곱을 평균한 값이다. PSI가 공개한 원문 대조표는 입력 비트 수와 상관없이 성립하는 이 영향력의 하한을 분산을 다항식 차수로 나눈 값의 일곱 제곱으로 명시하고, 이를 검사하는 코드의 정의와 연결했다.

논문의 AI 사용 설명에 따르면 데이비드 투르투레안이 문제 범위를 정하고 PSI 내부 연구 환경을 만들었다. 여러 모델 인스턴스가 기존 아이디어를 찾고, 새 접근을 제안·시험하며 서로의 작업을 조정했다. 부록은 실행 셋째 날 첫 완성 증명이 나왔고, 이후 결과를 두 번 개선해 하한식의 지수를 22에서 11, 다시 7로 낮췄다고 기록했다. 완성 뒤 다른 미해결 문제를 탐색하도록 지시한 과정에서 중간 결과를 다듬어 증명을 강화했다는 설명이다. 투르투레안은 모델이 만든 논문 초고를 직접 검토·수정했으며 정확성에 책임을 진다고 밝혔다.

증명 코드가 검사하는 범위

기계 검증에 제공된 라이브러리는 감사 기록상 84개 모듈의 761개 선언으로 구성됐다. 이 가운데 648개는 정리, 113개는 정의다. 감사 결과에 따르면 최종 정리들은 Lean의 표준 기초 공리 세 개에만 의존하며, 증명되지 않은 결론을 끼워 넣는 별도 공리나 미완성 증명 표시는 포함하지 않는다. 핵심 결과 세 개와 별도로, 더 강한 수치 경계를 얻는 네 번째 정리에는 외부 연구의 가정이 붙는다. 감사 문서는 그 가정이 핵심 세 정리에는 적용되지 않는다고 명시했다.

검사 기록은 소스 문자열을 훑는 감사와 증명 자체를 다시 검사하는 절차를 나눴다. 후자는 Lean 검사기에 각 증명 항을 다시 넘기고, 별도로 구현된 검사기로도 확인하는 방식이다. 빈 환경에서 Lean의 기초 라이브러리와 수학 라이브러리까지 다시 검사한 기록도 공개했다. 10월 22일의 과거 실행과 11월 공개 준비 실행은 날짜와 코드 식별자로 구분돼 있다.

11월 6일 공개 준비 기록에는 빌드, 공리 점검, 84개 모듈 재검사와 최종 정리 네 개의 비교 검사가 통과했다고 표시돼 있다. 올바른 예제 하나를 받아들이고 잘못된 예제 네 개를 거부한 대조 검사 결과도 포함됐다. 이는 PSI가 공개한 실행 산출물이며, 원래 실행이 이뤄진 준비용 저장소의 비공개 링크 대신 결과 파일을 읽을 수 있게 한 것이다.

논문과 Lean 코드의 대응 문서는 각 수학적 주장에 해당하는 정리를 안내한다. 다만 논문의 동기·관련 연구·일부 결과 해설은 형식 증명의 대상에서 빠져 있다. 기계 검사는 코드에 적힌 명제가 주어진 기초 위에서 도출되는지를 확인하고, 대응 문서는 코드가 다루는 부분과 사람이 읽을 설명의 경계를 구체적으로 나눠 놓았다.

PSI는 스탠퍼드 연구진 네 명이 증명을 읽고 의견을 보냈으며 전문가용으로 더 짧은 설명을 작성 중이라고 밝혔다.