activity
20232026
most citedFormal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

1 citations · 2 across the 5 of their papers we have counts for

collaborators

5 papers

cs.LG2026

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…

cs.LG2025

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…

cs.LG2024★ 1 cited

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…

cs.LG2023★ 1 cited

Beyond NTK with Vanilla Gradient Descent: A Mean-Field Analysis of Neural Networks with Polynomial Width, Samples, and Time

Arvind Mahankali, Jeff Z. Haochen, Kefan Dong +2

Despite recent theoretical progress on the non-convex optimization of two-layer neural networks, it is still an open question whether gradient descent on neural networks without un…

cs.LG2023

Toward -recovery of Nonlinear Functions: A Polynomial Sample Complexity Bound for Gaussian Random Fields

Kefan Dong, Tengyu Ma

Many machine learning applications require learning a function with a small worst-case error over the entire input domain, that is, the -error, whereas most existing theo…