12 papers
Enabling Token-wise Importance Sampling in Off-Policy RLVR with Proximal KL Regularization
Hao Bai, Jiarui Yao, Tong Zhang
Off-policy data in reinforcement learning with verifiable rewards (RLVR) can arise from asynchronous generation, rollout-training mismatch, and response reuse. Token-wise importanc…
Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation
Ruida Wang, Rui Pan, Pengcheng Wang +2
Enhancing the formal math reasoning capabilities of Large Language Models (LLMs) has become a key focus in both mathematical and computer science communities in recent years. While…
AgentSPEX: An Agent SPecification and EXecution Language
Pengcheng Wang, Jerry Huang, Jiarui Yao +7
Language-model agent systems commonly rely on reactive prompting, in which a single instruction guides the model through an open-ended sequence of reasoning and tool-use steps, lea…
What Papers Don't Tell You: Recovering Tacit Knowledge for Automated Paper Reproduction
Lehui Li, Ruining Wang, Haochen Song +8
Automated paper reproduction -- generating executable code from academic papers -- is bottlenecked not by information retrieval but by the tacit knowledge that papers inevitably le…
PhysProver: Advancing Automatic Theorem Proving for Physics
Hanning Zhang, Ruida Wang, Rui Pan +3
The combination of verifiable languages and LLMs has significantly influenced both the mathematical and computer science communities because it provides a rigorous foundation for t…
Future-KL Regularized GRPO: Process-Level Credit Assignment from -Divergence Regularization
Jiarui Yao, Ruida Wang, Hao Bai +1
Group Relative Policy Optimization (GRPO) is widely used for critic-free Large Language Model (LLM) post-training, but its KL regularization is usually implemented as a local loss-…
Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4
Yuxin Li, Minghao Liu, Ruida Wang +6
We present **Lean4PHYS**, a comprehensive reasoning framework for college-level physics problems in Lean4. **Lean4PHYS** includes *LeanPhysBench*, a college-level benchmark for for…
ERA: Transforming VLMs into Embodied Agents via Embodied Prior Learning and Online Reinforcement Learning
Hanyang Chen, Mark Zhao, Rui Yang +15
Recent advances in embodied AI highlight the potential of vision language models (VLMs) as agents capable of perception, reasoning, and interaction in complex environments. However…
GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
Ruida Wang, Jiarui Yao, Rui Pan +2
Solving math problems through verifiable languages such as Lean has significantly impacted both the mathematics and computer science communities. Current state-of-the-art models ar…
Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability
Ruida Wang, Yuxin Li, Yi R. Fung +1
Enhancing the mathematical reasoning capabilities of LLMs has garnered significant attention in both the mathematical and computer science communities. Recent works have made subst…
FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
Jiarui Yao, Ruida Wang, Tong Zhang
Large Language Models (LLMs) have displayed astonishing abilities in various tasks, especially in text generation, classification, question answering, etc. However, the reasoning a…
MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
Ruida Wang, Rui Pan, Yuxin Li +6
Solving mathematical problems using computer-verifiable languages like Lean has significantly impacted the mathematical and computer science communities. State-of-the-art methods u…