Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.04472 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910194259197952 |
|---|---|
| author | Xiong, Beibei Lv, Hangyu Liu, Junqi Wang, Yisen Chen, Shaoshi Wang, Jianlin Yang, Zhengfeng Zhi, Lihong |
| author_facet | Xiong, Beibei Lv, Hangyu Liu, Junqi Wang, Yisen Chen, Shaoshi Wang, Jianlin Yang, Zhengfeng Zhi, Lihong |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_04472 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs Xiong, Beibei Lv, Hangyu Liu, Junqi Wang, Yisen Chen, Shaoshi Wang, Jianlin Yang, Zhengfeng Zhi, Lihong Machine Learning 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. |
| title | Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs |
| topic | Machine Learning |
| url | https://arxiv.org/abs/2605.04472 |