Activation Steering in Neural Theorem Provers

要約

大規模な言語モデル（LLMS）は、Leanのようなプルーフアシスタントを使用して正式な定理を証明することで有望を示しています。
ただし、現在の最先端の言語モデルは、実務家がさまざまなサンプリング手法を使用してLLMS機能を改善することを導く証明の次のステップを予測するのに苦労しています。
LLMは正しい戦術を予測できることを観察します。
ただし、候補戦術のセット内で適切にランキングする際の課題に直面しており、全体的な選択プロセスに影響します。
このハードルを克服するために、アクティベーションステアリングを使用してLLMS応答をガイドして、推論時の世代を改善します。
我々の結果は、アクティベーションステアリングが、特にリソースに制約のある環境で価値がある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, Google