1 citations · 1 across the 5 of their papers we have counts for
6 papers
Trust the Critic More
Kaiyue Wen, Luke Bailey, Arvind Mahankali +1
Standard language model RL algorithms credit every token of a long rollout with the same advantage determined by the terminal reward. Actor-critic methods can provide finer-grained…
Pseudo-Formalization for Automatic Proof Verification
Slim Barkallah, Luke Bailey, Kaiyue Wen +2
Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to…
Scaling Self-Play with Self-Guidance
Luke Bailey, Kaiyue Wen, Kefan Dong +2
LLM self-play algorithms are notable in that, in principle, nothing bounds their learning: a Conjecturer model creates problems for a Solver, and both improve together. However, in…
Divide-and-Conquer CoT: RL for Reducing Latency via Parallel Reasoning
Arvind Mahankali, Kaiyue Wen, Tengyu Ma
Long chain-of-thought reasoning (Long CoT) is now fundamental to state-of-the-art LLMs, especially in mathematical reasoning. However, LLM generation is highly sequential, and long…
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Kefan Dong, Tengyu Ma
A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this is…
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
Kefan Dong, Arvind Mahankali, Tengyu Ma
Mathematical theorem proving is an important testbed for large language models' deep and abstract reasoning capability. This paper focuses on improving LLMs' ability to write proof…