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

TL;DR

This work addresses the discrepancy between training on only correct proof paths and the inference-time need to explore many tactics. It introduces PropL, a Lean-formalized benchmark of intuitionistic propositional logic theorems with complete trial-and-error proofs generated by focused proof search, and compares two training/inference paradigms: TrialMaster, which learns from failed search paths, and a conventional DFS baseline. Empirical results show TrialMaster achieves higher success on unseen theorems with lower search costs, and ablative analyses confirm the value of trial-and-error data for backtracking-enabled proof search. The dataset and methods offer a pathway to more robust, failure-aware theorem proving and set the stage for extending these insights to broader mathematical domains.

Abstract

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.

Figures (7)

• Figure 1: A simple example for how learning trial-and-error data impacts inference distribution. See Figure \ref{['fig:intro-propl-example']} for a concrete case.
• Figure 2: Method comparison. (a) A conventional system: The tactic generator (i.e., LLM) is fine-tuned on correct proof paths only. During inference, the trained tactic generator produces $N_{\text{sampled}}$ (e.g., 2 in the example) tactics at a time. If Lean decides that the current tactic is wrong, the system backtracks to the last valid state and tries other candidate tactics. (b) Our methodology: The tactic generator is fine-tuned on proofs with trial-and-error. During inference, we take the first tactic it generates and feed that into Lean for state checking at each step.
• Figure 3: An illustration of the bijection between a proposition and a natural number, where gray nodes are leaf nodes. ID is computed using \ref{['alg:encoding']} with $n = 6$ and $p = 2$ in this case.
• Figure 4: Two proofs for one propositional logic theorem with tactics and states in Lean.
• Figure 5: Experiment results on OOD task. (a) We fix $N_{\text{sampled}} = 10$ to see the impact of temperature on the DFS system. (b) We fix $t=1.2$ to see the impact of the number of sampled tactics. The number of Lean calls is noted beside the marker. (c) Comparison of $N_{\text{Lean}}$ among our method and top 3 DFS systems with the highest success rate. In summary, training with trial-and-error achieves a higher success rate with a relatively lower search cost compared to the DFS systems.