LLM-guided formal verification
LLM-guided hierarchical decomposition solves 50-59% of TLA+ proof obligations TLA+ - The Temporal Logic of ActionsTL;DW
- TLA+ proofs differ fundamentally from tactic-based provers like Lean—they decompose obligations into intermediate claims rather than apply sequential tactics, requiring a new LLM strategy.
- Direct LLM-based proof generation (DLPG) fails due to syntax errors: LLMs struggle with TLA+'s low-resource language, mixing in syntax from other systems like Isabelle.
- Hierarchical decomposition approach: use symbolic tool SAPG for simple obligations, ask LLM to decompose complex ones recursively until all leaves are provable by SAPG.
- Normalize LLM output to structured JSON with assume/goal fields containing only boolean expressions, not full TLA+ proofs, reducing syntax errors dramatically.
- LMGPA (LLM-guided proof automation) achieves 59% proof success on mathematical theorems with DeepSeek vs. 29% for direct generation with same model.
- Validate decompositions by checking that subclaims together actually imply the parent obligation, preventing logically invalid decompositions from LLMs.
- Syntactic validity improved from <1% (Gemini 2.5 Flash in DLPG) to 60%+ across models using normalized decomposition strategy.
- Evaluated on 119 TLA+ theorems: 93 from mathematical benchmarks (F2F, ProofNet translated) and 26 from distributed protocol induction proofs representing practical use cases.
- LMGPA consistently outperforms all baselines including obvious, SAPG alone, and DLPG across six state-of-the-art LLMs without fine-tuning.
TL;DW
- TLA+ proofs differ fundamentally from tactic-based provers like Lean—they decompose obligations into intermediate claims rather than apply sequential tactics, requiring a new LLM strategy.
- Direct LLM-based proof generation (DLPG) fails due to syntax errors: LLMs struggle with TLA+'s low-resource language, mixing in syntax from other systems like Isabelle.
- Hierarchical decomposition approach: use symbolic tool SAPG for simple obligations, ask LLM to decompose complex ones recursively until all leaves are provable by SAPG.
- Normalize LLM output to structured JSON with assume/goal fields containing only boolean expressions, not full TLA+ proofs, reducing syntax errors dramatically.
- LMGPA (LLM-guided proof automation) achieves 59% proof success on mathematical theorems with DeepSeek vs. 29% for direct generation with same model.
- Validate decompositions by checking that subclaims together actually imply the parent obligation, preventing logically invalid decompositions from LLMs.
- Syntactic validity improved from <1% (Gemini 2.5 Flash in DLPG) to 60%+ across models using normalized decomposition strategy.
- Evaluated on 119 TLA+ theorems: 93 from mathematical benchmarks (F2F, ProofNet translated) and 26 from distributed protocol induction proofs representing practical use cases.
- LMGPA consistently outperforms all baselines including obvious, SAPG alone, and DLPG across six state-of-the-art LLMs without fine-tuning.
LMGPA pairs an LLM with symbolic prover SAPG: simple obligations go straight to SAPG, complex ones get recursively decomposed by the LLM into normalized JSON subclaims rather than raw TLA+ syntax. The constraint lifts proof validity from ~20% to >60%, tested across 119 theorems from math and distributed protocols using six frontier models.