Activation Steering in Neural Theorem Provers

要約

大規模言語モデル（LLM）は、Leanのような証明アシスタントを用いた形式定理の証明に有望である。しかし、現在の言語モデルは証明の次のステップを予測するのに苦労しており、実務家はLLMの能力を向上させるために様々なサンプリング技術を使用している。我々は、LLMが正しい戦術を予測する能力があることを観察している。しかし、LLMは、候補戦術の集合の中でそれを適切にランク付けするという課題に直面しており、全体的な選択プロセスに影響を及ぼしている。このハードルを克服するために、我々は活性化ステアリングを用いてLLMの応答を誘導し、推論時の世代を改善する。我々の結果は、活性化ステアリングが、LLMの定理証明能力を向上させるために、特化した微調整に代わる有望な軽量な代替手段を提供することを示唆しており、特にリソースに制約のある環境において価値がある。

要約(オリジナル)

Large Language Models (LLMs) have shown promise in proving formal theorems using proof assistants like Lean. However, current state of the art language models struggles to predict next step in proofs leading practitioners to use different sampling techniques to improve LLMs capabilities. We observe that the LLM is capable of predicting the correct tactic; however, it faces challenges in ranking it appropriately within the set of candidate tactics, affecting the overall selection process. To overcome this hurdle, we use activation steering to guide LLMs responses to improve the generations at the time of inference. Our results suggest that activation steering offers a promising lightweight alternative to specialized fine-tuning for enhancing theorem proving capabilities in LLMs, particularly valuable in resource-constrained environments.

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL