Seminar by Dr. Zhenguo Li, Huawei Noah's Ark AI Theory Lab

Large language models (LLMs) have revolutionized numerous fields, yet automated theorem proving remains a formidable frontier, testing the limits of AI's reasoning capabilities. In this talk, we explore groundbreaking research at the intersection of LLMs and formal reasoning, spotlighting three innovative approaches: LEGO-Prover (ICLR 2024 oral), POETRY, and ProofAug. LEGO-Prover challenges conventional theorem proving by introducing a growing library of verified lemmas. Unlike static approaches, it modularly constructs proofs, enabling LLMs to leverage existing skills and generate new ones dynamically. This iterative expansion of the skill library not only bridges the gap between human and formal proofs but also boosts performance on the miniF2F benchmark, achieving a 9% increase in the valid set pass rate and generating over 20,000 reusable skills. POETRY (NeurIPS 2024) rethinks the proof search strategy. Instead of relying on short-sighted heuristics, it recursively decomposes theorems into hierarchical sketches in the Isabelle prover. By deferring detailed proofs to lower levels, POETRY navigates complex proofs more effectively, achieving a 5.1% success rate improvement on miniF2F and extending the maximum proof length from 10 to 26 steps. Finally, ProofAug (ICML 2025) optimizes the synergy between LLMs and automated theorem provers. Through fine-grained analysis of proof structures, it integrates automation tools at multiple granularities, enhancing the efficiency of neural theorem provers. On the miniF2F-test benchmark, ProofAug, combined with a mixed prompting strategy, outperforms prior state-of-the-art methods by achieving a 66.0% pass rate with fewer model queries. Collectively, these works showcase the transformative potential of LLMs in formal reasoning. As AI continues to evolve, mathematical theorem proving emerges not only as a rigorous testbed for advanced reasoning but also as a catalyst for new discoveries in mathematics and beyond.

Zhenguo Li is the director of Huawei Noah's Ark AI Theory Lab, and an Adjunct Professor in the department of computer science and engineering, The Hong Kong University of Science and Technology. He was an associate research scientist in the department of electrical engineering, Columbia University. He received BS and MS degrees in mathematics at Peking University, and PhD degree in machine learning at The Chinese University of Hong Kong, under the supervision of Prof. Xiaoou Tang. His research interests include machine learning and artificial intelligence, with representative works such as DeepFM for deep learning for recommendation, Meta-SGD for meta-learning for few-shot learning, PixArt-α for AIGC, and LEGO-Prover for automated theorem proving. He is also a pioneer in AutoML and deep learning for data compression, which have been successfully deployed in autonomous driving and Huawei Pura 70 Ultra flagship smart phones for satellite image communication, respectively. He is selected as AI 2000 Most Influential Scholars (by Aminer) and Top 2% Most-cited Scientists (by Stanford University), and has been frequently serving as an area chair for NeurIPS, ICLR and ICML.