Publications
Research papers and technical reports from the ReasLab team
Optimization for Machine Learning and Artificial Intelligence
- Accelerating LLM Pre-Training through Flat-Direction Dynamics Enhancement
- Non-Asymptotic Global Convergence of PPO-Clip
- A Memory Efficient Randomized Subspace Optimization Method for Training Large Language Models
- Enhancing Zeroth-order Fine-tuning for Language Models with Low-rank Structures
- Accelerated Natural Gradient Method for Parametric Manifold Optimization
- An Improved Finite-time Analysis of Temporal Difference Learning with Deep Neural Networks
- Riemannian Natural Gradient Methods
- Convergence analysis of an adaptively regularized natural gradient method
- Convergence Analysis of Stochastic Gradient Descent with MCMC Estimators
- Gauss-Newton Temporal Difference Learning with Nonlinear Function Approximation
- A Stochastic Composite Augmented Lagrangian Method For Reinforcement Learning
- An Efficient Fisher Matrix Approximation Method for Large-Scale Neural Network Optimization
- A Near-Optimal Primal-Dual Method for Off-Policy Learning in CMDP
- Sketchy Empirical Natural Gradient Methods for Deep Learning
- A stochastic trust region framework for policy optimization
- Structured Stochastic Quasi-Newton Methods for Large-Scale Optimization Problems
- Sharper Convergence Guarantees for Federated Learning with Partial Model Personalization
- Adaptive Low Rank Approximation for State Aggregation of Markov Chain
- Toward Solving 2-TBSG Efficiently
Learning-based Optimization (Learn to Optimize)
- LMask: Learn to Solve Constrained Routing Problems with Lazy Masking
- OptMATH: A Scalable Bidirectional Data Synthesis Framework for Optimization Modeling
- ODE-based learning to optimize
- Accelerating Optimization via Differentiable Stopping Time
- A Monte Carlo Policy Gradient Method with Local Search for Binary Optimization
- Reinforcement Learning for Heterogeneous DAG Scheduling with Weighted Cross-Attention
- Learning the Quadratic Assignment Problem with Warm-Started MCMC Finetuning and Cross-Graph Attention
- Constructing Industrial-Scale Optimization Modeling Benchmark
- PEARL: Interactive Optimization Modeling with Tool-Integrated Agentic Reinforcement Learning
- Optimization Modular Modeling for Statistical Learning
AI for Mathematics
- M2F: Automated Formalization of Mathematical Literature at Scale
- SITA: A Framework for Structure-to-Instance Theorem Autoformalization
- Formalization of Algorithms for Optimization with Block Structures
- Formalization of Convergence Rates of Four First-order Algorithms for Convex Optimization
- Tree-Based Premise Selection for Lean4
- Introduction to Mathematical Formalization Based on Lean
- Formalization of Optimality Conditions for Smooth Constrained Optimization Problems
- Translating Informal Proofs into Formal Proofs Using a Chain of States
- Advancing Mathematical Research via Human-AI Interactive Theorem Proving
- Construction-Verification: A Benchmark for Formalizing Applied Mathematics in Lean 4
- OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
- Directed Multi-Relational GCNs for Premise Selection