4 papers
Learning with a Single Rollout via Pass@k Policy Optimization
Fengdi Che, Yang Liu, Lei Yu +4
Group Relative Policy Optimization (GRPO) typically requires multiple rollouts per prompt to estimate relative credit, incurring substantial sampling cost and exacerbating training…
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
Lingfei Zeng, Fengdi Che, Xuhan Huang +4
Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specificatio…
A Tutorial: An Intuitive Explanation of Offline Reinforcement Learning Theory
Fengdi Che
Offline reinforcement learning (RL) aims to optimize the return given a fixed dataset of agent trajectories without additional interactions with the environment. While algorithm de…
Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
Chuanhao Yan, Fengdi Che, Xuhan Huang +12
Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification proce…