DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving

Motivation

• Known: 기존 neural premise selector들은 premise selection을 semantic similarity 기반 retrieval로 프레이밍하여, 후보를 텍스트 임베딩 유사도로 개별적으로 랭킹한다. Hammer 기반 방법, decomposition 기반 방법, retrieval-augmented prover 등 다양한 접근이 존재하지만 모두 의미적 유사성에 크게 의존한다.
• Gap: Semantic similarity 기반 접근은 (P1) 빈도가 높은 foundational lemma가 희귀하고 최신인 premise를 top-K에서 밀어내는 frequency-skewed retrieval, (P2) 각 lemma를 독립적으로 랭킹하여 top-K가 하나의 일관된 proof toolkit을 이루는지 고려하지 못하는 pairwise ranking의 한계, (P3) 대회 문제나 비형식 언어 같은 out-of-distribution 쿼리에서의 성능 저하라는 세 가지 본질적 한계를 가진다. 이는 mathematics가 similarity가 아니라 dependency로 구조화되어 있다는 근본 원인에서 기인하며, 기존 연구들은 이 dependency 신호를 훈련 데이터와 모델 구조 모두에 복원하지 않았다.
• Why: Lean 4 기반 LLM 정리 증명기가 Mathlib4에 새로 기여된 lemma나 협업 formalization 프로젝트에서 전문가가 확립한 정리를 제대로 활용하지 못하는 것은 수십만 개의 declaration 중 적절한 premise를 신뢰성 있게 식별할 방법이 없기 때문이며, 이는 최신·희귀 premise에 도달할 수 있는 premise selection이 형식 수학 자동화 발전에 핵심적임을 의미한다.
• Approach: Mathematics가 dependency로 구조화된다는 통찰에 기반해, Lean Blueprint와 Mathlib4의 dependency 자원을 체계적으로 마이닝하여 훈련 데이터에 구조적 신호를 복원하고, 이를 구조적 이웃 인코더와 group-level contrastive objective로 모델 아키텍처에도 반영하는 DAPS를 설계한다.

Achievement

1. 신규 데이터 자원 구축: 53개 Lean Blueprint 프로젝트에서 3,805개의 수작업 큐레이션된 informal+formal 노드(형식 71.7%, 비형식 28.3%)를 최초로 체계적으로 마이닝하여, Mathlib4에 없는 희귀·연구 수준 premise를 포착하는 자원을 공개한다.
2. 포괄적 Mathlib4 dependency 그래프 추출: 275k+ 노드, 6.5M 엣지로 구성된 typed, heterogeneous, multi-level DAG를 추출하고 15종의 edge type을 정의하여 frequency skew(상위 10% 노드가 in-edge의 56% 차지)와 in/out-degree 비대칭 구조를 정량적으로 분석한다.
3. 4개 평가 벤치마크 공개: 분포 이동 정도가 증가하는 순서로 Mathlib4-Random, Mathlib4-Heldout, DAPS-Collection, DAPS-Blueprint 네 가지 벤치마크를 derive하여 공개한다.
4. DAPS 모델의 성능 우위: Mathlib4-Heldout에서 Recall@32 89.31을 달성하여 강력한 selector인 LeanHammer 대비 11.47 포인트 향상시키고, 모든 out-of-distribution 벤치마크에서도 우위를 유지하며, 작은 retrieval budget에서도 DAPS-Blueprint 상 우위를 지속한다.
5. 다운스트림 성능 개선: DAPS로 선택한 premise를 기존 Lean 검색 엔진 대신 사용함으로써 비형식 IMO-ProofBench에서 세 개의 범용 LLM의 성능을 개선한다.

How

• 구조적 이웃 인코더(structural neighborhood encoder): 각 후보 premise의 텍스트 표현을 dependency graph 상의 위치(의존하는 declaration 종류, connectivity, query와의 관계 등)를 요약한 feature로 augment하여 long-tail collapse(P1)를 완화.
• Group-level contrastive objective: 한 쿼리의 여러 gold premise들을 개별 항목이 아니라 하나의 group으로 query embedding에 가깝게, negative로부터는 멀게 학습시켜, 개별 최근접 이웃이 아니라 jointly-useful한 premise set을 top에 랭킹하도록 학습(P2 대응).
• Mathlib-then-Blueprint 적응 절차: 먼저 방대한 typed Mathlib graph로 사전 학습한 뒤, Blueprint dependency로 continual adaptation을 수행하여 distribution shift(P3)를 흡수.
• 데이터 마이닝 파이프라인: 53개 Lean Blueprint 프로젝트와 Mathlib4 컴파일된 constant graph를 파싱하여 typed, multi-level dependency를 추출하고, 이를 기반으로 4개 벤치마크(Mathlib4-Random, Mathlib4-Heldout, DAPS-Collection, DAPS-Blueprint)를 구성.
• 평가: Recall@K 및 hit@32 지표로 여러 selector(LeanHammer 등)와 비교하고, 세 가지 범용 LLM에 DAPS가 선택한 premise를 투입하여 IMO-ProofBench에서의 증명 성능을 측정.

Originality

• Lean Blueprint 프로젝트를 premise selection을 위한 학습/평가 자원으로 처음 체계적으로 마이닝하여, Mathlib4에 없는 연구 수준 premise를 다루는 새로운 데이터 소스를 발굴했다는 점이 독창적이다.
• Semantic similarity 중심의 기존 premise selection 패러다임에서 벗어나, dependency graph의 구조(타입별 edge, in/out-degree 비대칭, frequency skew)를 명시적으로 모델 입력과 학습 목표에 반영한 최초의 시도로 보인다.
• 개별 lemma가 아닌 premise group 단위의 group-level contrastive objective를 도입하여, 증명에 실제로 함께 쓰이는 premise 집합의 co-usefulness를 학습 신호로 사용한 점이 새롭다.
• 점진적으로 분포 이동이 커지는 4개 벤치마크(Mathlib4-Random → Mathlib4-Heldout → DAPS-Collection → DAPS-Blueprint)를 체계적으로 설계하여 OOD 강건성을 다각도로 측정할 수 있게 한 점도 방법론적 기여이다.

Limitation & Further Study

• 논문 발췌본에서는 DAPS의 구체적인 아키텍처(구조적 이웃 인코더의 feature 설계, group-level contrastive loss의 정확한 수식)와 실험 세부사항(baseline 비교의 통계적 유의성, ablation)이 충분히 제시되지 않아 재현성과 세부 검증이 어렵다.
• Blueprint corpus가 3,805개 노드, 4,651개 엣지로 상대적으로 작고 평균 degree 1.2로 희소하여, 이 자원만으로 일반화 가능한 structural signal을 충분히 학습할 수 있는지에 대한 우려가 있으며, Mathlib-then-Blueprint adaptation의 강건성에 대한 추가 검증이 필요하다.
• IMO-ProofBench 실험이 세 개의 범용 LLM에 국한되어 있어, 다양한 최신 frontier prover(DeepSeek-Prover-V2, Kimina-Prover, Goedel-Prover-V2 등)에 대한 일반화 여부는 추가 검증이 필요하다.
• 향후 연구로 dependency graph를 실시간으로 갱신하며 지속적으로 성장하는 Mathlib4/Blueprint 생태계에 적응하는 online/incremental learning 방향, 그리고 selector와 prover를 공동 최적화하는 end-to-end 학습이 고려될 수 있다.

Evaluation

총평: Dependency 구조라는 수학 고유의 신호를 premise selection에 명시적으로 복원한다는 아이디어가 명확하고 설득력 있으며, 새로운 Blueprint corpus와 다층 Mathlib4 dependency 추출, 그리고 4개의 체계적 벤치마크는 커뮤니티에 실질적으로 기여할 자원이다. 다만 발췌된 내용만으로는 모델 세부사항과 ablation 검증이 부족해 보이며, 전체 논문에서의 상세한 실험 분석이 뒷받침되어야 완성도가 높아질 것이다.