論文の概要: Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge
- arxiv url: http://arxiv.org/abs/2012.10987v2
- Date: Sat, 26 Dec 2020 16:38:05 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-20 02:27:20.345037
- Title: Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge
- Title(参考訳): prove-it: 一般的な数学的知識の整理と検証のための証明アシスタント
- Authors: Wayne M. Witzel, Warren D. Craft, Robert D. Carr and Joaqu\'in E.
Madrid Larra\~naga
- Abstract要約: Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce Prove-It, a Python-based general-purpose interactive
theorem-proving assistant designed with the goal of making formal theorem
proving as easy and natural as informal theorem proving (with moderate
training). Prove-It uses a highly-flexible Jupyter notebook-based user
interface that documents interactions and proof steps using LaTeX. We review
Prove-It's highly expressive representation of expressions, judgments,
theorems, and proofs; demonstrate the system by constructing a traditional
proof-by-contradiction that $\sqrt{2}\notin\mathbb{Q}$; and discuss how the
system avoids inconsistencies such as Russell's and Curry's paradoxes.
Extensive documentation is provided in the appendices about core elements of
the system. Current development and future work includes promising applications
to quantum circuit manipulation and quantum algorithm verification.
- Abstract(参考訳): 形式的定理証明を(適度な訓練で)非公式な定理証明と同じくらい簡単かつ自然なものにすることを目的として設計された,pythonベースの汎用対話型定理証明アシスタントであるpromise-itを紹介する。
Prove-Itは、高フレキシブルなJupyterノートブックベースのユーザインターフェースを使用して、LaTeXを使用してインタラクションと証明ステップを文書化する。
本稿では,表現,判断,定理,証明の表現を高度に表現し,$\sqrt{2}\notin\mathbb{q}$という従来の証明バイコントラディションを構築し,ラッセルやカリーのパラドックスのような矛盾を避ける方法について論じる。
システムの中核要素に関する付録には、広範なドキュメントが記載されている。
現在の開発と今後の研究は、量子回路操作と量子アルゴリズム検証への有望な応用を含んでいる。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文 参考訳(メタデータ) (2024-01-22T12:49:08Z) - Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。
Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
論文 参考訳(メタデータ) (2023-04-05T01:21:00Z) - 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) - 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) - 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) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。