arXiv:2502.15507v2 通知类型: replace-cross 摘要：大型语言模型（LLMs）在使用Lean等证明助手证明形式定理方面展现了潜力。然而，当前最先进的语言模型在预测证明中的下一步时存在困难，促使实践者采用不同的采样技术以提高LLMs的能力。我们观察到，LLM能够预测正确的策略；然而，它在适当排序候选策略方面面临挑战，这影响了整体选择过程。为了克服这一困难，我们在推理时刻使用激活控制来指导LLM的响应，以改进生成结果。我们的结果表明，激活控制为增强LLMs的定理证明能力提供了一种轻量级的有前景的替代方案，特别是在资源受限的环境中尤其有价值。