4 papers
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…