7 papers
A Proof of the Dittert Conjecture in Dimension 4 via an Exact Constrained Sum-of-Squares Certificate
Jinhui Li, Beibei Xiong, Zhengfeng Yang
The Dittert conjecture states that the Dittert functional on nonnegative matrices whose entries sum to is uniquely maximized by the uniform matrix. We prove the con…
Richer Representations for Neural Algorithmic Reasoning via Auxiliary Reconstruction
Jiafu Huang, Chao Peng, Chenyang Xu +7
Neural algorithmic reasoning has emerged as a popular research direction. It aims to train neural networks to mimic the step-by-step behavior of classical rule-based algorithms. Mo…
From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates
Ruobing Zuo, Hanrui Zhao, Gaolei He +2
Automated proving of polynomial inequalities is a fundamental challenge in automated mathematical reasoning, where rich algebraic structure and a rapidly growing certificate search…
Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
Beibei Xiong, Hangyu Lv, Junqi Liu +5
Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Sym…
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
Shuming Shi, Ruobing Zuo, Gaolei He +3
Automated theorem proving (ATP) is one of the most challenging mathematical reasoning tasks for Large Language Models (LLMs). Most existing LLM-based ATP methods rely on supervised…
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
Beibei Xiong, Hangyu Lv, Haojia Shan +3
Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematica…