11 papers
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…
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-…
Code as Agent Harness
Xuying Ning, Katherine Tieu, Dongqi Fu +39
Recent large language models (LLMs) have demonstrated strong capabilities in understanding and generating code, from competitive programming to repository-level software engineerin…
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…
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…
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…