데일리환경
  데일리환경
닫기
  • 정치
  • 경제
  • 사회
  • 문화/생활
  • 세계
  • IT/과학
  • 보도자료
  • 인사/부고/사고
  • 오피니언
  • 지면보기

#Lean

기사
  • AI 연구시스템, 양자컴퓨팅 난제 증명 발표…독립 검토 주목
    IT/과학

    AI 연구시스템, 양자컴퓨팅 난제 증명 발표…독립 검토 주목

    PSI, 아론슨–암바이니스 추측을 Lean으로 형식검증했다고 밝혀 공개 저장소에서 증명·코드 제공…외부 전문가 검토는 진행 중
    [데일리환경=유승철 기자] 미국 연구기업 Physical Superintelligence(PSI)가 인공지능(AI) 연구시스템으로 양자컴퓨팅 이론의 오랜 난제인 아론슨–암바이니스 추측을 증명했다고 발표했다. 회사는 증명을 정리증명기 Lean으로 형식화했고, 컴퓨터 검사를 통과했다고 밝혔다. 이 발표는 양자컴퓨터의 모든 성능 우위를 입증하거나 부정한 결과가 아니라, 무작위 입력을 다루는 특정 문제군의 속도 한계를 설명하는 수학적 결과다. PSI가 2026년 11월 6일 공개한 연구 설명은 이 추측을 2008년부터 열려 있던 문제로 소개했다. 아론슨과 암바이니스가 관련 추측을 정식화한 논문은 이후 학술지에 2014년 실렸다. 문제의 핵심은 양자컴퓨터가 입력에 특별한 구조가 없는 상황에서도 일반 컴퓨터보다 지수적으로 적은 정보 확인만으로 답을 낼 수 있는가다. 여기서 정보 확인은 알고리즘이 입력 자료의 특정 비트 값을 묻는 ‘질의’를 뜻한다.양자컴퓨터가 특정 계산에서 빠른 이유를 이해하려면 문제의 구조를 함께 봐야 한다. 쇼어 알고리즘은 큰 수의 소인수분해 등에 활용되는 양자 알고리즘으로, 입력에 숨어 있는 반복 구조를 찾아 속도를 높인다. 아론슨–암바이니스 추측은 이런 구조가 드러나지 않는 무작위 입력에서도 같은 수준의 지수적 이점이 가능한지를 다룬다. 모든 양자 알고리즘이 무작위 입력에서 느리다는 뜻은 아니며, 무작위 입력에 관한 제한된 유형의 예·아니오 문제에서 고전적 모의 계산이 얼마나 효율적인지를 묻는다.공개된 PSI 논문과 Lean 저장소는 결과를 저차 다항식의 변수 영향도에 관한 정리로 표현한다. 함수값이 0과 1 사이에 있는 다항식에서 전체 값의 변동이 일정 수준 이상이면, 입력 비트 가운데 적어도 하나를 바꿀 때 함수값이 일정한 크기 이상 달라지는 변수가 있다는 내용이다. 영향도는 해당 비트를 뒤집었을 때 함수값이 평균적으로 얼마나 달라지는지를 수치화한다. 기존 이론에 따르면 양자 알고리즘의 답변 확률은 입력 비트의 다항식으로 나타낼 수 있다. 따라서 영향도가 큰 변수를 찾아 입력을 확인하는 방식은 일반 컴퓨터가 양자 알고리즘의 답변 확률을 근사하는 데 연결된다.PSI는 내부 시스템이 비공개 앤트로픽 모델을 사용했고, 실행 사흘째 완전한 증명을 얻었다고 밝혔다. 연구진은 관련 문제를 더 살피며 결과를 두 차례 개선했고, 최종 증명을 Lean으로 검사했다고 설명했다. 공개 저장소는 증명 코드와 논문, 검증 방법을 제공하며 형식화 과정에 AI 모델이 사용됐다고 적었다. 연구를 이끈 데이비드 투르테란은 문제 설정과 시스템 운영을 맡았고, 생성된 논문 초안을 검토했다. PSI는 자문역 짐 핼버슨이 증명을 감사하고 피알라 섀너핸이 형식화에 의견을 보탰다고 밝혔다.Lean은 정리를 작은 논리 단계로 쪼개 각 단계가 정해진 규칙에서 도출되는지 검사하는 프로그램이다. 저장소는 완성된 네 개 정리에 미완성 증명 표시나 추가 공리가 없고, 서로 다른 두 Lean 커널 구현으로 다시 검사했다고 설명한다. 이런 검사는 형식화된 문장과 증명 사이의 논리적 연결을 점검하는 데 유용하다. 하지만 수학자가 읽을 수 있는 논문 속 개념이 원래 추측과 같은지, 정의나 형식화에 빠진 전제가 없는지, 결과가 기존 연구에서 어떤 새 의미를 갖는지에 대한 전문적 검토와는 다른 절차다.외부 검토도 진행 단계와 완료 단계를 구분해야 한다. PSI는 2026년 8월 추측의 특수한 경우를 증명한 스탠퍼드대 연구자들이 전체 증명을 읽고 의견을 전달했으며, 전문가용 설명을 작성 중이라고 밝혔다. 이는 PSI가 공개한 내용이며, 해당 연구자들의 독립 검증이 끝났거나 동료심사를 통과했다는 뜻으로 확인된 것은 아니다. 다만 논문과 코드를 공개한 만큼 다른 연구자가 형식화된 정리와 증명 과정을 살펴볼 수 있는 기반은 마련됐다.이번 사례는 AI가 수학적 연구에 참여하는 방식도 보여준다. PSI의 설명에 따르면 모델이 문제 풀이와 초안 작성에 관여했지만, 사람 연구자가 문제를 선택하고 시스템을 운영했으며 결과를 검토하고 논문 정확성에 책임을 진다. 기계검증 결과는 증명 과정의 신뢰도를 높이는 한 축이지만, 연구의 타당성을 완전히 판정하는 최종 인증과 같지는 않다. 독립 검토자가 논문과 코드, 원래 추측의 대응 관계를 확인하는 과정이 뒤따라야 한다.따라서 발표의 의미는 양자컴퓨팅의 실용적 성능이 즉시 바뀌었다는 데 있지 않다. 추측이 증명되면 무작위 입력에서 양자 알고리즘의 지수적 질의 이득이 성립하기 어려운 조건을 더 명확히 설명할 수 있다. 그러나 특정 양자 장치의 성능이나 상용화 시점을 직접 측정한 결과는 아니다. PSI의 증명 주장이 수학계에서 받아들여질지는 공개된 증거를 바탕으로 한 후속 검토와 재현이 이어지는지에 달려 있다.
    2026-11-08 18:18:08 유승철
  • 데일리환경
  • 서울특별시 용산구 원효로31길 17 (원효로3가) 2층
  • PC보기
Copyright ⓒ 데일리환경 All rights reserved.