摘要

本文介绍了一种名为Lean-STaR的新型框架，旨在通过在每个证明步骤之前生成非正式的思维链（“思维”）来提升语言模型在定理证明中的能力。传统上，基于语言模型的定理证明假设通过在大量形式证明数据上进行训练，模型将学会证明定理。然而，我们的关键观察是，形式证明中未包含的丰富非正式信息对于学习证明定理可能是有用的。Lean-STaR利用回顾性的真实策略生成合成思维，用于训练语言模型。在推理时，训练后的模型直接在预测每个证明步骤的策略之前生成思维。此外，Lean-STaR在自我教学推理者框架的基础上，应用专家迭代算法对模型进行进一步微调，使其在Lean定理证明环境中在miniF2F-test基准上取得了最先进的结果。

原理

Lean-STaR框架的核心在于将非正式的思维链与形式证明步骤交错结合。首先，模型通过提示一个足够强大的语言模型（如GPT-4），并基于人类编写的证明数据集（如Mathlib）生成回顾性思维。随后，对一个增强思维的策略预测器进行微调，该预测器在给定Lean状态时，能够生成思维并预测后续策略。最后，通过专家迭代算法优化这个增强思维的策略预测器，使用多步骤成功率作为奖励。这种方法不仅提高了定理证明的准确性，还通过分析增强思维对定理证明过程各个方面的影响，提供了对其有效性的深入见解。

流程

Lean-STaR的工作流程分为两个主要阶段：首先，通过GPT-4生成大约50,000个增强思维的示例，然后通过两轮专家迭代合成额外的50,000个示例。在第一阶段，模型生成思维并预测策略；在第二阶段，通过专家迭代进一步优化模型，使其在正确的证明样本上进行微调。整个过程通过迭代生成和验证证明轨迹，不断优化模型的定理证明能力。

应用

Lean-STaR框架的应用前景广泛，不仅限于数学定理的自动证明，还可以扩展到教育、科学发现和程序验证等多个领域。通过提高语言模型在定理证明中的能力，Lean-STaR有望在促进数学教育、加速科学研究和提高软件可靠性方面发挥重要作用。