PSI의 Aaronson–Ambainis 추측 증명: Lean 검증의 범위와 공개 코드

PSI가 2026년 11월 6일 Aaronson–Ambainis 추측의 증명을 공개했다. 비공개 Anthropic 모델을 쓰는 내부 연구 시스템이 증명을 찾았고 Lean이 받아들였다는 발표다. 개발자 관점에서는 AI가 만든 결과를 어떤 명제로 고정하고 어떤 검사기로 확인했는지 살펴볼 만하다. PSI 공식 발표에서 연구 경위와 수학적 배경을 확인할 수 있다.

양자 계산의 어떤 질문을 다뤘나

이 추측은 양자 컴퓨터가 무작위 입력에서도 고전 컴퓨터보다 지수적으로 적은 질의로 문제를 풀 수 있는지와 연결된다. 여기서 질의는 입력 정보를 읽는 횟수다. PSI는 낮은 차수의 유계 다항식에 영향력이 충분히 큰 변수가 존재한다는 명제를 증명했다고 밝혔다.

이 결과를 모든 양자 알고리즘의 실행 시간이나 모든 입력에 관한 결론으로 넓혀 읽으면 안 된다. 공식 설명은 작은 오차와 예외 입력의 비율을 고정한 조건에서 질의 수가 어떻게 늘어나는지를 다룬다.

공개 저장소에서 확인할 수 있는 것

공식 GitHub 저장소는 논문과 Lean 4 형식화, 검증 기록을 함께 공개했다. 최종 정리의 명세는 AaronsonAmbainis/Conjecture.lean에, 정리 선언은 AaronsonAmbainis/Main.lean에 있다. 설명 글과 기계가 검사한 명제를 나란히 읽을 수 있는 구성이다.

저장소는 핵심 정리에 자리표시자나 추가 공리가 없으며 별도 커널 구현으로 재검사했다고 보고한다. 다만 네 번째 정리는 별도 가정을 받는 강화 결과다. 모든 정리가 같은 가정 아래 있다는 식으로 묶으면 조건을 놓친다.

Lean 검사를 통과했다는 말의 범위

저장소가 밝힌 검증 범위에도 경계가 있다. 형식화한 명제가 원래 추측을 정확히 표현하는지는 사람이 대조해야 한다. 논문 전체가 기계 검사를 받은 것도 아니다. Lean과 Mathlib, 실행한 기계에 대한 신뢰도 남는다.

PSI는 실행 사흘째에 완전한 증명을 얻었고 이후 결과를 두 차례 개선했다고 설명한다. 이는 연구진의 보고다. 이번 글에서는 공개 자료를 읽고 설명과 조건을 대조했으며 Lean 빌드나 커널 재검사를 직접 실행하지 않았다. 연구진이 공개한 검사 기록을 독립 재현 결과로 표현하지 않는다.

AI 개발에서 참고할 검증 방식

이 사례를 개발 작업에 적용한다면 명세, 산출물, 검사 기록을 따로 남기는 방식부터 참고할 수 있다. 코드가 빌드되는지 확인하는 것과 의도한 요구사항을 만족하는지 확인하는 과정도 구분할 필요가 있다. 이는 공개 저장소의 검증 구조에서 얻은 개발 관점의 해석이다.

비공개 모델로 얻은 연구 성과이므로 같은 모델을 지금 내려받아 재현할 수 있다고 안내할 근거는 없다. 당장 검토할 수 있는 대상은 공개된 논문과 형식화 코드, 그리고 검사 범위를 명시한 기록이다.