論文の概要: Proof Recommendation System for the HOL4 Theorem Prover

• arxiv url: http://arxiv.org/abs/2501.05463v1
• Date: Tue, 31 Dec 2024 17:13:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-20 04:34:19.68713
• Title: Proof Recommendation System for the HOL4 Theorem Prover
• Title（参考訳）: HOL4理論プロバーの証明推薦システム
• Authors: Nour Dekhil, Adnan Rashid, Sofiene Tahar,
• Abstract要約: 本稿では,HOL4定理証明器の証明推薦システムを提案する。 本ツールは,HOL4の証明支援に特化して設計されたトランスフォーマーベースモデル上に構築されている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s).
• Abstract（参考訳）: 本稿では,HOL4定理証明器の証明推薦システムを提案する。 本ツールは,HOL4の証明支援に特化して設計されたトランスフォーマーモデル[2]上に構築されている。 このモデルは定理の証明を含むHOL4の広範なライブラリから定理を証明するパターンを識別するように訓練されている。 これにより、以前に使用した戦術の歴史に基づいて、次の戦術(防御段階)を正確に予測することができる。 このツールは、証明プロセス(この場合、少なくとも3つの戦術を含む)で既に使われている特定の戦術列を読み、現在の証明状態と呼ばれ、次の最適な証明ステップの推奨を提供する。

関連論文リスト

• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
  NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。 既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。 本稿では, 対物近似(CF)の2つの手法を提案する。
  論文  参考訳（メタデータ） (2023-10-01T07:31:04Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
  我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。 システムの性能は、Coq Standard Libraryで評価される。 CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
  論文  参考訳（メタデータ） (2020-03-20T08:22:30Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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