기술 요약: 신경 증명 임베딩 내 선택 공리(Axiom of Choice)의 기하학적 측정

문제 정의

선택 공리(AC)는 역사적으로 수학적 기초를 고전적(classical) 진영과 구성적(constructive) 진영으로 나누어 왔으며, 이 구분은 주로 철학적 및 방법론적인 차이에 머물러 왔다. 고전적 증명은 AC에 의해 허용되는 비구성적 지름길을 사용하는 반면, 구성적 증명은 명시적인 증거(witness)를 요구하지만, 이 두 패러다임이 단순히 공리 의존성을 넘어 탐지 가능한 방식으로 구조적 차이를 보이는지는 불분명했다. 본 논문은 선택 공리가 형식 증명 공간, 특히 Lean 4의 Mathlib 라이브러리 내에서 측정 가능한 "기하학적 시그니처(geometric signature)"를 남기는지, 그리고 이러한 시그니처가 신경 정리 증명기(neural theorem provers)에 운영상의 결과를 초래하는지 조사한다.

연구 방법론

데이터 분할 및 의존성 추적

저자들은 Lean 4의 커널 수준 의존성 추적을 활용하여 471,260개의 기계 인증 선언(declarations)을 포함하는 Mathlib 라이브러리를 분할한다. 의존성 그래프에 대한 너비 우선 탐색(BFS)을 수행함으로써, 저자들은 선언들을 다음 두 집합으로 분류한다:

1. 고전적 증명 (Classical Proofs): Classical.choice에 이행적으로(transitively) 의존하는 것들.
2. 구성적 증명 (Constructive Proofs): 그렇지 않은 것들.

고전적 증명의 "거리"는 해당 증명에서 Classical.choice까지의 최단 의존성 체인 길이로 정의된다. 이를 통해 증명들은 공리로부터의 깊이에 따라 계층화된 데이터셋으로 그룹화된다. 본 연구는 태틱 트레이스(tactic traces)의 길이가 2에서 200단계 사이인 42,355개의 정리(고전적 정리 31,144개, 구성적 정리 11,211개)로 필터링된 모집단을 대상으로 한다.

레이블 프리 표현 학습 (Label-Free Representation Learning)

증명의 기하학적 특성을 편향 없이 측정하기 위해, 저자들은 오직 구성적 증명만을 사용하여 **자기 지도 노이즈 제거 오토인코더(self-supervised denoising autoencoder)**를 학습시킨다.

• 입력: 증명은 특정 인자(arguments)를 제외하고 증명 구성에 집중하기 위해 태틱 헤드(tactic heads, 예: intro, rw, simp)의 시퀀스로 표현된다.
• 아키텍처: 4개 층의 트랜스포머 인코더와 2개 층의 디코더가 결합된 형태이다. 모델은 입력 시퀀스에서 마스킹된 태틱 토큰(20% 오염)을 재구성하도록 학습된다.
• 임베딩: 증명 임베딩은 패딩을 제외한 인코더 은닉 상태(hidden states)의 평균이며, 단위 구(unit sphere)로 정규화된다.
• 레이블 프리 제약: 인코더는 학습, 어휘 구축 또는 하이퍼파라미터 선정 과정에서 고전적 증명을 전혀 보지 않는다. 고전적 증명은 엄격하게 측정용 홀드아웃(held-out) 모집단으로만 사용된다.

기하학적 측정

고전적 증명이 구성적 학습 분포로부터 벗어나는 정도를 의존 깊이에 따른 함수로서 측정하기 위해 세 가지 상호 보완적인 지표를 사용한다:

1. 이상치 점수 (Anomaly Score, k-NN): $k$-최근접 구성적 이웃과의 유클리드 거리.
2. 재구성 손실 (Reconstruction Loss): 구성적으로 학습된 모델이 고전적 증명의 마스킹된 토큰을 예측할 때 발생하는 교차 엔트로피 손실.
3. 밀도 상위 레벨 포함도 (Density-Superlevel Containment): 구성적 학습 분포에 의해 정의된 고밀도 영역(superlevel set) 밖에 위치하는 고전적 증명의 비율.

운영 평가

본 연구는 두 가지 시스템을 사용하여 정리 증명 성능에 미치는 영향을 평가한다:

1. aesop: 심볼릭 최선 우선 탐색(best-first search) 증명기.
2. 하이브리드 (ReProver + aesop): 태틱 생성기가 첫 번째 움직임을 제안한 후 aesop가 이어지는 신경 가이드 방식.

주요 결과

깊이 법칙 (The Depth Law)

주요 발견은 "깊이 법칙"의 존재이다: 즉, 고전적 증명과 구성적 증명 사이의 기하학적 차이는 Classical.choice로부터의 거리에 따라 예측 가능한 방식으로 감소한다.

• 얕은 깊이에서의 뚜렷한 분리: 깊이 2(직접적으로 고전적 렘마를 호출하는 증명)에서 분리는 강력하다. k-NN 이상치 점수는 0.847의 AUC를 달와, 재구성 손실은 구성적 베이스라인보다 34.5% 높으며, 고전적 증명의 **43%**가 구성적 90% 밀도 영역 밖에 위치한다.
• 구분 불가능성으로의 수렴: 깊이가 증가함에 따라, 지표들은 구성적 베이스라인으로 수렴한다. 깊이 9 이상에서는 세 가지 지표 모두 우연 수준(AUC $\approx$ 0.5, 손실 $\approx$ 베이스라인, 포함도 $\approx$ 90%)에 도달하여, 깊은 단계의 고전적 증명은 구성적 증명과 기하학적으로 구분이 불가능해진다.
• 단일 파라미터 혼합 법칙: 저자들은 이 기울기를 두 분포의 혼합으로 모델링한다: 구성적 분포 $P$와 직접적 고전 분포 $R$. 깊이 $d$의 분포 $Q_d$는 $Q_d = (1 - \lambda_d)P + \lambda_d R$로 모델링되며, 여기서 $\lambda_d$는 감소하는 혼합 가중치이다. 정규화했을 때 세 가지 서로 다른 측정치가 하나의 곡선으로 수렴하며, 이는 단일 파라미터 법칙을 뒷받침한다.

강건성 제어 (Robustness Controls)

이 시그니처는 다음과 같은 잠재적 혼란 변수들에 대해 강건하다:

• 키워드: 명시적인 고전적 태틱 마커(예: classical, by contra)를 제거해도 깊이-2 AUC는 약간만 감소(0.847에서 0.754로)하며, 이는 신호가 어휘적인 것이 아니라 구조적임을 나타낸다.
• 길이: 임베딩을 증명 길이에 대해 잔차화(residualizing)해도 기울기가 사라지지 않는다.
• 저자/파일/주제: 저자, 파일, 수학적 하위 도메인을 제어하는 혼합 효과 모델(mixed-effects models)을 적용해도 신호가 지속됨을 확인했다.
• 정리(Statement) vs 증명(Proof): 정리 진술은 증명에 비해 훨씬 약한 깊이 기울기(집계 AUC 0.604)를 보였으며, 이는 신호가 주로 구성적(증명 구조)이지 주제적(정리 내용)이지 않음을 확인시켜 준다.
• 공리의 특이성: propext와 Quot.sound 또한 깊이 기울기를 보이지만, Classical.choice가 가장 가파른 기울기를 생성하며, 이는 독특한 운영적 결합을 시사한다.

운영적 결과

기하학적 시그니처는 증명기 성능과 상관관계를 갖는다:

• aesop 실패: aesop는 구성적 정리는 20.0% 해결하는 반면, 고전적 정리는 **1.5%**만 해결한다 (13배 차이). 기하학적 신호와 달리, 이 운영적 격차는 깊이에 따라 완화되지 않는다. 즉, 고전적 증명은 Classical.choice와의 거리에 관계없이 aesop에게 여전히 어렵다.
• 신경 가이드: 신경 태틱 생성기(ReProver)를 추가하면 격차가 약 5배(22.0% vs 4.5%)로 압축되지만, 완전히 해소되지는 않는다.
• 예측력: 기하학적 이상치 점수는 증명 길이보다 aesop의 실패를 더 잘 예측한다 (이상치 점수를 추가할 때 AUC가 0.766에서 0.841로 증가).

의의 및 주장

본 논문은 선택 공리가 증명 공간 내에서 측정 가능한 기하학적 상관물을 가진다는 최초의 경험적 증거를 제공한다고 주장한다. 저자들의 주장은 다음과 같다:

1. 구조적 구분: 고전적/구성적 구분은 단순한 철학적 입장이 아니라, 신경 임베딩을 통해 관찰 가능한 증명 구성의 구조적 속성이다.
2. 운영적 관련성: 이 기하학적 시그니처는 추상적인 호기심에 그치지 않고, 자동 정리 증명기의 성능을 예측한다. "깊이 법칙"은 증명이 공리로부터 멀어질수록 구조적으로 구성적 증명과 유사해지지만, aesop와 같은 심볼릭 증명기에게는 Classical.choice의 존재 자체가 여전히 운영적 장벽으로 남는다는 것을 시사한다.
3. 방법론적 기여: 본 연구는 단일 클래스(구성적 증명)에 대한 레이블 프리 자기 지도 학습이 논리적 의존성에 의해 정의된 홀드아웃 클래스(고전적 증명)의 구조적 경계를 드러낼 수 있음을 보여주며, 이는 메타 수학적 분석을 위한 새로운 도구를 제공한다.

저자들은 인과 기제에 대해 조심스러운 입장을 유지하며, 기하학적 시그니처와 운영적 격차가 강하게 연관되어 있기는 하지만, 증명기의 어려움의 구체적인 원인(구조적 장벽인지 아니면 규칙 집합의 설정 때문인지)은 추가적인 조사가 필요하다고 언급했다. 본 연구는 커뮤니티가 형식 라이브러리 내에서 이와 유사한 구조적 축을 식별하도록 초대하는 작업으로 프레임화되었다.