論文の概要: Baldur: Whole-Proof Generation and Repair with Large Language Models

• arxiv url: http://arxiv.org/abs/2303.04910v1
• Date: Wed, 8 Mar 2023 22:00:15 GMT
• ステータス: 処理完了
• システム内更新日: 2023-03-10 16:48:02.880015
• Title: Baldur: Whole-Proof Generation and Repair with Large Language Models
• Title（参考訳）: Baldur: 大きな言語モデルによる全体生成と修復
• Authors: Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
• Abstract要約: 我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。 我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。 本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
• 参考スコア（独自算出の注目度）: 8.100054850290507
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time, and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language text and code and fine-tuned on proofs, to generate whole proofs for theorems at once, rather than one step at a time. We combine this proof generation model with a fine-tuned repair model to repair generated proofs, further increasing proving power. As its main contributions, this paper demonstrates for the first time that: (1) Whole-proof generation using transformers is possible and is as effective as search-based techniques without requiring costly search. (2) Giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair and further improves automated proof generation. (3) We establish a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs. In addition to empirically showing the effectiveness of whole-proof generation, repair, and added context, we show that Baldur improves on the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.
• Abstract（参考訳）: ソフトウェア特性を正式に検証することは、非常に望ましいが労働集約的なタスクである。 最近の研究は、coqやisabelle/holのような証明アシスタントを使った形式的検証を自動化する手法を開発しており、例えば、モデルに一度に1つの証明ステップを予測させ、そのモデルを使って可能な証明の空間を探索する。 本稿では形式的検証を自動化する新しい手法について紹介する。我々は、自然言語テキストとコードに基づいて訓練され、証明に基づいて微調整された大規模言語モデルを用いて、一度に1ステップではなく、一度に定理の証明全体を生成する。 この証明生成モデルと微調整された修復モデルを組み合わせて、生成した証明を修復し、さらに証明能力を高める。 本稿は,(1)トランスフォーマによる完全耐性生成は可能であり,コストのかかる検索を必要とせず,検索に基づく手法と同じくらい効果的であることを示す。 2) 学習したモデルに事前の失敗証明試行やその後のエラーメッセージなどの追加のコンテキストを与えることで, 検証の修復が達成され, さらに自動証明生成が向上する。 (3) 完全自動証明合成のための新しい技術を確立した。 我々はプロトタイプであるBaldurで手法を改良し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。 また,全耐久生成,補修,追加コンテキストの有効性を実証的に示すとともに,定理の8.7%の証明を自動的に生成することにより,最先端ツールであるThorの改善が示されている。 ボールドゥルとトールは共に65.7%の定理を完全自動で証明できる。 本稿では,形式的検証を自動化するため,大規模言語モデルを用いた新たな研究の道を開く。

関連論文リスト

• Cobblestone: Iterative Automation for Formal Verification [11.445689801392657]
  Coqのような証明アシスタントを用いた形式的検証は、ソフトウェア品質を改善する効果的な方法であるが、高価である。 最近の研究では、機械学習を使って証明を自動的に合成し、検証の労力を削減しているが、これらのツールは、望まれるソフトウェアプロパティのほんの一部しか証明できない。 我々は, 証明合成における部分的な進歩を生かして, 技術状況を改善する新しい証明合成手法であるCobblestoneを紹介した。
  論文  参考訳（メタデータ） (2024-10-25T19:25:00Z)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs [30.57062828812679]
  本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。 大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
  論文  参考訳（メタデータ） (2022-10-21T22:37:22Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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