A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation

2025-02-25 · Beibei Xiong, Hangyu Lv, Haojia Shan, Jianlin Wang, Zhengfeng Yang, Lihong Zhi

Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone of mathematics, provides essential tools for analyzing discrete structures and solving optimization problems. However, its inherent complexity makes it particularly challenging for automated theorem proving (ATP) for combinatorial identities. To address this, we manually construct LeanComb, combinatorial identities benchmark in Lean, which is, to our knowledge, the first formalized theorem proving benchmark built for combinatorial identities. We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for tactic prediction. By utilizing ATG4CI, we generate a LeanComb-Enhanced dataset comprising 260K combinatorial identities theorems, each with a complete formal proof in Lean, and experimental evaluations demonstrate that models trained on this dataset can generate more effective tactics, thereby improving success rates in automated theorem proving for combinatorial identities.

📄 PDF Abstract BibTeX arXiv:2502.17840

Code (0)

등록된 구현이 없습니다.

Tasks

Automated Theorem ProvingLanguage ModelingLanguage ModellingLarge Language Model

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

2026-05-06 · Beibei Xiong, Hangyu Lv, Junqi Liu, Yisen Wang 외 arxiv

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-Zeilberge…

A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving

2019-11-05 · Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead 외

Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, how…

Automated Theorem Proving Deep Reinforcement Learning reinforcement-learning Reinforcement Learning+1

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

2026-01-26 · Qiyuan Xu, Xiaokun Luan, Renxi Wang, Joshua Ong Jun Leang 외 arxiv

Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification frequently encounters hard VCs that existin…

MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?

2025-06-06 · Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo 외

Numerous theorems, such as those in geometry, are often presented in multimodal forms (e.g., diagrams). Humans benefit from visual reasoning in such settings, using diagrams to gain intuition and guide the proof process.…

Automated Theorem Proving Visual Reasoning

ATG: Benchmarking Automated Theorem Generation for Generative Language Models

2024-05-05 · Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang 외

Humans can develop new theorems to explore broader and more complex mathematical results. While current generative language models (LMs) have achieved significant improvement in automatically proving theorems, their abil…

Automated Theorem Proving Benchmarking