Automated Formal Proofs of Combinatorial Identities via Wilf–Zeilberger Guidance and LLMs

Motivation

• Known: LLM 기반 automated theorem proving(ATP)은 tactic 단위 탐색(BFS/MCTS)이나 whole-proof 생성 방식으로 발전해왔으며, WZ method, creative telescoping, Gröbner basis 등 기호적 계산 기법은 조합항등식을 기계적으로 검증 가능한 형태로 환원하는 데 오랫동안 사용되어 왔다.
• Gap: 조합항등식 증명은 long-horizon proof planning을 요구하는데, 원칙적인 증명 계획 없이는 LLM 기반 prover의 탐색이 combinatorial explosion에 빠지며, 기존 WZ 등 symbolic method의 출력은 Lean 등 interactive proof assistant로 직접 변환되지 않아 telescoping 논증, 경계 조건, 정규화, non-vanishing 조건 등을 다시 형식화해야 하는 문제가 있다. 또한 Lean 조합수학 분야는 데이터 부족(data scarcity) 문제도 겪고 있다.
• Why: 조합수학(combinatorics)은 ATP에서 가장 어려운 영역 중 하나로 꼽히며, 조합항등식은 그 안에서 근본적이고 편재하는 명제 부류이기 때문에 이를 기계 검증 가능하게 자동화하는 것은 재사용 가능한 검증 라이브러리 구축과 형식 증명 개발의 인적 노력 절감에 핵심적인 목표이다.
• Approach: WZ 방법의 recurrence 및 boundary/initial condition 합성 구조를 Lean 4의 실행 가능한 proof sketch(recurrence lemma와 관련 obligation)로 변환하고, 이 하위 목표들을 LLM 기반 prover가 처리하도록 하는 neuro-symbolic 프레임워크를 구성했으며, 데이터 부족 문제를 해결하기 위해 Lean-kernel-verified bootstrapping loop와 DAPO 기반 강화학습 정제로 전용 WZ-Prover를 학습시켰다.

Achievement

Figure 2. Lean InfoView output of the wz prove tactic. The tactic automatically invokes symbolic computation and the tra

1. WZ-LLM 프레임워크 제안: WZ 증명 계획을 Lean 4의 executable proof sketch로 변환하고 LLM prover로 하위 목표를 해결하는 neuro-symbolic 파이프라인을 구축.
2. Lean-verified 데이터셋 및 전용 prover 학습: 307개의 고전 교재 조합항등식을 수작업 formalization한 seed corpus로 cold-start SFT를 수행하고, expert-verified iteration과 DAPO refinement를 거쳐 WZ-Prover를 학습.
3. 벤치마크 성능 개선: 새로 구축한 LCI-Test(고전 조합항등식 100개)에서 34%의 end-to-end 증명 성공률을 달성해 DeepSeek-V3, Goedel-Prover-V2 등 강력한 baseline을 능가했으며, symbolic-only baseline이 실패한 5개 항등식도 증명. CombiBench와 PutnamBench-Comb에서도 일관된 성능 향상을 보임.

How

Figure 1. Overview of WZ-LLM. (A) Symbolic decomposition. Given combinatorial-identity statements, the symbolic engine c

• WZ method의 핵심 개념인 F(n,k)와 auxiliary term G(n,k)로 구성된 WZ-pair, 그리고 WZ equation(식 2)을 활용해 항등식을 recurrence와 boundary/initial condition으로 분해.
• 이 분해 결과를 Lean 4의 executable proof sketch(즉, recurrence lemma와 관련 machine-checkable subgoal)로 자동 변환하는 symbolic decomposition 모듈 구성.
• 307개의 고전 조합항등식을 수작업 formalization하여 cold-start SFT를 위한 고품질 seed corpus 마련.
• Lean-kernel-verified bootstrapping loop를 통해 검증된 모델 출력(WZ-sketch lemma 및 WZ 미적용 항등식의 direct proof)만 training corpus에 추가하고 proving-task pool에서 제거하며, 미검증 시도는 후속 iteration을 위해 보존하는 expert-verified iteration 절차 수행.
• cold-start SFT, iterative training, DAPO(Dynamic Sampling Policy Optimization) 기반 강화학습 정제를 거쳐 전용 WZ-Prover 학습.
• LCI-Test(100개 고전 조합항등식), CombiBench, PutnamBench-Comb에서 성능 평가.

Originality

• WZ method라는 고전적 symbolic 알고리즘의 증명 구조(recurrence + boundary condition)를 Lean 4의 executable proof sketch로 변환하는 최초의 시도로, symbolic method의 출력이 interactive proof assistant로 직접 연결되지 않던 기존 한계를 해결.
• symbolic decomposition과 LLM 기반 prover를 결합한 neuro-symbolic 설계를 통해, WZ가 커버하지 못하는 항등식에는 direct proving으로 대응하고 WZ가 적용 가능한 경우 sketch로 탐색 공간을 제약하는 상호보완적 구조를 제시.
• Lean-kernel-verified bootstrapping loop와 expert-verified iteration을 결합한 데이터 확장 전략으로 조합수학 분야의 Lean 데이터 부족 문제를 해결.

Limitation & Further Study

• WZ method 자체가 hypergeometric term에 한정된 기법이므로, 그 적용 범위 밖의 항등식에 대해서는 WZ sketch 없이 direct proving에만 의존해야 하는 근본적 한계가 있음.
• 307개의 seed corpus는 수작업 formalization에 의존하므로 확장성(scalability) 측면에서 사람 개입 비용이 여전히 존재.
• 34%라는 성공률 자체는 아직 실용적 수준의 완전 자동화에는 미치지 못하며, 더 어려운 조합수학 정리(예: 비고전적, 비합산형 항등식)로의 일반화 가능성에 대한 추가 검증이 필요.
• 후속 연구로 WZ 외의 다른 symbolic 알고리즘(creative telescoping의 일반화, q-analogue 등)과의 결합, 더 큰 벤치마크로의 확장이 기대됨.

Evaluation

총평: 고전적 symbolic 증명 기법인 WZ method와 LLM 기반 formal prover를 결합한 실용적이고 독창적인 neuro-symbolic 접근으로, 조합항등식 자동 형식 증명이라는 어려운 문제에서 명확한 성능 향상을 보여준 견실한 연구이다.