通过激活向量干预，让大模型更准地把数学表述转为形式化证明。
Steering LLMs for Formal Theorem Proving
- 在推理时调整模型内部激活方向，引导逻辑推理路径。
- 两种解码策略下，证明成功率显著提升，无需重新训练。
- 方法可解释性强，揭示了模型如何编码数学推理过程。
近期自动化定理证明研究利用大语言模型（LLMs）将非正式数学陈述转化为形式化证明。然而，非正式线索常含糊且缺乏严格逻辑结构，导致模型难以精准理解。现有方法虽表现良好，但对模型如何内部表征非正式线索及其影响尚不清楚。为此，我们探索了激活转向（activation steering）——一种推理时的干预技术，识别与非正式推理轨迹相关的残差激活线性方向，并调整这些方向以改进证明生成，无需微调。该机制还提供了关于推理在模型激活空间中如何编码的可解释信息。我们在已形式化的定理上测试该方法生成形式化证明的能力。贡献有二：（1）提出一种基于激活的干预方法，用于引导LLM的证明合成；（2）证明该方法在两种解码策略（采样与最佳优先搜索）下均提升性能，且无需额外训练。
原文摘要 · Abstract (English)
Recent advances in automated theorem proving use Large Language Models (LLMs) to translate informal mathematical statements into formal proofs. However, informal cues are often ambiguous or lack strict logical structure, making it hard for models to interpret them precisely. While existing methods achieve strong performance, little is known about how LLMs internally represent informal cues, or how these influence proof generation. To address this, we explore \textit{activation steering}, an inference-time intervention that identifies linear directions in residual activations associated with informal reasoning traces and adjusts them to improve proof construction without fine-tuning. This mechanism also yields interpretable information about how reasoning is internally encoded in the activation space of LLMs. We test our method for generating formal proofs from already-formalized theorems. Our contributions are twofold: (1) a novel activation-based intervention for guiding proof synthesis in LLMs; and (2) demonstration that this intervention improves performance under two decoding strategies (sampling and best-first search) without any further training.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。