論文の概要: Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs
- arxiv url: http://arxiv.org/abs/2210.12283v1
- Date: Fri, 21 Oct 2022 22:37:22 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-25 14:22:38.781665
- Title: Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs
- Title(参考訳): ドラフト, スケッチ, 証明: 形式的証明による形式的定理証明の指導
- Authors: Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu,
Mateja Jamnik, Timoth\'ee Lacroix, Yuhuai Wu, Guillaume Lample
- Abstract要約: 本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。
大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
- 参考スコア(独自算出の注目度): 30.57062828812679
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The formalization of existing mathematical proofs is a notoriously difficult
process. Despite decades of research on automation and proof assistants,
writing formal proofs remains arduous and only accessible to a few experts.
While previous studies to automate formalization focused on powerful search
algorithms, no attempts were made to take advantage of available informal
proofs. In this work, we introduce Draft, Sketch, and Prove (DSP), a method
that maps informal proofs to formal proof sketches, and uses the sketches to
guide an automated prover by directing its search to easier sub-problems. We
investigate two relevant setups where informal proofs are either written by
humans or generated by a language model. Our experiments and ablation studies
show that large language models are able to produce well-structured formal
sketches that follow the same reasoning steps as the informal proofs. Guiding
an automated prover with these sketches enhances its performance from 20.9% to
39.3% on a collection of mathematical competition problems.
- Abstract(参考訳): 既存の数学的証明の形式化は、非常に難しいプロセスである。
自動化と証明アシスタントに関する何十年もの研究にもかかわらず、正式な証明を書くことは困難であり、少数の専門家にしかアクセスできない。
これまでは、強力な検索アルゴリズムに焦点をあてて形式化を自動化する研究が行われてきたが、非公式な証明を活用する試みは行われなかった。
本研究では,非公式な証明を形式的な証明スケッチにマッピングするDraft, Sketch, Prove (DSP)を導入し,そのスケッチを用いて自動証明を誘導し,サブプロブレムの検索を容易にする手法を提案する。
非公式な証明が人間によって書かれるか、言語モデルによって生成されるかの2つの関連する設定について検討する。
我々の実験とアブレーションの研究は、大きな言語モデルが形式的証明と同じ推論ステップに従って、十分に構造化された形式的スケッチを作成できることを示しています。
これらのスケッチによる自動証明器の誘導は、数学的な競合問題の集合において、その性能を20.9%から39.3%に向上させる。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳(メタデータ) (2023-03-08T22:00:15Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳(メタデータ) (2023-02-24T03:28:46Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳(メタデータ) (2023-01-05T17:56:00Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳(メタデータ) (2022-11-14T16:52:32Z) - 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) - Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。
また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文 参考訳(メタデータ) (2022-02-03T00:17:00Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳(メタデータ) (2021-06-02T17:58:35Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。