A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL

TL;DR

<3-5 sentence high-level summary> This work addresses the mismatch between informal mathematical reasoning and formal proof languages by introducing Minilang, a minimalist, declarative proof language designed to mirror informal proofs and minimize prover-specific idioms. A rule-based Isar-to-Minilang translator enables large-scale NTP training by distilling Isabelle proofs into compact, high-level proof outlines that LLMs can learn more effectively, and an enhanced Sledgehammer (Sledgehammer*) augments automated proof discharge. Through supervised fine-tuning on translated corpora from Isabelle AFP and HOL libraries, the authors demonstrate substantial gains over prior Isabelle-based declarative approaches, achieving state-of-the-art pass@k metrics on the PISA benchmark. The combination of language redesign, improved ATP integration, and a scalable translation pipeline provides a strong foundation for declarative neural theorem proving across proof assistants.

Abstract

Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using natural languages, the transition to mechanized formal theorem proving presents persistent challenges. Mechanized proof languages often contain many syntactic constructs and diverse, specialized proof tactics, which facilitate expert use but have no direct counterpart in informal mathematical proofs. These prover-specific idioms represent an additional burden for LLM-based NTPs that might be otherwise successful in generating informal proofs. Seeking to bridge this gap between formal proof construction and informal reasoning, in order to better facilitate NTP, this work approaches these challenges from a language design perspective. We look at common reasoning patterns in informal proofs and in existing mechanized proofs, and design Minilang -- a minimalist proof language that captures these reasoning patterns. In contrast to proof languages (informal and formal) that often feature a large collection of operations with unclear semantic boundaries, Minilang is deliberately kept minimalist -- its core design comprises only 10 operations, each with clear semantic distinctions. We further develop a rule-based translator from Isabelle's language (Isar) to Minilang, translating ~340K existing proofs with an ~85% success rate. Using this translated corpus, we finetune two LLMs to compare machine learning performance on Minilang versus the original Isar. Experiments show Minilang benefits the two LLMs by improving the pass@1 success rate on the PISA benchmark by up to 20/29 percentage points in comparison to the Isar-based LLMs w/wo Sledgehammer. The pass@1 rate reaches 69.1%, exceeding the prior work Baldur's pass@64 (65.7%); the pass@8 rate reaches 79.2%, exceeding the SOTA on PISA (71.0%) achieved by Magnushammer.

Figures (14)

• Figure 1: Minilang and mainstream proof languages on the same proof goal. While Lean and Isar incorporate natural-language-like structures, (e.g., build-in keywords such ashave and hence), their proofs are interspersed with tactics and other expert-oriented constructs that complicate learning. In contrast, Minilang aims to highlight the key proof outlines with close alignment to informal proofs.
• Figure 2: Minilang's state machine.
• Figure 3: An example written in Minilang.
• Figure 4: The transition of the tree state in the example of \ref{['fig:sqrt2-example']}. Each node represents the state after the execution of the labeled line.
• Figure 5: The semantics of Minilang commands. Notation $\bar{x} / \bar{H}$ denote a sequence of variables/hypothesis

Theorems & Definitions (3)

• Theorem 1: Soundness
• Theorem 2: Relative Completeness
• proof