Fugu-MT 論文翻訳(概要): QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

論文の概要: QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning

arxiv url: http://arxiv.org/abs/2408.09237v6
Date: Wed, 11 Dec 2024 19:53:23 GMT
ステータス: 翻訳完了
システム内更新日: 2024-12-13 13:30:12.315729
Title: QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
Title（参考訳）: QEDCartographer: Reward-free Reinforcement Learning を用いた形式検証の自動化
Authors: Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, Yuriy Brun,
Abstract要約: QEDCartographerは、教師付きと強化学習を組み合わせた自動証明合成ツールである。オープンソースCoqプロジェクトの68.5K定理のCoqGymベンチマークを用いて,QEDCartographerを評価した。本研究は,強化学習が証明合成ツールの探索機構を改善するための実りある研究方向であることを実証する。
参考スコア（独自算出の注目度）: 8.116854714039452
License:
Abstract: Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 34% shorter proofs 29% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 30.3% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms.
Abstract（参考訳）: 形式的検証は信頼性の高いソフトウェアを作成するための有望な方法であるが,手作業による検証証明の難しさにより,実用性は著しく制限されている。近年の手法では、定理証明器を用いて証明空間を探索し、いくつかの証明合成を自動化している。残念なことに、定理証明器は最も粗末な進捗推定のみを提供し、事実上無向探索をもたらす。この問題に対処するために、教師付きと強化学習を組み合わせた自動証明合成ツールであるQEDCartographerを作成し、より効果的に証明空間を探索する。 QEDCartographerは証明の分岐構造を取り入れ、報酬のない探索を可能にし、形式検証に固有のスパース報酬問題を克服する。オープンソースCoqプロジェクトの68.5K定理のCoqGymベンチマークを用いて,QEDCartographerを評価した。 QEDCartographerはテストセット定理の21.4%を自動的に証明している。従来の検索ベースの証明合成ツールであるTok、Tac、ASTactic、Passport、Proverbot9001は、教師あり学習のみに依存しており、それぞれ9.6%、9.8%、10.9%、12.5%、19.8%を証明している。 62のツールを組み合わせたDidiaは19.2%を証明している。最も効果的な先行ツールであるProverbot9001と比較して、QEDCartographerは29%高速で34%の短い証明を生成する。 QEDCartographerと非学習ベースのCoqHammerは30.3%、CoqHammerは26.6%である。本研究は,強化学習が証明合成ツールの探索機構を改善するための実りある研究方向であることを実証する。

関連論文リスト

Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
論文参考訳（メタデータ） (2024-10-25T19:25:00Z)
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。この合成データセットでDeepSeekMath 7Bモデルを微調整します。我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文参考訳（メタデータ） (2024-05-23T09:03:42Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。本研究では,LLM ベースの証明器 ReProver を開発した。
論文参考訳（メタデータ） (2023-06-27T17:05:32Z)
Progressive-Hint Prompting Improves Reasoning in Large Language Models [63.98629132836499]
本稿では,プログレッシブ・ヒント・プロンプト(PHP)と呼ばれる新しいプロンプト手法を提案する。事前に生成された回答をヒントとして使用することで、ユーザとLLM(Large Language Models)間の自動多元的対話を可能にする。我々は7つのベンチマークで広範囲かつ包括的な実験を行った。その結果、PHPは高い効率を保ちながら精度を大幅に向上することが示された。
論文参考訳（メタデータ） (2023-04-19T16:29:48Z)
Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文参考訳（メタデータ） (2023-03-08T22:00:15Z)
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文参考訳（メタデータ） (2022-10-21T22:37:22Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
HyperTree Proof Search for Neural Theorem Proving [14.677400513932852]
本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。 HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
論文参考訳（メタデータ） (2022-05-23T17:49:55Z)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)
Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
我々のシステムは適切な戦術を予測し、戦術スクリプトの形で証明を見つける。システムの性能は、Coq Standard Libraryで評価される。 CoqHammerシステムと組み合わせると、この2つのシステムは図書館の補題の56.7%を証明している。
論文参考訳（メタデータ） (2020-03-20T08:22:30Z)

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

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