Chenyi Li

Chenyi Li

EmailGoogle ScholarGitHubORCID

I am a third-year Ph.D. student in Computational Mathematics at the School of Mathematical Sciences, Peking University, advised by Prof. Zaiwen Wen. I received my B.S. degree in Information and Computing Science from the School of Mathematical Sciences, Peking University, in 2024.

I am a member of the Elite Ph.D. Program in Applied Mathematics and the Elite Program in Mathematics at the School of Mathematical Sciences, Peking University. My email is lichenyi@stu.pku.edu.cn.

My research interests span large language model reasoning, formal theorem proving, and optimization.

  • LLM ReasoningReinforcement learning and verifier-guided training to improve the reliability and diversity of reasoning in large language models.
  • Formal Theorem ProvingLean-based theorem proving, autoformalization, and the formalization of mathematical theories and algorithms in applied mathematics.
  • OptimizationThe design and analysis of optimization algorithms, and the development of optimization-inspired methods for large language models.

News

Our paper A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization was published in Journal of Scientific Computing.

Our papers SetPO and OptProver have been accepted to ICML 2026.

Our paper Formalization of algorithms for optimization with block structures was published in Science China Mathematics.

Our paper SITA has been accepted to AAAI 2026.

Our work on formalizing convergence rates of first-order optimization algorithms was published in the Journal of Automated Reasoning.

Education

Selected publications

* denotes equal contribution.

LLM Reasoning and Formal Theorem Proving

  1. OptBench accuracy comparison under different continual-training settings, with Pass@1 and Pass@32 results

    OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

    Chenyi Li*, Yanchen Nie*, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

    The 43rd International Conference on Machine Learning, 2026

    arXivPaperCode
  2. GRPO
    GRPO trajectory embeddings
    SetPO
    SetPO trajectory embeddings
    Shared training-step color scale, from 0 to 10k

    SetPO: Set-Level Policy Optimization for Diversity-Preserving LLM Reasoning

    Chenyi Li*, Yuan Zhang*, Bo Wang, Guoqing Ma, Wei Tang, Haoyang Huang, Nan Duan

    The 43rd International Conference on Machine Learning, 2026

    arXivPaperCode
  3. Preview for CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

    CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

    Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen

    arXiv preprint, 2026

    arXivPaperCode
  4. Preview for SITA: A Framework for Structure-to-Instance Theorem Autoformalization

    SITA: A Framework for Structure-to-Instance Theorem Autoformalization

    Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen

    Proceedings of the AAAI Conference on Artificial Intelligence, 2026

    arXivPaperCode
  5. Preview for A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

    A Human-AI Collaborative Workflow for Mathematical Discovery: A Case Study in Grover-Compatible Riemannian Optimization

    Chenyi Li, Zhijian Lai, Dong An, Jiang Hu, Zaiwen Wen

    Journal of Scientific Computing, 109:74, 2026

    arXivPaper

Formalization of Optimization

  1. Schematic of Lean formalization: convexity and smoothness to convergence proofs

    Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization

    Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, Zaiwen Wen

    Journal of Automated Reasoning, 69(4):28, 2025

    arXivPaperCode
  2. Schematic of Lean formalization for BCD and ADMM convergence

    Formalization of algorithms for optimization with block structures

    Chenyi Li, Zichen Wang, Yifan Bai, Yunxi Duan, Yuqing Gao, Pengfei Hao, Zaiwen Wen

    Science China Mathematics, 2026

    arXivPaperCode
  3. Schematic of Lean formalization for KKT optimality conditions

    Formalization of Optimality Conditions for Smooth Constrained Optimization Problems

    Chenyi Li, Shengyang Xu, Chenyang Sun, Liangqi Zhou, Zaiwen Wen

    arXiv preprint, 2025

    arXivCode

Optimization

  1. Training loss comparison for ANGD, NGD, Adam, and SGD on the Burgers equation; Figure 1, left panel

    Accelerated Natural Gradient Method for Parametric Manifold Optimization

    Chenyi Li*, Shuchen Zhu*, Zhonglin Xie, Zaiwen Wen

    arXiv preprint, 2025

    arXiv