用数学方法+大模型，自动证明组合恒等式
Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
- 将威尔夫-齐勒伯格方法转化为可执行的证明框架
- 在经典恒等式测试集上达34%成功率，优于多个基线模型
- 适合想自动化证明组合恒等式的研究人员
基于大模型的组合恒等式自动证明面临长程证明规划难题，且无约束搜索易爆炸。符号方法如威尔夫-齐勒伯格（WZ）方法可通过构造辅助函数并验证其满足特定递推关系来实现机械化证明。我们提出WZ-LLM，一种神经符号框架，将WZ证明计划转化为Lean 4中的可执行证明草图，并利用大模型证明器解决生成的机器可验证子目标。通过专家验证迭代的Lean内核验证自举循环训练专用的WZ-Prover，再经DAPO优化改进。实验显示，WZ-LLM在LCI-Test（100个经典组合恒等式）上达到34%的证明成功率，优于DeepSeek-V3和Goedel-Prover-V2等强基线，在CombiBench和PutnamBench-Comb上也持续提升。结果表明该框架兼具双重优势：对超出WZ适用范围的恒等式实现更优直接证明，以及在使用WZ草图引导专用证明器时显著提升端到端成功率。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。