Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Motivation

• Known: Lean 4와 Mathlib 같은 대규모 interactive theorem prover 라이브러리는 axiom dependency(propext, Quot.sound, Classical.choice)를 kernel 수준에서 추적할 수 있으며, classical/constructive 증명 구분은 오래된 철학적·방법론적 논쟁으로 존재해왔다. 또한 neural theorem prover(예: ReProver, AlphaProof)들이 Mathlib으로 학습되며 proof search 성능 향상을 목표로 발전해왔다.
• Gap: classical/constructive 구분이 순수히 axiom dependency라는 논리적 사실을 넘어 proof space에서 측정 가능한 기하학적 구조를 갖는지, 그리고 그것이 neural theorem prover의 실제 성능에 조작적(operational) 영향을 미치는지는 알려져 있지 않았다.
• Why: 이 연구는 axiom of choice라는 순수 논리적·철학적 구분이 학습된 표현 공간에서 정량적으로 측정 가능한 신호로 나타남을 보여줌으로써, 메타수학적 성질과 neural network의 표현 기하학을 연결하고, 나아가 neural theorem prover의 실패를 예측하는 실용적 지표(anomaly score)를 제공한다.
• Approach: Mathlib의 471,260개 선언을 axiom of choice에 대한 transitive dependency로 classical/constructive로 분할하고 dependency graph 상의 거리를 계산한 뒤, constructive proof의 tactic sequence로 self-supervised denoising encoder를 학습하여 classical proof를 이 임베딩 공간에 투영해 anomaly score, reconstruction loss, density-superlevel containment 세 가지 척도로 측정한다.

Achievement

Figure 4. Three measurements, one gradient. Each metric is

1. depth law의 발견: classical proof와 constructive proof 간의 기하학적 분리가 axiom으로부터의 dependency distance에 따라 감소하는 공통된 패턴을 세 가지 독립적 척도(anomaly score, reconstruction loss, density-superlevel containment)에서 일관되게 확인했다(distance 2에서 AUC 0.847, distance 9+에서 구별 불가).
2. one-parameter mixture law로의 통합: 세 측정치의 depth gradient가 개별 현상이 아니라 depth별 mixing weight λd 하나로 설명되는 단일 법칙(Qd = (1−λd)P + λd R)임을 이론적으로 모델링했다.
3. 강건성 검증: 길이, 파일, 저자, 주제(topic) 통제 하에서도 신호가 유지되며, tactic head 기반 encoder뿐 아니라 정규화된 proof source로 학습한 full-source encoder에서도 재현됨을 확인했다.
4. prover 성능과의 조작적 연결: 251개 평가 표본에서 aesop이 constructive 정리를 classical 정리보다 13배 높은 비율로 해결하며, ReProver와 결합 시 격차가 5배로 줄어드는 것을 보였고, geometric anomaly score가 proof length를 넘어서 aesop 실패를 예측함을 입증했다.

How

Figure 4. Three measurements, one gradient. Each metric is

• Lean kernel의 axiom dependence tracking(propext, Quot.sound, Classical.choice)을 이용해 breadth-first search로 471,260개 Mathlib declaration의 dependency graph를 구성하고 classical/constructive로 분할, Classical.choice까지의 최단 dependency chain 길이를 distance로 정의.
• LeanDojo로 tactic 수가 2~200개인 42,355개 traced theorem(classical 31,144, constructive 11,211)을 필터링하고, 각 tactic invocation을 tactic head 시퀀스로 요약(vocabulary 219개).
• constructive proof만으로 self-supervised denoising encoder(masked-token reconstruction)를 학습하고, 이를 이용해 classical proof를 k-NN anomaly score, reconstruction loss, density-superlevel containment(constructive KDE의 S90 superlevel set) 세 가지로 측정.
• depth별 측정치 변화를 mixture model Qd = (1−λd)P + λd R로 모델링.
• 길이, 파일, 저자, 주제 controlled ablation 및 normalised proof source로 학습한 full-source encoder로 재현성 검증.
• 251개 held-out Mathlib theorem에서 aesop 및 ReProver-guided hybrid의 성공률을 classical/constructive로 나누어 비교하고, anomaly score와 proof length를 이용한 실패 예측 회귀분석 수행.

Originality

• axiom of choice라는 순수 논리적·철학적 구분을 kernel-level dependency graph와 neural embedding geometry를 결합해 정량적으로 측정한 최초의 시도로 보인다.
• classical/constructive 구분을 dataset origin이 아닌 논리적 의존성(logical dependence)으로 정의한 held-out population 개념을 one-class/out-of-distribution detection 방법론에 접목시킨 점이 독창적이다.
• 세 개의 독립적 측정치(anomaly score, reconstruction loss, density-superlevel containment)가 하나의 one-parameter mixture law로 통합될 수 있음을 이론적으로 모델링하여 메타수학적 발견의 통일된 해석을 제공한다.
• neural theorem prover의 실패 예측이라는 실용적 응용까지 연결한 점에서 순수 이론적 발견을 조작적(operational) 결과로 확장했다.

Limitation & Further Study

• tactic head 시퀀스만을 이용한 coarse한 proof representation은 구체적 argument, term-level 정보를 버리므로, 관찰된 신호가 axiom of choice 자체의 기하학적 성질인지 tactic 사용 패턴의 대리 변수(proxy)인지 완전히 분리되지 않을 가능성이 있다.
• Mathlib이라는 단일 라이브러리에 국한된 분석으로, 다른 formal library(Coq, Isabelle 등)나 다른 axiom(propext, Quot.sound)에 대한 일반화는 검증되지 않았다.
• classical/constructive 구분이 "기록된 Mathlib 증명"에 한정되며, 정리 자체가 constructive proof를 허용하는지 여부와는 무관하다는 저자들의 명시적 한계가 존재해, 해석에 주의가 필요하다.
• 251개의 비교적 작은 평가 표본에서의 aesop/ReProver 성능 비교는 통계적 검정력이 제한적일 수 있으며, 더 큰 규모의 prover 벤치마크에서의 검증이 필요하다.
• 후속 연구로 term-level 또는 proof-term embedding을 활용한 세밀한 표현, 다른 axiom이나 다른 정리 증명 라이브러리로의 확장, 그리고 anomaly score를 실제 tactic 생성 전략에 통합하는 연구가 제안될 수 있다.

Evaluation

총평: 수학기초론의 오랜 철학적 논쟁인 axiom of choice 문제를 kernel-level dependency tracking과 neural embedding geometry를 결합하여 정량적으로 측정하고, 이를 neural theorem prover 성능과 연결한 참신하고 흥미로운 연구이다. tactic head 기반의 coarse한 표현과 단일 라이브러리 한정이라는 한계가 있으나, 메타수학과 기계학습의 교차점에서 새로운 연구 방향을 제시하는 의미 있는 기여로 평가된다.