論文の概要: A Learning Method for Symbolic Systems Using Large Language Models
- arxiv url: http://arxiv.org/abs/2605.08694v1
- Date: Sat, 09 May 2026 05:05:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-19 20:59:26.993678
- Title: A Learning Method for Symbolic Systems Using Large Language Models
- Title（参考訳）: 大規模言語モデルを用いた記号システムの学習法
- Abstract要約: 我々は、データから純粋に象徴的な戦術をマイニングするために、LLM2Ltacをインテリジェントシンセサイザーとして提案する。
我々は,Rocq 8.20.0 上で LLM2Ltac を実装し,標準ライブラリの 11,725 個の定理をマイニングする。
その結果、採掘された戦術は23.87%の定理を証明できるようにCoqHammerを改善し、改良されたCoqHammerとClaude Codeを統合すると、全体の定理は9.90%増加した。
- 参考スコア（独自算出の注目度）: 2.3263761713486066
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Automated theorem proving is essential for the formal verification of safety-critical systems. As the corpus of formal proofs grows, a natural paradigm is to learn from existing proofs. However, current learning-based approaches predominantly train Large Language Models (LLMs) as end-to-end provers, which yields resource-intensive, opaque systems. Conversely, while traditional symbolic provers are computationally efficient, how to automatically improve these solvers from data remains an open challenge. This paper bridges this gap by proposing LLM2Ltac, the first approach that leverages the reasoning power of LLMs not as end-to-end provers, but as intelligent synthesizers to mine purely symbolic tactics from data. Given a corpus of formal proofs, LLM2Ltac asks an LLM to identify latent proof strategies and formalize them into reusable tactics. These tactics are verified for validity and generalizability, and finally integrated into symbolic provers to enhance their automated proving capabilities without the runtime cost of LLMs. We implement LLM2Ltac on Rocq 8.20.0 and mine tactics from 11,725 theorems in the standard library. We evaluate our approach on 6,199 theorems from four large real-world verification projects, namely, compcert, Coq-Art, Ext-Lib, and VFA. Results show that the mined tactics improve CoqHammer to prove 23.87% more theorems, and when integrating the improved CoqHammer with Claude Code, the overall proved theorems increases by 9.90%, indicating the effectiveness of LLM2Ltac.
- Abstract（参考訳）: 自動定理証明は安全クリティカルシステムの形式的検証に不可欠である。
形式的証明のコーパスが大きくなるにつれて、自然パラダイムは既存の証明から学ぶことである。
しかし、現在の学習ベースのアプローチは、主に大規模言語モデル(LLM)をエンドツーエンドのプローバーとして訓練し、リソース集約型不透明なシステムを生み出している。
逆に、従来の記号型プローバーは計算効率が良いが、データからこれらの解法を自動的に改善する方法はオープンな課題である。
本稿では,LLM2Ltacをエンド・ツー・エンドのプローバーとしてではなく,データから純粋に象徴的な戦術をマイニングするためのインテリジェントシンセサイザーとして活用する最初のアプローチである。
正式な証明のコーパスが与えられた後、LLM2Ltac は LLM に潜伏した証明戦略を特定し、それらを再利用可能な戦術に定式化するよう依頼する。
これらの戦術は妥当性と一般化性を検証するとともに,LLMのランタイムコストを伴わずに,その自動証明能力を向上するシンボリック・プロバーに統合される。
我々は,Rocq 8.20.0 上で LLM2Ltac を実装し,標準ライブラリの 11,725 個の定理をマイニングする。
我々は,4つの大規模実世界検証プロジェクト,すなわちcompcert,Coq-Art,Ext-Lib,VFAの6,199の定理に対するアプローチを評価する。
その結果、採掘された戦術は23.87%以上の定理を証明するためにコクハマーを改善し、改良されたコクハマーとクロード・コードを統合すると、全体の定理は9.90%増加し、LLM2Ltacの有効性を示した。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - On Reasoning-Centric LLM-based Automated Theorem Proving [1.8002666661892468]
本稿では,Rocq の推論中心の証明エージェント ReCent-Prover を紹介する。
ReCent-Proverは、過去の最先端技術よりも証明された定理の数において相対的に22.58%向上していることを示す。
論文 参考訳（メタデータ） (2026-04-21T15:11:42Z) - MM-HELIX: Boosting Multimodal Long-Chain Reflective Reasoning with Holistic Platform and Adaptive Hybrid Policy Optimization [103.74675519953898]
ロングチェーンのリフレクティブ推論は、複雑な現実世界の問題を解決するための前提条件である。
我々は42の難解な合成タスクの1,260のサンプルからなるベンチマークを構築した。
トレーニング後のデータを生成し、そのようなデータを活用するための学習パラダイムを探索する。
論文 参考訳（メタデータ） (2025-10-09T17:53:58Z) - 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) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - LLM2: Let Large Language Models Harness System 2 Reasoning [65.89293674479907]
大規模言語モデル(LLM)は、無数のタスクにまたがって印象的な機能を示してきたが、時には望ましくない出力が得られる。
本稿では LLM とプロセスベースの検証器を組み合わせた新しいフレームワーク LLM2 を紹介する。
LLMs2は妥当な候補を生成するのに責任を持ち、検証者は望ましい出力と望ましくない出力を区別するためにタイムリーなプロセスベースのフィードバックを提供する。
論文 参考訳（メタデータ） (2024-12-29T06:32:36Z) - Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。
本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。
その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文 参考訳（メタデータ） (2024-09-22T00:19:27Z) - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。
人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。
定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
論文 参考訳（メタデータ） (2024-04-18T22:54:08Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。