组合恒等式的形式化证明是自动定理证明领域中的一项重要挑战。此类证明往往需要复杂的长程规划，而无约束的证明搜索空间会迅速膨胀，使得现有基于大语言模型的定理证明方法在该方向上的表现仍较为有限。如何有效结合符号计算的结构化推理能力与大语言模型的灵活生成能力，实现组合恒等式的自动化、机器可验证证明，是数学机械化与人工智能交叉领域亟待解决的重要问题。

    针对这一挑战，中国科学院数学与系统科学研究院数学机械化实验室陈绍示研究员、支丽红研究员，联合华东师范大学杨争峰教授、河南大学王建林副教授，以及研究生熊贝贝、吕航宇、刘俊杞、王艺森，提出了 WZ-LLM：一种融合 Wilf–Zeilberger 方法与大语言模型的神经符号证明框架，用于在 Lean 4 定理证明器中自动完成组合恒等式的形式化证明。

    WZ-LLM 将经典 Wilf–Zeilberger 方法所提供的结构化证明思路与大语言模型的自动证明能力相结合。该框架首先利用 WZ 方法将目标恒等式分解为可执行的证明骨架，再由专门训练的证明模型 WZ-Prover自动完成递推关系、边界条件以及非零性约束等关键子目标的形式化证明。对于难以直接由 WZ 方法覆盖的恒等式，模型还能够尝试进行端到端形式化证明，从而提升系统的适用范围和自动化能力。

    实验结果表明，在包含 100 个经典组合恒等式的 LCI-Test基准测试集上，WZ-LLM 实现了 34%的端到端证明成功率，显著优于 DeepSeek-V3、Goedel-Prover-V2 以及 Gemini 系列模型等强基线方法。该工作展示了符号计算方法与大语言模型深度结合在形式化数学证明中的潜力，为组合恒等式的自动化证明提供了一条新的技术路径。

    相关论文已被机器学习顶级会议 ICML 2026接收为 spotlight论文。

Publication:

ICML 2026

https://arxiv.org/abs/2605.04472

Code:

https://github.com/BeibeiX0/WZ-LLM

Author:

Beibei Xiong 

School of Software Engineering, East China Normal University, Shanghai, China

Hangyu Lv

School of Software Engineering, East China Normal University, Shanghai, China

Junqi Liu

Institute of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China

Yisen Wang

Institute of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China

Shaoshi Chen

Institute of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China

Jianlin Wang

School of Computer and Information Engineering, Henan University, Kaifeng, China

Zhengfeng Yang

School of Software Engineering, East China Normal University, Shanghai, China

Correspondence to: Zhengfeng Yang <zfyang@sei.ecnu.edu.cn>.

Lihong Zhi

Institute of Mathematics and Systems Science, Chinese Academy of Sciences, Beijing, China