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.

通过从失败的搜索路径中学习，我们展示了训练模型的益处。我们与仅使用正确路径训练的模型进行比较，并发现前者以更少的搜索次数解决了更多未见过的定理。

借鉴失败：使用试错数据对直觉命题逻辑证明进行微调的 LLM

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

The interactive theorem prover, Lean, enables the verification of formal
mathematical proofs and is backed by an expanding community. Central to this
ecosystem is its mathematical library, mathlib4, which lays the groundwork for
the formalization of an expanding range of mathematical theories. However,
searching for theorems in mathlib4 can be challenging. To successfully search
in mathlib4, users often need to be familiar with its naming conventions or
documentation strings. Therefore, creating a semantic search engine that can be
used easily by individuals with varying familiarity with mathlib4 is very
important. In this paper, we present a semantic search engine for mathlib4 that
accepts informal queries and finds the relevant theorems. We also establish a
benchmark for assessing the performance of various search engines for mathlib4.

为 mathlib4 设计了一个语义搜索引擎，可以接收非正式查询并找到相应的定理，同时还建立了一个用于评估各个搜索引擎性能的基准。

Mathlib4 的语义搜索引擎

A Semantic Search Engine for Mathlib4

Large language models (LLMs) often struggle with complex logical reasoning
due to logical inconsistencies and the inherent difficulty of such reasoning.
We use Lean, a theorem proving framework, to address these challenges. By
formalizing logical reasoning problems into theorems within Lean, we can solve
them by proving or disproving the corresponding theorems. This method reduces
the risk of logical inconsistencies with the help of Lean's symbolic solver. It
also enhances our ability to treat complex reasoning tasks by using Lean's
extensive library of theorem proofs. Our method achieves state-of-the-art
performance on the FOLIO dataset and achieves performance near this level on
ProofWriter. Notably, these results were accomplished by fine-tuning on fewer
than 100 in-domain samples for each dataset.

利用 Lean 框架，将复杂的逻辑推理问题形式化为定理后进行求解，以减少逻辑不一致性的风险并提升处理复杂推理任务的能力，取得了在 FOLIO 数据集上的最先进表现，并在 ProofWriter 上接近该水平的成果。值得注意的是，这些结果是在每个数据集的不到 100 个领域内样本进行微调实现的。