Structured Hints for Sample-Efficient Lean Theorem Proving
作者: Zachary Burton
分类: cs.AI
发布日期: 2026-01-22
备注: 9 pages, 1 figure
💡 一句话要点
利用结构化提示提升精简定理证明的样本效率
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 神经定理证明 强化学习 结构化提示 样本效率 miniF2F基准
📋 核心要点
- 现有神经定理证明器训练复杂，但可能未能充分利用策略语言的结构化信息。
- 论文提出一种轻量级的干预方法，即在推理时使用固定提示调度，引导模型生成。
- 实验表明，该方法在miniF2F基准上显著提升了定理证明的性能，相对提升达43%。
📝 摘要（中文）
最先进的神经定理证明器，如DeepSeek-Prover-V1.5，结合了大型语言模型和强化学习，通过复杂的训练实现了令人印象深刻的结果。本文探讨了一个问题：这些经过高度训练的模型在推理时是否仍然能从简单的结构化指导中受益？我们在miniF2F基准上评估了一种轻量级的干预方法——一个在15个常见策略骨架上的固定提示调度。与同一模型的标准采样相比，这种简单的方法产生了21.7%的pass@16，而标准采样为15.2%，在使用相同数量的样本（k=16）和相同最大生成长度（1024个token）的情况下，相对提高了43%。我们的结果表明，即使是功能强大的、经过强化学习训练的证明器，也未能充分利用策略语言中可用的结构先验知识，并且简单的推理时指导仍然是一种廉价的、互补的提升方法。
🔬 方法详解
问题定义：现有的神经定理证明器，例如DeepSeek-Prover-V1.5，虽然通过大型语言模型和强化学习取得了显著成果，但可能存在对策略语言内在结构先验知识利用不足的问题。这些模型在推理时，可能无法有效地探索策略空间，导致样本效率低下。因此，如何更有效地利用策略语言的结构信息，提升定理证明的样本效率，是本文要解决的核心问题。
核心思路：本文的核心思路是在推理阶段，通过引入结构化提示来引导神经定理证明器的生成过程。具体来说，作者设计了一组固定的提示调度，这些提示基于15个常见的策略骨架。通过在推理时按照预定的顺序给出这些提示，可以帮助模型更好地探索策略空间，并生成更有效的证明策略。这种方法的关键在于利用了策略语言的结构化信息，从而提升了模型的样本效率。
技术框架：该方法的技术框架非常简洁。它主要包括两个部分：一是预定义的15个常见策略骨架，这些骨架代表了定理证明中常用的策略模式；二是固定的提示调度，它规定了在推理过程中，按照什么顺序给出这些策略骨架对应的提示。在推理时，模型首先接收到第一个提示，然后生成相应的策略。如果生成的策略未能成功证明定理，则模型接收到下一个提示，并重复上述过程。整个过程持续到达到预定的最大生成长度或成功证明定理为止。
关键创新：该方法最重要的技术创新点在于它在推理时引入了结构化提示。与传统的神经定理证明器直接从模型中采样生成策略不同，该方法通过提示来引导模型的生成过程，从而更好地利用了策略语言的结构化信息。这种方法可以看作是一种轻量级的干预，它不需要对模型进行额外的训练，就可以显著提升定理证明的性能。
关键设计：该方法的一个关键设计是策略骨架的选择。作者选择了15个常见的策略骨架，这些骨架覆盖了定理证明中常用的策略模式。另一个关键设计是提示调度的顺序。作者采用了一种固定的提示调度，这意味着在推理过程中，提示的顺序是预先确定的。这种固定的调度方式可以简化推理过程，并降低计算成本。此外，最大生成长度设置为1024个token，样本数量k设置为16，这些参数的选择也影响着最终的性能。
🖼️ 关键图片
📊 实验亮点
实验结果表明，在miniF2F基准上，使用结构化提示的神经定理证明器pass@16指标达到了21.7%，而标准采样方法仅为15.2%。这意味着在相同的样本数量（k=16）和最大生成长度（1024个token）下，该方法实现了43%的相对性能提升。这一结果表明，即使是经过强化学习训练的强大模型，也能从简单的推理时指导中受益。
🎯 应用场景
该研究成果可应用于自动化定理证明、形式化验证等领域，有助于提高软件和硬件系统的可靠性。通过提升定理证明的效率，可以加速数学研究和计算机科学的发展，并为构建更安全、更可靠的智能系统奠定基础。未来，该方法有望扩展到更复杂的定理证明场景，并与其他技术相结合，实现更强大的自动化推理能力。
📄 摘要（原文）
State-of-the-art neural theorem provers like DeepSeek-Prover-V1.5 combine large language models with reinforcement learning, achieving impressive results through sophisticated training. We ask: do these highly-trained models still benefit from simple structural guidance at inference time? We evaluate a lightweight intervention -- a fixed prompt schedule over 15 common tactic skeletons -- on the miniF2F benchmark. This simple approach yields 21.7% pass@16 compared to 15.2% for standard sampling from the same model, a 43% relative improvement using the same number of samples (k=16) and same maximum generation length (1024 tokens). Our results suggest that even capable RL-trained provers underutilize structural priors available in the tactic language, and that simple inference-time guidance remains a cheap, complementary boost.