activity
20242026
collaborators

6 papers

cs.LO2026

MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics

Xinyu Liu, Zixuan Xie, Amir Moeini +5

While the ecosystem of Lean and Mathlib has enjoyed celebrated success in formal mathematical reasoning with the help of large language models (LLMs), the absence of many folklore…

cs.LG2025

The ODE Method for Stochastic Approximation and Reinforcement Learning with Markovian Noise

Shuze Daniel Liu, Shuhang Chen, Shangtong Zhang

Stochastic approximation is a class of algorithms that update a vector iteratively, incrementally, and stochastically, including, e.g., stochastic gradient descent and temporal dif…

cs.LG2025

Efficient Policy Evaluation with Safety Constraint for Reinforcement Learning

Claire Chen, Shuze Daniel Liu, Shangtong Zhang

In reinforcement learning, classic on-policy evaluation methods often suffer from high variance and require massive online data to attain the desired accuracy. Previous studies att…

cs.LG2025

Doubly Optimal Policy Evaluation for Reinforcement Learning

Shuze Daniel Liu, Claire Chen, Shangtong Zhang

Policy evaluation estimates the performance of a policy by (1) collecting data from the environment and (2) processing raw data into a meaningful estimate. Due to the sequential na…

cs.LG2024

Efficient Multi-Policy Evaluation for Reinforcement Learning

Shuze Daniel Liu, Claire Chen, Shangtong Zhang

To unbiasedly evaluate multiple target policies, the dominant approach among RL practitioners is to run and evaluate each target policy separately. However, this evaluation method…

cs.LG2024

Efficient Policy Evaluation with Offline Data Informed Behavior Policy Design

Shuze Liu, Shangtong Zhang

Most reinforcement learning practitioners evaluate their policies with online Monte Carlo estimators for either hyperparameter tuning or testing different algorithmic design choice…