論文の概要: Steering LLMs for Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2502.15507v5
• Date: Mon, 13 Oct 2025 01:51:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-14 15:48:08.226346
• Title: Steering LLMs for Formal Theorem Proving
• Title（参考訳）: フォーマルな理論証明のための操舵LDM
• Authors: Shashank Kirtania, Arun Iyer,
• Abstract要約: 我々は,非公式な推論トレースに関連する残効活性化における線形方向を同定する推論時間介入を開発する。 このメカニズムはまた、大規模言語モデルのアクティベーション空間において、推論がどのように内部的にエンコードされているかについての解釈可能な情報を与える。 1) LLM の証明合成を導くための新しいアクティベーションベースの介入,(2) この介入が2つの復号化戦略の下で性能を向上させることの実証である。
• 参考スコア（独自算出の注目度）: 1.083373217040891
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.
• Abstract（参考訳）: 自動定理証明の最近の進歩は、非公式な数学的ステートメントを形式的な証明に変換するためにLarge Language Models (LLMs)を用いている。 しかし、非公式な方法はしばしば曖昧であり、厳密な論理構造が欠如しているため、モデルを正確に解釈することは困難である。 既存の手法は高い性能を達成するが、LLMが内部的に非公式な手がかりをどのように表現するか、またこれらの証明生成にどのように影響するかは分かっていない。 そこで本稿では,不規則な推論トレースに関連付けられた残効活性化における線形方向を識別し,微調整を伴わずに検証構造を改善するための推論時間介入である「textit{activation steering」について検討する。 この機構はまた、LSMの活性化空間において、推論がどのように内部的に符号化されているかの解釈可能な情報を与える。 我々は、既に形式化された定理から形式的証明を生成する方法をテストする。 筆者らの貢献は,(1) LLMにおける証明合成を導くための新規なアクティベーションに基づく介入,(2) この介入が更なる訓練を伴わずに2つの復号戦略(サンプリングと最優先探索)の下で性能を向上させることの実証である。

関連論文リスト

• LLM Post-Training: A Deep Dive into Reasoning Large Language Models [131.10969986056]
  大規模言語モデル (LLMs) は自然言語処理の状況を変え、多様な応用をもたらした。 ポストトレーニング手法により、LLMは知識を洗練させ、推論を改善し、事実の正確性を高め、ユーザの意図や倫理的配慮をより効果的に整合させることができる。
  論文  参考訳（メタデータ） (2025-02-28T18:59:54Z)
• LLM-Powered Preference Elicitation in Combinatorial Assignment [17.367432304040662]
  提案手法は,大規模言語モデル(LLM)を人為的プロキシとして活用し,課題における選好選択(PE)を簡素化するものである。 本稿では,SOTA ML を用いた嗜好推論方式と併用して動作する LLM プロキシのフレームワークを提案する。 コース割当て領域における人間の問合せに対するLLMプロキシの有効性を実験的に評価した。
  論文  参考訳（メタデータ） (2025-02-14T17:12:20Z)
• CogSteer: Cognition-Inspired Selective Layer Intervention for Efficiently Steering Large Language Models [37.476241509187304]
  大規模言語モデル(LLM)は、広範囲なデータに対する事前学習を通じて、優れたパフォーマンスを達成する。 基本的なメカニズムにおける解釈可能性の欠如は、特定のアプリケーションに対してLLMを効果的に操る能力を制限する。 本研究では,眼球運動計測を用いた認知的視点からLLMのメカニズムを考察する。
  論文  参考訳（メタデータ） (2024-10-23T09:40:15Z)
• Zero-shot Model-based Reinforcement Learning using Large Language Models [12.930241182192988]
  本稿では,マルコフ決定過程の動的状態を予測するために,事前学習した大規模言語モデルをどのように活用することができるかを検討する。 本稿では,モデルに基づく政策評価とデータ強化型オフ政治強化学習という2つの強化学習環境における概念実証の応用について述べる。
  論文  参考訳（メタデータ） (2024-10-15T15:46:53Z)
• In-Context Learning with Reinforcement Learning for Incomplete Utterance Rewriting [33.89176174108559]
  大規模言語モデル(LLM)の文脈内学習は、いくつかの例で拡張された命令に基づいて予測を行う。 ICLの既存の例選択方法はスパースまたは高密度レトリバーを使用し、有効性能を導出する。 本稿では,言語モデルセレクタとLLMジェネレータから構成される実例選択(RLS)のためのポリシーベース強化学習フレームワークを提案する。
  論文  参考訳（メタデータ） (2024-08-23T12:32:12Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  大規模言語モデル(LLM)は多くの自然言語タスクにおいて印象的な能力を示している。 LLMは多段階推論を行う際にエラー、幻覚、矛盾する文を生成する傾向がある。 本稿では,LLMの復号化過程を検討計画で導くためのフレームワークであるQ*を紹介する。
  論文  参考訳（メタデータ） (2024-06-20T13:08:09Z)
• From Words to Actions: Unveiling the Theoretical Underpinnings of LLM-Driven Autonomous Systems [59.40480894948944]
  大規模言語モデル (LLM) は、物理世界の意思決定問題を解くことができる。 このモデルの下で、LLM Plannerは、プロンプトを介して言語ベースのサブゴールを反復的に生成することにより、部分的に観測可能なマルコフ決定プロセス(POMDP)をナビゲートする。 我々は,事前学習したLLMプランナーが,文脈内学習を通じてベイズ的集計模倣学習(BAIL)を効果的に行うことを証明した。
  論文  参考訳（メタデータ） (2024-05-30T09:42:54Z)
• One Token Can Help! Learning Scalable and Pluggable Virtual Tokens for Retrieval-Augmented Large Language Models [67.49462724595445]
  Retrieval-augmented Generation (RAG)は、大規模言語モデル(LLM)を改善するための有望な方法である。 本稿では,RAGのためのスケーラブルでプラガブルな仮想トークンを学習する新しい手法を提案する。
  論文  参考訳（メタデータ） (2024-05-30T03:44:54Z)
• Improve Temporal Awareness of LLMs for Sequential Recommendation [61.723928508200196]
  大規模言語モデル(LLM)は、幅広い汎用タスクを解く際、印象的なゼロショット能力を示した。 LLMは時間的情報の認識と利用に不足しており、シーケンシャルなデータの理解を必要とするタスクではパフォーマンスが悪い。 LLMに基づくシーケンシャルレコメンデーションのために、歴史的相互作用の中で時間情報を利用する3つのプロンプト戦略を提案する。
  論文  参考訳（メタデータ） (2024-05-05T00:21:26Z)
• PANDA: Preference Adaptation for Enhancing Domain-Specific Abilities of LLMs [49.32067576992511]
  大規模言語モデルは、しばしばドメイン固有の最先端モデルによって達成されるパフォーマンスに欠ける。 LLMのドメイン固有の機能を強化する1つの潜在的アプローチは、対応するデータセットを使用してそれらを微調整することである。 LLM(PANDA)のドメイン固有能力を高めるための優先度適応法を提案する。 実験の結果,PANDA はテキスト分類や対話型意思決定タスクにおいて LLM のドメイン固有性を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-02-20T09:02:55Z)
• Are Large Language Models Good Prompt Optimizers? [65.48910201816223]
  我々は,LLMに基づくPrompt Optimizationの実際のメカニズムを明らかにするために研究を行っている。 以上の結果から, LLMは, 反射中の誤差の真の原因を特定するのに苦慮し, 自己の事前知識に偏っていることが明らかとなった。 我々は、より制御可能な方法でターゲットモデルの振舞いを直接最適化する新しい「自動振舞い最適化」パラダイムを導入する。
  論文  参考訳（メタデータ） (2024-02-03T09:48:54Z)
• LLMRec: Benchmarking Large Language Models on Recommendation Task [54.48899723591296]
  推奨領域におけるLarge Language Models (LLMs) の適用について, 十分に検討されていない。 我々は、評価予測、シーケンシャルレコメンデーション、直接レコメンデーション、説明生成、レビュー要約を含む5つのレコメンデーションタスクにおいて、市販のLLMをベンチマークする。 ベンチマークの結果,LLMは逐次的・直接的推薦といった精度に基づくタスクにおいて適度な熟練度しか示さないことがわかった。
  論文  参考訳（メタデータ） (2023-08-23T16:32:54Z)
• PRISMA-DFLLM: An Extension of PRISMA for Systematic Literature Reviews using Domain-specific Finetuned Large Language Models [0.0]
  本稿では,Large Language Models(LLMs)のパワーと,PRISMA(Preferred Reporting Items for Systematic Reviews and Meta-Analyses)の厳密な報告ガイドラインを組み合わせたAI対応方法論フレームワークを提案する。 厳密なSLRプロセスの結果として選択されたドメイン固有の学術論文にLCMを微調整することにより、提案するPRISMA-DFLLMレポートガイドラインは、より効率、再利用性、拡張性を達成する可能性を秘めている。
  論文  参考訳（メタデータ） (2023-06-15T02:52:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。