피지컬 슈퍼인텔리전스(PSI)가 2008년 제기된 양자 추측을 증명했다고 밝혔어요. 비공개 Anthropic 모델 기반 시스템이 사흘째에 완전한 증명을 냈고 Lean이 검증했어요. 다만 저널 심사나 원저자 평가는 아직이라, 검증 이후가 더 중요해요.
11월 6일, 피지컬 슈퍼인텔리전스(Physical Superintelligence, 이하 PSI)라는 미국 스타트업이 꽤 큰 주장을 내놨어요. 🔬 양자 컴퓨팅 이론에서 2008년부터 열려 있던 'Aaronson-Ambainis 추측'을 자사 연구 시스템이 증명했다는 거예요. 이 추측은 쉽게 말해, 차수가 낮은 함수라면 결과에 꽤 큰 영향을 주는 입력 좌표가 반드시 하나는 있다는 내용이고, 양자 컴퓨터가 언제 고전 컴퓨터보다 확실히 빨라질 수 있는지를 가르는 문제와 이어져 있어요.
눈에 띄는 건 누가 풀었느냐예요. PSI는 자사 시스템이 Anthropic의 비공개 모델을 써서 작업했다고 밝혔어요. 보도에 따르면 시스템은 작업 3일차에 완전한 증명을 만들었고, 그 증명의 각 단계를 증명 보조기 Lean이 받아들였어요. 이후에는 결과를 두 번 더 개선했고, 최초 증명과 개선본 모두 Lean 검증을 거쳤다고 해요. 증명 전략은 샤하르 로벳과 지아펑 장이 제시한 계획을 따랐는데, 두 사람이 추측 상태로 남겨 둔 부등식 하나를 메운 구조라고 하고요.
여기서 Lean이 왜 중요하냐면, AI가 쓴 긴 증명은 사람이 읽고 맞는지 확인하기가 정말 어렵거든요. 그런데 Lean은 형식 검증이라 단계가 틀리면 통과 자체가 안 돼요. 그래서 요즘 AI 수학 주장들이 자꾸 Lean 이야기를 하는 거고, 얼마 전 다뤘던 Axiom의 유한 단순군 분류 사례도 같은 맥락이었어요. 코드는 GitHub의 physical-superintelligence/aaronson-ambainis 저장소에 공개돼 있고, 논문과 Lean 4 형식화가 같이 올라와 있다고 해요. 📊
근데 솔직히 조심할 부분도 있어요. Lean이 보장하는 건 '형식화된 문장이 참'이라는 것까지고, 그 문장이 원래 문제와 정확히 같은지는 사람이 봐야 해요. 저장소 README가 Conjecture.lean의 첫 정의를 원문과 대조해 보라고 안내하는 이유가 그거예요. 게다가 아직 저널 심사도 없고, 아론슨이나 암바이니스가 공개적으로 평가했다는 기록도 찾지 못했어요. 짐 할버슨이 증명을 감수하고 피알라 샤나한이 Lean 형식화에 의견을 냈다고는 하지만, 어디까지나 회사 측 설명이에요.
제 생각엔 이번 건의 핵심은 '풀렸다'보다 '확인 가능한 형태로 나왔다'예요. 주장은 넘쳐나는데 검증 가능한 산출물이 같이 나오는 경우는 드물잖아요. 🚀 만약 커뮤니티 검증까지 통과한다면, 비공개 모델이 이런 수준의 연구를 해낸다는 사실 자체가 공개 모델 경쟁의 기준선을 올려놓을 것 같아요. 며칠 안에 전문가들의 반응이 어떻게 나올지, 그게 제일 궁금해요.
출처