A Complete Lean Formalization of a TCS Proving Benchmark

Motivation

• Known: Lean/mathlib 환경에서 실행 가능한 자료구조와 알고리즘(예: 힙, 트립, 세그먼트 트리)에 대한 형식 검증은 알려진 연구 주제이며, executable implementation과 추상 수학적 명세 사이의 간극을 메우는 abstraction relation과 inductive invariant 기법이 검증 알고리즘 분야에서 표준적으로 쓰인다.
• Gap: 기존에는 Dijkstra의 shortest-path algorithm과 Kruskal의 minimum-spanning-tree algorithm처럼 공개된 명세는 간결하지만 실제 증명을 완결하려면 heap membership, priority invariant, disjoint-set/forest connectivity invariant, cut-property exchange argument 같은 중간 불변량이 필요하다는 점에서, 이 벤치마크에 대한 완전하고 공개적으로 검증 가능한 해가 부재했다.
• Why: 이 벤치마크는 ICML 2026 AI for Math Workshop Track 2의 공식 평가 기준이 되는 것으로 보이며, TCS 알고리즘의 executable-to-abstract 증명 패턴을 명시적으로 기록함으로써 향후 AI 기반 정리 증명 시스템의 훈련/평가 기준선(baseline) 및 라이브러리 인터페이스 설계에 참고 자료로 활용될 수 있다.
• Approach: 저자는 CSLib과 mathlib 환경에서 제공된 Def 파일을 변경하지 않고, executable 자료구조와 수학적 명세를 잇는 abstraction relation과 강화된 inductive invariant를 정의하는 표준 refinement 패턴을 통해 29개 챌린지 파일 전체를 증명했다.

Achievement

1. 완전한 벤치마크 해결: treap, segment tree, binary heap, Dijkstra, Kruskal MST를 아우르는 29개 챌린지 파일(500점)을 sorry/admit 없이 제공된 Lean 4.28.0, CSLib, mathlib 환경에서 컴파일되도록 증명하고, 제공된 정의 파일은 전혀 수정하지 않았다.
2. Dijkstra를 위한 boundary invariant 설계: min-heap 순서, no-duplicate, source distance zero, upper-bound, settled-exact, boundary invariant(6개 조건)로 구성된 강화된 invariant를 통해 shortest-path witness argument로 추출된 정점의 exactness를 증명했다.
3. Kruskal을 위한 cut-property exchange 증명: union-find 상태와 forest reachability를 잇는 abstraction relation(findUF(x)=findUF(y) ⇔ ReachF(x,y))과 safe-forest invariant를 통해 spanning tree의 acyclicity, connectedness, optimality(minimality)를 모두 도출했다.
4. 재사용 가능한 증명 패턴 및 라이브러리 인터페이스 제시: heap의 list model, membership equivalence, no-duplicate preservation, priority congruence/update lemma 등 CSLib에 제안 가능한 인터페이스를 구체적으로 기술했다.

How

• executable 자료구조(binary heap, union-find forest 등)에 대해 수학적 명세와 연결하는 abstraction relation을 정의(예: 힙 멤버십을 이진 트리 기반 list model로 표현, union-find representative 동일성을 forest reachability와 동치로 표현).
• 직접적인 executable recursion에 대한 induction만으로는 최종 정리에 부족하므로, 각 재귀 단계에서 보존되는 강화된 invariant를 도입하고 초기 상태에서 인스턴스화해 공개 정리를 도출.
• Dijkstra: heap membership, no-duplicate preservation, priority-update heap preservation, boundary invariant, shortest-path witness lemma를 조합해 strong induction으로 정확성 증명.
• Kruskal: union-find semantic tracking, selected-forest acyclicity, cut lightness from sorted scan, spanning-tree exchange, weight-sum comparison을 조합해 safe-forest invariant 기반으로 minimality(cut property exchange argument)를 증명.
• treap과 segment tree는 probability decomposition/expected-depth summation, coverage-interval semantics 등 지역적(local) 구조 귀납으로 처리.

Originality

• 특정 워크숍의 공식 벤치마크(29개 파일, 500점) 전체를 완결적으로 형식화한 최초의 공개 아티팩트로 보이며, 단순 개별 알고리즘 검증이 아니라 벤치마크 전체를 아우르는 통합적 증명 아키텍처를 제시했다.
• Dijkstra의 boundary invariant와 Kruskal의 safe-forest exchange invariant를 명시적 수식(예: Heap(q, dist) ∧ NoDup(q) ∧ ... 형태의 conjunction, SpanningTree exchange 부등식)으로 정형화하여 textbook 증명과 Lean 형식 증명 사이의 간극을 명시적으로 메웠다.
• CSLib 기반의 재사용 가능한 라이브러리 인터페이스(heap list model, union-find tracking invariant 등)를 제안하여 향후 유사 벤치마크나 AI 정리 증명 훈련에 활용될 수 있는 실용적 기여를 담았다.

Limitation & Further Study

• 본 논문은 공개된 Phase 1 벤치마크만을 다루며, 실제 워크숍의 최종 평가에 사용될 수 있는 non-public 또는 확장된 Phase 2/3 문제에 대한 일반화 가능성은 논의되지 않는다.
• 증명 자동화나 AI 모델의 성능 평가와 직접 연관된 실험적 비교(예: LLM이 이 벤치마크를 얼마나 풀 수 있는지)는 포함되어 있지 않아, 벤치마크로서의 실제 난이도·변별력에 대한 정량적 근거가 부족하다.
• Figure나 시각적 자료가 전혀 제공되지 않아 증명 구조나 invariant 관계를 직관적으로 파악하기 어려우며, 후속 연구로 증명 시간, 코드 크기, 재사용성 등 정량적 지표를 제공하면 벤치마크 난이도 평가에 도움이 될 것이다.
• 단일 저자에 의한 수작업 형식화로 보이며, 다른 형식화 방식(예: 다른 invariant 선택)과의 비교나 대체 가능한 접근법에 대한 논의가 없다.

Evaluation

총평: 공개 TCS 증명 벤치마크를 완전히, sorry 없이 해결한 견고한 엔지니어링 성과를 담은 워크숍용 아티팩트 논문으로, 학술적 새로움보다는 실용적 참고 자료로서의 가치가 크다.