論文の概要: Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
- arxiv url: http://arxiv.org/abs/2605.04472v1
- Date: Wed, 06 May 2026 03:49:35 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-07 18:41:07.636429
- Title: Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
- Title（参考訳）: Wilf-Zeilberger Guidance と LLM による組合せアイデンティティの自動証明
- Abstract要約: WZ-LLMはニューロシンボリックなフレームワークで、WZの証明計画をLean 4.0で実行可能な証明スケッチに変換する。
We show that WZ-LLM achieve a 34% proof success rate on LCI-Test (100 classic identities), developed on strong baselines as DeepSeek-V3 Goedel-V2。
- 参考スコア（独自算出の注目度）: 26.76149523669167
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Automating formal proofs of combinatorial identities is challenging for LLM-based provers, as long-horizon proof planning is required and unconstrained search quickly explodes. Symbolic methods such as the Wilf-Zeilberger (WZ) method can achieve a mechanized proof of combinatorial identities by constructing special auxiliary functions and demonstrating that they satisfy specific recurrence relations. We propose WZ-LLM, a neuro-symbolic framework that turns WZ proof plans into executable proof sketches in Lean 4 and uses an LLM-based prover to discharge the resulting machine-checkable subgoals. We also train a dedicated WZ-Prover via a Lean-kernel-verified bootstrapping loop with expert-verified iteration, followed by DAPO-based refinement. Experiments show that WZ-LLM achieves a 34% proof success rate on LCI-Test (100 classic combinatorial identities), outperforming strong baselines such as DeepSeek-V3 and Goedel-Prover-V2, and delivering consistent gains on CombiBench and PutnamBench-Comb. These results indicate that our framework provides two complementary strengths: improved direct proving for identities beyond the scope of WZ, and substantially higher end-to-end success when WZ sketches guide a specialized prover.
- Abstract（参考訳）: 長期の証明計画が必要であり、制約のない探索が急速に爆発するので、LLMベースの証明者にとって、組合せアイデンティティの正式な証明の自動化は困難である。
Wilf-Zeilberger (WZ) 法のようなシンボリックな手法は、特別な補助関数を構築し、それらが特定の反復関係を満たすことを示すことによって、組合せアイデンティティの機械的証明を達成することができる。
WZ-LLMは,WZの証明計画をLean 4の実行可能な証明スケッチに変換するニューロシンボリックなフレームワークであり,LLMベースの証明器を用いてマシンチェック可能なサブゴールを出力する。
専門的なイテレーションでリーンカーネルを検証したブートストラップループを通じて、専用のWZ-Proverをトレーニングします。
実験の結果、WZ-LLMはLCI-Test(100の古典的な組合せアイデンティティ)で34%の成功率を獲得し、DeepSeek-V3やGoedel-Prover-V2といった強力なベースラインを上回り、CombiBenchとPatnamBench-Combで一貫した利得を提供する。
これらの結果から,本フレームワークは,WZの範囲を越えたアイデンティティの直接証明の改善と,WZスケッチが特殊証明を導く場合のエンド・ツー・エンドの成功という2つの相補的強みを示唆している。
関連論文リスト
- Process-Verified Reinforcement Learning for Theorem Proving via Lean [47.294932573003756]
リーン証明アシスタント自体が、象徴的なプロセスのオラクルとして機能できることを示します。
LeanLeanとDeepSeek-V1.5の実験によると、戦術レベルの監視は、ほとんどの設定で結果のみのベースラインを上回っている。
論文 参考訳（メタデータ） (2026-06-18T10:40:55Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - ProRAG: Process-Supervised Reinforcement Learning for Retrieval-Augmented Generation [54.071574153853994]
ProRAGは、学習段階の監視をオンライン最適化ループに統合するために設計されたプロセス教師付き強化学習フレームワークである。
本フレームワークは,(1)構造化推論形式でモデルを初期化するための監視されたポリシーワームアップ,(2)中間推論品質を定量化するためのMCTSベースのプロセスリワードモデル(PRM)の構築,(3)細粒度プロセスの好みに合わせてポリシーを調整するためのPRM誘導推論リファインメント,(4)プロセススーパービジョン強化学習と2つのグラニュラリティー・アドバンテージ・メカニズムの4段階から構成される。
論文 参考訳（メタデータ） (2026-01-29T16:04:59Z) - MatchTIR: Fine-Grained Supervision for Tool-Integrated Reasoning via Bipartite Matching [60.886768806064936]
Tool-Integrated Reasoningは、外部ツールのインタラクションと推論ステップをインターリーブすることで、大規模な言語モデルで複雑なタスクに対処することを可能にする。
既存の強化学習法は、結果や軌道レベルの報酬に依存し、軌道内のすべてのステップに一様の利点を割り当てる。
両部間マッチングに基づくターンレベルの報酬割当と二重レベルの優位性推定によるきめ細かい監視を実現するフレームワークであるMatchTIRを提案する。
論文 参考訳（メタデータ） (2026-01-15T18:59:23Z) - A Fano-Style Accuracy Upper Bound for LLM Single-Pass Reasoning in Multi-Hop QA [65.38186593873313]
MHQA(Multi-Hop Question Answering)は、ノイズ下でのシーケンシャルな推論を通じて、分散した相互依存的な証拠を統合する必要がある。
我々はMHQAのための概念実証マルチコールフレームワークをInfoQAで紹介する。
我々は、理論とフレームワークを検証するために、厳密で騒音に富んだベンチマークを構築した。
論文 参考訳（メタデータ） (2025-09-25T14:11:57Z) - RouteMark: A Fingerprint for Intellectual Property Attribution in Routing-based Model Merging [69.2230254959204]
我々は,統合されたMoEモデルにおけるIP保護のためのフレームワークであるRouteMarkを提案する。
我々の重要な洞察は、タスク固有の専門家は、探索入力の下で安定かつ独特なルーティング行動を示すことである。
属性と改ざん検出のために,類似性に基づくマッチングアルゴリズムを導入する。
論文 参考訳（メタデータ） (2025-08-03T14:51:58Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement [7.702809989052384]
HybridProverは、戦術ベースの生成と全防御合成を組み合わせたデュアルモデル証明フレームワークである。
最適化されたデータセット上にIsabelle定理証明器とファインチューンLPMにHybridProverを実装した。
論文 参考訳（メタデータ） (2025-05-21T16:45:43Z) - 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) - A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation [3.003569769097376]
コンビニティクスは数学の基盤であり、離散構造の分析と問題解決に不可欠なツールを提供する。
これを解決するために、手動でLeanCombを構築しました。
我々は,自己改善型大規模言語モデルによって提案される候補戦略と,予測のための強化学習木探索アプローチを組み合わせた,コンビニアル・アイデンティティのための自動定理ジェネレータATG4CIを開発した。
論文 参考訳（メタデータ） (2025-02-25T04:41:49Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。