論文の概要: 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つの復号戦略(サンプリングと最優先探索)の下で性能を向上させることの実証である。

関連論文リスト

• Translating Informal Proofs into Formal Proofs Using a Chain of States [20.0011959667642]
  本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。 まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。 次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
  論文  参考訳（メタデータ） (2025-12-11T06:08:34Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  大規模言語モデル(LLM)は、幅広いタスクにまたがる強力な一般化を実証している。 最近の研究は、暗黙の推論に拍車をかけた、明示的な思考の連鎖から注意を向けている。 本調査では,表現形式から計算戦略へ焦点を移し,実行パラダイムを中心とした分類を紹介した。
  論文  参考訳（メタデータ） (2025-09-02T14:16:02Z)
• Revisiting LLM Reasoning via Information Bottleneck [57.519119962528166]
  大規模言語モデル(LLM)は、最近、検証可能な報酬付き強化学習(RLVR)を通じて推論能力の顕著な進歩を示した。 本稿では,情報ボトルネック(IB)の原理に基づくLLM推論の理論的特徴について述べる。 IB対応推論最適化(IBRO)を提案する。
  論文  参考訳（メタデータ） (2025-07-24T13:14:25Z)
• Sound and Complete Neurosymbolic Reasoning with LLM-Grounded Interpretations [7.81820080453498]
  大規模言語モデル(LLM)は、自然言語の理解と生成において印象的な能力を示している。 パラ一貫性論理に対する形式的意味論の解釈関数に LLM を直接統合する手法を提案する。
  論文  参考訳（メタデータ） (2025-07-13T19:05:43Z)
• Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations [13.485604499678262]
  自然言語推論(NLI)における自然言語説明の役割 近年の研究では、大言語モデル(LLM)と定理証明器(TP)の相互作用が、NLI説明の有効性の検証と改善に役立つことが示されている。 本稿では,自己形式化時の意味喪失を軽減するための戦略について検討する。
  論文  参考訳（メタデータ） (2025-05-30T06:38:39Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-05-20T15:13:32Z)
• Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification [0.26763498831034044]
  組込み戦術の力と既製の自動定理プローバーを利用するシステム内で使用される形式言語で全ての証明を生成するフレームワークを導入する。 LLMのトレーニングには2段階の微調整プロセスを使用し、まずSFTベースのトレーニングを使用して、モデルが構文的に正しいIsabelleコードを生成する。 我々は,MiniF2F-testベンチマークとIsabelle証明アシスタントを用いてフレームワークを検証し,S3バケットアクセスポリシーコードの正当性を検証するためのユースケースを設計する。
  論文  参考訳（メタデータ） (2025-04-23T18:04:38Z)
• LLM Post-Training: A Deep Dive into Reasoning Large Language Models [131.10969986056]
  大規模言語モデル (LLMs) は自然言語処理の状況を変え、多様な応用をもたらした。 ポストトレーニング手法により、LLMは知識を洗練させ、推論を改善し、事実の正確性を高め、ユーザの意図や倫理的配慮をより効果的に整合させることができる。
  論文  参考訳（メタデータ） (2025-02-28T18:59:54Z)
• InductionBench: LLMs Fail in the Simplest Complexity Class [53.70978746199222]
  大規模言語モデル(LLM)は推論において顕著に改善されている。 帰納的推論(inductive reasoning)は、観測されたデータから基礎となるルールを推測するものであり、まだ探索されていない。 本稿では, LLMの帰納的推論能力を評価するための新しいベンチマークであるインジェクションベンチを紹介する。
  論文  参考訳（メタデータ） (2025-02-20T03:48:00Z)
• 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)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• 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)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• 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)

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

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