# Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving

arXiv: https://arxiv.org/abs/2404.07382 · HTML: https://mlsanity.com/paper/2404.07382/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 49 references that are in the map.
- First posted on arXiv 10 Apr 2024.

## Builds on (most cited first, 25 of 25)

- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [HuggingFace's Transformers: State-of-the-art Natural Language Processing](https://mlsanity.com/paper/1910.03771/) (2019)
- [Least-to-Most Prompting Enables Complex Reasoning in Large Language Models](https://mlsanity.com/paper/2205.10625/) (2022)
- [Graph of Thoughts: Solving Elaborate Problems with Large Language Models](https://mlsanity.com/paper/2308.09687/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Complexity-Based Prompting for Multi-Step Reasoning](https://mlsanity.com/paper/2210.00720/) (2022)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Navigate through Enigmatic Labyrinth A Survey of Chain of Thought Reasoning: Advances, Frontiers and Future](https://mlsanity.com/paper/2309.15402/) (2023)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Constructions in combinatorics via neural networks](https://mlsanity.com/paper/2104.14516/) (2021)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [A Survey on Theorem Provers in Formal Methods](https://mlsanity.com/paper/1912.03028/) (2019)
- [Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning](https://mlsanity.com/paper/1811.00796/) (2018)
- [Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic](https://mlsanity.com/paper/1706.06462/) (2017)
- [Automated proof synthesis for propositional logic with deep neural networks](https://mlsanity.com/paper/1805.11799/) (2018)

## Built on by (most cited first, 11 of 11)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [On Almost Surely Safe Alignment of Large Language Models at Inference-Time](https://mlsanity.com/paper/2502.01208/) (2025)
- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Can Transformers Do Enumerative Geometry?](https://mlsanity.com/paper/2408.14915/) (2024)
- [Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation](https://mlsanity.com/paper/2411.00863/) (2024)
- [LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation](https://mlsanity.com/paper/2505.12031/) (2025)
- [WarriorMath: Enhancing the Mathematical Ability of Large Language Models with a Defect-aware Framework](https://mlsanity.com/paper/2508.01245/) (2025)
- [Boule or Baguette? A Study on Task Topology, Length Generalization, and the Benefit of Reasoning Traces](https://mlsanity.com/paper/2602.14404/) (2026)
- [LeanPolish: Verified Supervision for Lean Proof Compression](https://mlsanity.com/paper/2609.38384/) (2026)

## Abstract (arXiv)

Recent advances in Automated Theorem Proving have shown the effectiveness of leveraging a (large) language model that generates tactics (i.e. proof steps) to search through proof states. The current model, while trained solely on successful proof paths, faces a discrepancy at the inference stage, as it must sample and try various tactics at each proof state until finding success, unlike its training which does not incorporate learning from failed attempts. Intuitively, a tactic that leads to a failed search path would indicate that similar tactics should receive less attention during the following trials. In this paper, we demonstrate the benefit of training models that additionally learn from failed search paths. Facing the lack of such trial-and-error data in existing open-source theorem-proving datasets, we curate a dataset on intuitionistic propositional logic theorems and formalize it in Lean, such that we can reliably check the correctness of proofs. We compare our model trained on relatively short trial-and-error information (TrialMaster) with models trained only on the correct paths and discover that the former solves more unseen theorems with lower trial searches.