OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
C. Li, Y. Nie, Z. Ming, G. Zhang, K. Yuan, Z. Wen
Learn with Optimization, Optimize with Learning.

MeLOn Lab explores the intersection of machine learning and optimization, with the goal of developing principled, efficient, and scalable methods for intelligent systems. Our research spans AI for Mathematics, distributed and decentralized learning, efficient training and inference optimization for large language models, as well as optimization theory and signal processing. We are particularly interested in how optimization can improve the efficiency, reliability, and understanding of modern learning systems, and how machine learning can, in turn, help solve challenging mathematical and optimization problems. By combining theoretical foundations with practical system design, we aim to advance both the science of learning and the development of impactful real-world applications.
Memory- and computation-efficient methods for pre-training and post-training large language models, including subspace and low-rank optimization, sparse attention, and mixture-of-experts training.
Algorithms and theory for optimization over networks and directed graphs, federated learning, communication compression, and bilevel optimization with provable convergence and linear speedup.
Foundational analysis of stochastic and nonconvex optimization, gradient tracking and normalization, lower bounds, and robust methods at the intersection of optimization and signal processing.
Machine learning for mathematical reasoning and optimization, including formal theorem proving, learning-to-optimize, and automated formulation and heuristic discovery.
C. Li, Y. Nie, Z. Ming, G. Zhang, K. Yuan, Z. Wen
R. Xin, Z. Zheng, Y. Nie, K. Yuan, X. Xiao
R. Hu, Y. Cao, B. Kong, M. Sun, K. Yuan