Fugu-MT 論文翻訳(概要): Proof Recommendation System for the HOL4 Theorem Prover

論文の概要: 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-19 08:09:23.475768
Title: Proof Recommendation System for the HOL4 Theorem Prover
Title（参考訳）: HOL4理論プロバーの証明推薦システム
Authors: Nour Dekhil, Adnan Rashid, Sofiene Tahar,
Abstract要約: 本稿では,HOL4定理証明器の証明推薦システムを提案する。本ツールは,HOL4の証明支援に特化して設計されたトランスフォーマーベースモデル上に構築されている。
参考スコア（独自算出の注目度）: 0.0
License:
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つの戦術を含む)で既に使われている特定の戦術列を読み、現在の証明状態と呼ばれ、次の最適な証明ステップの推奨を提供する。

関連論文リスト

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)
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
探索経路の失敗から学習する訓練モデルの利点を実証する。既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
論文参考訳（メタデータ） (2024-04-10T23:01:45Z)
Faithful Explanations of Black-box NLP Models Using LLM-generated Counterfactuals [67.64770842323966]
NLPシステムの予測に関する因果的説明は、安全性を確保し、信頼を確立するために不可欠である。既存の手法は、しばしばモデル予測を効果的または効率的に説明できない。本稿では, 対物近似(CF)の2つの手法を提案する。
論文参考訳（メタデータ） (2023-10-01T07:31:04Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)
Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文参考訳（メタデータ） (2023-03-08T22:00:15Z)
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)

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