기술 요약: 데이터 검증은 양자 컴퓨팅 코파일럿의 미래이다

문제 정의

양자 프로그램의 생성과 컴파일은 대규모 언어 모델(LLM)의 통계적 추론 특성과 충돌하는 수준의 정밀도를 요구한다. 양자 컴퓨팅 작업은 고수준 회로 기술부터 저수준 게이트 배치에 이르기까지 여러 추상화 계층을 가로질러야 하며, 엄격한 수학적 제약 조건(예: 유니타리성, 하드웨어 토폴로지, 게이트 충실도)을 준수해야 한다. 오류를 허용하거나 평균화할 수 있는 자연어 작업과 달리, 양자 프로그램 생성은 오류에 대한 무관용(zero tolerance)을 요구한다. 단 하나의 잘못된 게이트 시퀀스만으로도 근본적인 물리 법칙을 위반하게 된다.

현재의 LLM 기반 접근 방식은 세 가지 결정적인 한계에 직면해 있다:

1. 실행 불가능한 솔루션: 데이터 검증 없이는 LLM의 통계적 본질 때문에 실행 불가능한 솔루션이 수학적으로 불가피하게 발생한다. 이는 모델 스케일링과 무관하다.
2. 데이터 희소성: 포괄적이고 검증된 양자 데이터셋을 생성하는 것은 매우 어렵다. 기존 데이터셋(예: QDataSet)은 1~2 큐비트의 작은 시스템만을 커버하기 위해 수개월의 HPC 시간이 소ло 필요했다.
3. 탐색 공간 제약: 양자 회로의 유효한 부분 공간(subspace)은 전체 설계 공간에 비해 지수적으로 작으며, 유니타리성과 하드웨어 제약에 의해 경계가 지어진다. 현재의 LLM 아키텍처는 이 공간을 탐색하는 데 필요한 검증 메커니즘을 내부적으로 제공할 수 없다.

방법론 및 프레임워크

본 논문은 "추론 전용(inference-only)" 또는 "사후 필터링(post-hoc filtering)"에서 **검증 우선 아키텍처(verification-first architectures)**로의 패러다임 전환을 제안한다. 저자들은 이론적 논거와 예비 실험을 통해 뒷받지되는 세 가지 핵심 입장을 정의한다.

1. 데이터 검증은 최소 요구 사항임 (P1)

저자들은 훈련 데이터가 훈련 세트에 포함되기 전에 반드시 형식적으로 검증되어야 한다고 주장한다.

• 개념: "검증 인식 모델(Verification-aware model)"은 모든 예시가 도메인 특화된 정답 제약 조건(예: Lean이나 Z3와 같은 자동 정리 증명기를 통해 증명됨)을 만족하는 데이터로만 훈련된다.
• 근거: 검증되지 않은 데이터(예: 저품질 코드 저장소)로 훈련하는 것은 "암묵적 데이터 오염(implicit data poisoning)"을 의미한다. 자연어에서는 방대한 데이터량이 노이즈를 상쇄할 수 있지만, 양자 회로 데이터에서의 단 하나의 잘못된 예시는 주변의 유효한 예시들과 상관없이 유니타리성을 위반한다. 이는 더 많은 검증되지 않은 데이터가 오류를 희석하는 것이 아니라 오히려 증폭시키는 "안티 스케일링(anti-scaling)" 현상으로 이어진다.
• 메커니즘: 검증된 데이터셋은 모델이 제약 조건을 통계적 근사가 아닌 학습된 구조로서 내재화할 수 있게 한다.

2. 사후 필터링보다 우선하는 사전 제약 (P2)

검증은 출력을 생성한 후 필터링하는 것이 아니라, 생성 과정 전에 출력을 제약해야 한다.

• 근거: 양자 회로 설계에서 유효한 설계의 비율은 구성 요소(큐비트/게이트)가 증가함에 따라 지수적으로 감소한다. 설계 공간이 $O(d^n)$으로 성장할 때, 제약 조건은 유효한 설계를 $O(\delta^n)$ ($\delta < d$)으로 줄인다.
• 결과: 사후 필터링(많은 후보를 생성하고 유효하지 않은 것을 거부하는 방식)에 의존하는 것은 지수적인 계산 비용을 초래하며 성공 확률이 극도로 낮아진다. 검증은 토큰 생성 중에 잘못된 경로를 방지하기 위한 아키텍처적 프리미티브(primitive)로 내장되어야 한다.

3. AI4Research를 위한 검증 우선 패러다임 (P3)

저자들은 이 검증 우선 접근 방식을 물리 법칙이나 수학적 공리에 의해 지배되는 다른 과학 분야(예: 신약 개발, 재료 과학, 엔지니어링 설계)로 확장할 것을 권고한다.

• 개념: 이러한 도메인들은 "누출된 추상화(leaky abstraction)" 및 "비분해성(non-decomposability)" 문제를 공유하며, 여기서 국소적 최적 선택이 전역적 최적성을 보장하지 않는다. 하드 제약 조건을 처리하기 위해서는 검증 인식 아키텍처가 필수적이다.

실험 결과

Position 1을 입증하기 위해, 저자들은 검증된 MAJ/UMA(Majority/UnMajority-and-Add) 회로 코퍼스에서 파생된 데이터셋을 사용하여 평가를 수행했다.

• 설정: 270M에서 120B 파라미터에 이르는 34개의 공개 LLM을 대상으로 2~8 큐비트 양자 애더(adder) 최적화에 관한 70,000개의 객관식 질문을 테스트했다. 정답(Ground Truth)은 Toffoli 카운트, 깊이, 총 게이트의 가중치 점수가 최소인 회로이다.
• 정확도: 검증 지식을 바탕으로 훈련되거나 미세 조정된 모델(예: gemma3:12b, gpt-oss:120b)은 0.60에서 0.79 사이의 정확도를 달림. 반면, 검증 인식이 없는 일반 모델들은 무작위 베이스라인(0.21–0.29) 근처에 머물렀다.
• 보정(Calibration): 검증 인식 모델들은 우수한 불확실성 정량화 능력을 보여주었다. gpt-oss 모델은 정답에 대해 60–80%의 확신도를 할당한 반면, gemma3 모델은 20–35% 범위에 머물렀다.
• 실패 모드: 몇몇 모델(예: mixtral:8x7b, deepseek-r1 변형)은 잘못된 출력(단일 문자 답변 대신 장황한 거절이나 설명)으로 인해 무작위 베이스라인보다 낮은 점수를 기록했으며, 이는 검증 훈련 없이는 모델이 형식적으로 제약된 작업에 안정적으로 참여할 수 없음을 강화한다.
• 탐색 공간 분석: 저자들은 200,000개의 검증된 애더 설계를 생성했다. 그들은 깊이 3~6 사이의 MAJ/UMA 모듈에 대한 총 가능한 게이트 배열이 148조 개를 초과하지만, 형식적 검증을 통해 약 200,000개의 유효한 설계만을 식별했음을 언급했다(비율 $\approx 10^{-9}$). 이는 사후 필터링의 불가능함을 보여준다.

주요 기여

1. 검증 인식 모델의 공식적 정의: 검증된 제약 조건으로 훈련된 모델과 검증되지 않은 코드 저장소로 훈련된 모델을 구분함.
2. 세 가지 핵심 입장: 데이터 검증이 최소 요구 사항이며, 제약 조건이 사전적(a priori)이어야 하고, 이 패러다임이 과학적 AI에 필수적임을 확립함.
3. 실증적 증거: 데이터 검증 없이는 파라미터 규모와 관계없이 LLM이 양자 최적화 작업에서 높은 정확도나 적절한 보정 능력을 갖추지 못한다는 정량적 데이터를 제공함.
4. "누출된 추상화" 식별: 양자 프로그램 생성이 국소적 최적화만으로는 전역적 정확성을 보장할 수 없는 방식으로 추상화 계층(예: 모듈 설계 vs 게이트 분해)을 병합해야 함을 강조함.

의의 및 향후 연구 방향

본 논문은 물리적 또는 수학적 법칙에 의해 지배되는 도메인에서 AI가 실행 가능하려면, 검증을 "사후 고려 사항"에서 "아키텍처적 기초"로 격상시켜야 한다고 주장한다.

저자들은 두 가지 구체적인 향후 연구 방향을 제안한다:

• FD1 (아키텍처): 양자 코파일럿 아키텍처는 형식적 검증(예: 만족 가능성 모듈론 이론(SMT) 또는 심볼릭 명세)을 LLM의 토큰 생성 루프에 직접 통합하여, 검증을 이진 필터가 아닌 구조화된 탐색 가이드로 변환해야 한다.
• FD2 (벤치마크): 커뮤니티는 실행 가능한 검증 오라클(oracle)과 결합된 제약 조건이 풍부한 벤치마크를 필요로 한다. 이는 단순한 애더를 넘어 모듈형 곱셈, 양자 푸리에 변환, 하드웨어 특화 라우팅 등을 포함하여 시스템 간 비교를 위한 재현 가능한 표준을 가능하게 해야 한다.

논문은 논의가 양자 컴퓨팅에 집중되어 있지만, 그 원칙이 정답이 이진(binary)이며, 유효한 솔루션이 지수적으로 작은 부분 공간에 존재하고, 형식적 검증 방법이 존재하는 모든 분야에 광범위하게 적용될 수 있다고 결론짓는다.