一句话：提出极简证明语言 Minilang，并翻译 Isar 语料微调 LLM，以提升 Isabelle/HOL 神经定理证明性能。
神经定理证明（NTP）用 LLM 自动构造 Isabelle/HOL 等形式证明，但形式证明语言包含大量专用语法与策略，与非形式数学证明差异显著，给 LLM 带来额外负担。本文从语言设计出发，归纳非形式证明与机器证明中的常见推理模式，提出极简证明语言 Minilang（Isabelle/Minilang），核心仅 10 个语义清晰的证明操作，并实现从 Isar 到 Minilang 的规则翻译器，以约 85% 成功率翻译约 34 万条 Isabelle 证明。基于该语料微调两个 LLM 后，实验表明 Minilang 相比原始 Isar 有/无 Sledgehammer 将 PISA 上 pass@1 最多提升 20/29 个百分点，达 69.1%，超过 Baldur 的 pass@64（65.7%）；pass@8 达 79.2%，超过 Magnushammer 的 71.0%。
Neural Theorem Proving (NTP) employs Large Language Models (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 (formally named Isabelle/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 proof operations, each with clear semantic distinctions. We further develop a rule-based translator from Isabelle’s proof language (Isar) to Minilang, translating ∼340,000 existing Isabelle 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 language. 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 state-of-the-art on PISA (71.0%) achieved by Magnushammer.
@article{paperbot3833,
title = {A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL},
author = {Qiyuan Xu and Renxi Wang and Peixin Wang and Haonan Li and Conrad Watt},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798275}
}