arXiv:2502.15507v3 通告类型: replace-cross 摘要：大型语言模型（LLMs）在使用证明助手如Lean验证形式定理方面显示出前景。然而，当前最先进的语言模型在预测证明中的下一步时遇到挣扎，导致研究人员使用不同的采样技术以提高LLMs的能力。我们观察到，LLM有能力预测正确的策略，但它在适当排序候选策略方面面临挑战，影响整体选择过程。为了克服这一障碍，我们使用激活转向来指导LLM的响应，以提高推理时的生成质量。我们的结果显示，激活转向提供了一种有前景的轻量级替代方案，用于增强LLMs的定理证明能力，特别是在资源受限的环境中特别有价值。