Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256

기술 요약: Lean을 이용한 쇼어 알고리즘(Shor's Algorithm) 구축

문제 정의
본 논문은 쇼어 알고리즘과 그 변형들, 특히 RSA-2048 및 타원 곡선 P-256의 암호 해독을 대상으로 수학적 기초, 회로 동작, 그리고 자원 추정치를 형식적으로 검증하는 과제를 다룹다. 기존의 형식 검증 노력들은 쇼어 알고리즘의 일부(예: 차수 찾기 또는 추상적 유니터리 연산)를 다루어 왔으나, 암호학적 문제 축소와 확률 분석에서부터 가역 산술 회로 및 구체적인 논리적 자원 계측에 이르기까지 전체 체인을 통합하여 기계적으로 검증된 개발은 부족한 실정이다. 저자들은 고수준의 암호학적 주장과 저수준의 게이트 수 및 성공 확률을 연결하는 통합된 기계 검증 프레임워크를 Lean 정리 증명기(theorem prover) 내에 제공함으로써 이 간극을 메우고자 한다.

방법론: 에이전트 기반 형식화(Agentic Formalization)
본 연구는 "에이전트 기반 형식화" 워크플로우를 채택한다. 이 과정에서 소프트웨어 에이전트는 다음과 같이 형식적 개발을 보조한다:

1. 소스 분석: 관련 과학 문헌(특히 [Quantum 5, 433] 및 [ASIACRYPT 2017, 241–270])을 검색하고 분석한다.
2. 분해 및 코딩: 과학적 주장을 수학적 및 계산적 의무로 분해한 후, Lean 코드와 증명을 생성한다.
3. 수정 및 반복: 에이전트는 증명 오류를 해결하기 위해 수정안을 제안한다.
4. 인간 검토: 인간 저자가 과학적 주장, 소스 정렬 및 결과적인 형식 문구를 검토한다.
5. 기계 검증: Lean 커널이 임포트된 정의 및 가정에 대해 모든 수락된 증명을 검증한다.

이 워크플로우는 일반 수학을 위한 Mathlib, 컴퓨터 과학 기초를 위한 CSLib, 그리고 유한 차원 양자 정보 이론을 위한 Lean-QIT를 포함하는 Lean 생태계에 의존한다. 결과물인 라이브러리는 에이전트와 연구자가 의존성을 찾고, 검사하며, 검증된 구성 요소를 재사용할 수 있도록 안정적인 이름(stable names)과 모듈 위치를 사용한다.

주요 기여
본 논문은 Lean 생태계 내에서 두 가지 주요 응용 수준의 형식화를 제시한다:

1. RSA-2048 인수 분해:

   • 정수 인수 분해를 차수 찾기(order finding)로 축소하는 과정을 형식화한다.
   • Vedral–Barenco–Ekert 구성을 기반으로 가역 모듈로 산술 회로(덧셈, 곱셈, 거듭제곱)를 개발한다.
   • 짧은 이산 로그를 위한 Ekerå–Håstad 경로를 구현하여 RSA-2048에 대한 특정 논리 회로 기준선을 제공한다.
   • 이를 결합하여 소인수 회복에 관한 기계 검증된 문장을 생성한다.

2. P-256 스칼라 회복:

   • 소수체 $\mathbb{F}_p$ 상에서의 타원 곡선 이산 로그 문제(ECDLP)를 형식화한다.
   • Montgomery–Kaliski 역원 계산 및 나눗셈을 포함한 소수체 상의 가역 산술을 구축한다.
   • 제어된 점 덧셈(controlled point additions)을 통한 가역 타원 곡선 점 연산(덧셈 및 배가)과 스칼라 곱셈을 구현한다.
   • 정량적 성공 범위와 논리적 자원 값을 갖춘, 기계 검증된 P-256 스칼라 회복 문장을 제공하는 최초의 Lean 개발 사례를 제시한다.

주요 결과
형식화 결과, 명시적인 자원 프로필과 성공 보장을 포함하는 두 가지 주요 정리가 도출된다:

• 정리 1 (RSA-2048): 확률이 최소 $2/3$ 이상인 확률로 인자 $d \in \{p, q\}$를 반환하는 양자 알고리즘이 존재한다. 성공 임계값 달성을 위한 세 번의 연속 시도에 대한 자원 프로필은 다음과 같다:

  • $6.19 \times 10^3$ 논리 큐비트.
  • $8.1 \times 10^9$ Toffoli 게이트.
  • $6.42 \times 10^9$ 최대 회로 깊이.
  • $3.69 \times 10^4$ 회복을 위한 고전적 산술 연산.

• 정리 2 (P-256): 확률이 최소 $2/3$ 이상인 확률로 개인키 스칼라 $m$을 반환하는 양자 알고리즘이 존재한다. 1회 실행에 대한 자원 프로필은 다음과 같다:

  • $2.33 \times 10^3$ 논리 큐비트.
  • $1.26 \times 10^{11}$ Toffoli 게이트.
  • $1.16 \times 10^{11}$ 최대 Toffoli-게이트 깊이.
  • 직접 회복을 위한 7개의 고전적 연산.

본 논문은 이러한 결과들을 기존의 점근적 분석 및 게이트 수준 추정치와 비교하며, Lean 형식이 이전의 기계 검증 맥락에서 결여되었거나 덜 엄격했던 명시적 성공 임계값과 고전적 연산 횟수를 제공한다는 점을 주목한다.

의의 및 주장
저자들은 본 연구가 양자 알고리즘의 AI 보조 설계 및 검증을 향한 중요한 진전이라고 주장한다. 수론, 확률 경계, 가역 회로 및 자원 공식이 단일 증명 언어를 공유하는 재사용 가능한 수학적 계층을 생성함으로써, 이 라이브러리는 연구자들이 다음을 수행할 수 있게 한다:

• 중간 정리들을 검색하고 그 의존성을 검사한다.
• 관련된 공식들을 비교하고 검증된 구성 요소를 새로운 분석에 조립한다.
• 최종 주장으로부터 수학적 전제까지의 추적 경로를 유지한다.

본 논문은 이 작업이 정량적 성공 범위와 논리적 자원 값을 갖춘 기계 검증된 P-256 스칼라 회복 문장을 제공하는 최초의 Lean 개발임을 명시적으로 밝히고 있다. 이는 더 넓은 기계 검증 양자 암호 해독을 위한 토대로 자리매김한다.

한계 및 향에 과제
본 논문은 그 범위에 대해 겸허한 태도를 보인다. 저자들은 다음과 같은 점을 언급한다:

• 자원 프로필은 **논리적(logical)**이며, 회로 노이즈, 양자 오류 수정, 매직 상태 생성 또는 물리적 큐비트 스케줄링을 고려하지 않는다.
• 최종 응용 수준의 정리들은 공공 입력(public inputs)으로부터 완전히 유도된 것이 아니라, 문헌(예: Ref [21] 및 [7]의 특정 자원 수치)에서 가져온 명시적 가정에 의존한다.
• 공공 입력(모듈러스 $N$ 또는 공공 점 $Q$)으로부터 전체 실행을 구축하고, 자원 분석을 결함 허용(fault-tolerant) 아키텍처 및 최적화된 회로군으로 확장하기 위한 향후 연구가 필요하다.