Learn from Failure: Fine-tuning LLM s with Trial-and-Error Data for Intuitionistic Propositional Logic Proving (2024)

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.

## introduction automated theorem proving is a challenging task that has recently gained popularity in the machinelearning community. researchers build neural theorem provers to synthesize formal proofs of mathematical theorems @xcite @xcite @xcite @xcite @xcite @xcite . typically, a neural theorem prover, given a partial proof and the current proof state, * the first two authors contributed equally to this work. ## propl: a new dataset for intuitionistic propositional logic theorems in lean our aim is to experimentally validate that trialand-error information can enhance models' ability to do backtracking and tactic generation for theorem-proving tasks. given that existing opensource theorem proving datasets lack information on trial-and-error processes, we have developed propl, which is based on theorems of intuitionistic propositional logic. this dataset uniquely includes proofs that encapsulate the complete search process, incorporating the trial-and-error data generated by the fps algorithm. our dataset has two other benefits. it is formalized in lean, so that the validity of the theorems and proofs are guaranteed. the tactics generated by the model trained on propl can also be directly sent to lean to be checked. propl is also representative of all the intuitionistic propositional logic theorems, since by uniformly sampling integers, we can use a bijection between natural numbers and propositions to uniformly sample propositions. this bijection is explained in the theorem generation section. ## conclusion and future work in this paper, we study automated theorem proving in formalized environments. we create a complete, scalable, and representative dataset of intuitionistic propositional logic theorems in lean. we demonstrate that leveraging information from failed search states and backtracking not only teaches models how to backtrack effectively, but also helps in developing better tactics than those generated by models trained without access to backtracking insights. we release our datasets on github and huggingface. foot_0 a natural extension of our research involves investigating whether trial-and-error information is beneficial for more general mathematical theoremproving settings. exploring this avenue could provide valuable insights into the effectiveness of our approach across broader mathematical domains.