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

TL;DR

This paper introduces WZ-LLM, a neuro-symbolic framework that automates formal proofs of combinatorial identities by combining Wilf-Zeilberger methods with large language models, achieving significant success rates.

Contribution

The paper presents a novel neuro-symbolic approach that integrates WZ proof plans with LLM-based provers, improving automation and success rates in formal combinatorial proofs.

Findings

WZ-LLM achieves a 34% proof success rate on LCI-Test.

Outperforms baselines like DeepSeek-V3 and Godel-Prover-V2.

Provides improved proof success for identities beyond WZ scope.

Abstract

Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.