样本高效精益定理证明的结构化提示

DeepSeek-Prover-V1.5 等最先进的神经定理证明器将大语言模型与强化学习相结合，通过复杂的训练取得了令人印象深刻的结果。我们问：这些训练有素的模型在推理时是否仍然受益于简单的结构指导？我们在 miniF2F 基准上评估了轻量级干预——超过 15 种常见策略框架的固定提示时间表。与来自同一模型的标准采样的 15.2% 相比，这种简单的方法产生了 21.7% pass@16，使用相同数量的样本 (k=16) 和相同的最大生成长度 (1024 个token) 相对提高了 43%。我们的结果表明，即使是有能力的强化学习训练的证明者也没有充分利用策略语言中可用的结构先验，而简单的推理时间指导仍然是一种廉价的补充性推动。