Generative reward models for formal theorem proving: Methods, benchmarks, and tree search integration

Automated theorem proving aims to generate machine-verifiable proofs with minimal human intervention, but effective proof search remains challenging. Tree search algorithms require guidance to navigate exponentially large proof spaces. However, existing approaches suffer from fundamental limitations. Log-probability heuristics conflate generation likelihood with step quality, binary feedback from proof assistants provides no notion of progress, and discriminative reward models compress complex reasoning into opaque scalar values. In addition, implementation fragmentation limits reproducibility, and the absence of evaluation frameworks blocks systematic development of reward models for formal mathematics. This thesis makes three contributions addressing these challenges. First, we develop TreeThink, a modular Python library providing unified implementations of best-first search, beam search, and Monte Carlo tree search for formal theorem proving. The architecture cleanly separates search strategy, environment interaction, and model inference, enabling reproducible experimentation and fair comparison across algorithms. All components support asynchronous execution and batched inference for computational efficiency. Second, we introduce a framework for generative reward models that produce natural language critiques evaluating proof steps. Unlike discriminative models that output scalar scores without explanation, our approach generates structured textual feedback describing correctness, progress toward goals, and strategic value, with embedded numerical scores for integration into tree search. A key design element is conditioning reward generation on environmental feedback from proof assistant execution, grounding evaluations in concrete compiler responses rather than predictions alone. We study both zero-shot deployment using pretrained models and reinforcement learning on proof trajectories to align critique scores with proof outcomes. Third, we introduce FormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving. The benchmark consists of preference pairs where correct Lean 4 proofs are paired with incorrect variants generated through five error injection strategies targeting realistic failure modes, including forced mistakes, minimal variations, complex incorrect proofs, natural language justification, and Python code injection. Quality control ensures errors are semantic rather than trivial, and evaluation protocols support both pointwise and pairwise reward models with position bias mitigation. Together, these contributions advance neural theorem proving by providing modular infrastructure for systematic experimentation, richer guidance signals through interpretable natural language feedback grounded in execution, and evaluation frameworks that enable principled development of reward models for formal mathematics. Our work addresses key limitations in automated theorem proving and establishes foundations for more capable and interpretable proof search systems.