Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

TL;DR

This paper demonstrates that hierarchical agentic theorem provers can achieve exponential sample complexity advantages over flat provers by reusing proof structures, as shown through a statistical learning framework.

Contribution

It introduces a formal analysis of proof search as an MDP and shows how hierarchical proof strategies can exponentially reduce sample complexity compared to flat strategies.

Findings

Hierarchical provers can exponentially outperform flat provers in sample efficiency.

Reusing proof structures reduces the number of required training samples exponentially.

Success bounds depend on proof length, predictability, and learning accuracy.

Abstract

Agentic theorem provers often introduce intermediate lemmas, proof sketches, or subgoal decompositions before returning to tactic-level search. This can look like an expensive detour: if proving lemmas is itself hard, why should a learned prover spend effort there? We give a statistical learning answer. Instead of worst-case proof complexity over all formulas, we study the biased data distribution produced by a teacher prover: initial theorem states together with successful verified proof traces. We model proof search as a deterministic finite-horizon MDP and analyze offline imitation learning from those traces. The success bounds depend on the average length of teacher proofs, how predictable the teacher's next action is, and how accurately the student learns that local prediction problem. A flat student learns from fully inlined traces, so repeated subproofs appear many times in its training and test-time certificate. A hierarchical student instead predicts a reusable proof DAG and solves each shared block once. When flattening duplicates the same hard local argument exponentially many times, the sufficient-sample certificate produced by our bounds can be exponentially smaller for the hierarchical learner. This gives a concrete statistical mechanism by which reusable proof structure helps verifier-based theorem proving.