Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4

TL;DR

The paper tackles machine-assisted theorem proving in Lean 4 by addressing the expansive and noisy tactic space that hinders learning. It introduces atomic tactics to create a finite, complete action set, and a transposing atomization framework to convert arbitrary proofs into atomized, trainable sequences, paired with a compact ExprGraph representation. Nazrin Prover, a graph neural network-based agent trained on atomized data, uses a neural probabilistic automaton with rainbow guidance to generate and contextualize tactics, enabling high-throughput proof searches on consumer hardware. Evaluations on Lean's standard library and Mathlib demonstrate Nazrin's complementary strengths to existing automation tools, along with clarifying limitations and avenues for improvement in cross-section handling and architectural tuning.

Abstract

In Machine-Assisted Theorem Proving, a theorem proving agent searches for a sequence of expressions and tactics that can prove a conjecture in a proof assistant. In this work, we introduce several novel concepts and capabilities to address obstacles faced by machine-assisted theorem proving. We first present a set of \textbf{atomic tactics}, a small finite set of tactics capable of proving any provable statement in Lean. We then introduce a \textbf{transposing atomization} algorithm which turns arbitrary proof expressions into a series of atomic tactics. We next introduce the \textbf{ExprGraph} data structure, which provides a succinct representation for Lean expressions. Finally, we present the \textbf{Nazrin Prover}, a graph neural network-based theorem proving agent using atomic tactics and ExprGraph. Nazrin circumvents many challenges faced by existing proving agents by exclusively dispatching atomic tactics, and it is robust enough to both train and evaluate on consumer-grade hardware. We demonstrate the potential of tools like Nazrin using theorems from Lean's standard library and from Mathlib.

Figures (10)

• Figure 1: The Three Views of a Proof and their relations. We discuss Transposition in Section \ref{['sec:transpose']} and Essentialization and Contextualization in Section \ref{['sec:Graph']}. We do not dicsuss Articulation.
• Figure 2: Built-in atomic tactics
• Figure 3: Synthetic atomic tactics for handling edge cases
• Figure 4: Blue arrows represent tactic applications. State-level transposition changes the dispatch order of tactics, but does not change the ordering of tactics on a particular goal.
• Figure 5: Goal-level transposition switches orders of tactics on the same goal. Although $\textcolor{purple}{?x}$ is not assigned, we can dispatch a rewrite tactic if we rearrange the order of semigrade tactics.