LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4

TL;DR

LeanTree introduces a white-box proof search method in Lean 4 that factorizes proof states into simpler components, enabling more efficient and parallelized theorem proving with potential advantages over black-box approaches.

Contribution

The paper presents LeanTree, a novel tool and dataset that enhance white-box proof search by factorizing proof states, addressing limitations of existing black-box methods.

Findings

White-box approach can outperform black-box in certain scenarios.

Factorization of proof states simplifies evaluation and reduces context.

Enables parallel search and efficient reuse of proof states.

Abstract

Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Large language models (LLMs) have recently emerged as a promising heuristic for ATP, but they lack correctness guarantees and thus require interaction with a proof verifier. Such interactions typically follow one of two approaches: black-box interaction, which does not utilize intermediate proof states, or white-box approaches, which allow for incremental proof construction and examination of intermediate states. While black-box approaches have directly benefited from recent LLM advances, white-box methods have comparatively lagged behind. In this paper, we address this gap by introducing LeanTree, which consists of (i) a tool built in the Lean 4 language that factorizes complex proof states into simpler, independent branches, and (ii) a dataset of these factorized intermediate states. Our white-box tooling offers several advantages over black-box approaches: it simplifies evaluation, reduces necessary context, generates richer training data, enables parallel search across multiple states, supports efficient reuse of states, and provides feedback in case of errors. Our preliminary results hint that white-box approaches outperform black-box alternatives in some settings.