論文の概要: Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs
- arxiv url: http://arxiv.org/abs/2301.02195v1
- Date: Thu, 5 Jan 2023 17:56:00 GMT
- ステータス: 処理完了
- システム内更新日: 2023-01-06 13:34:13.281013
- Title: Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs
- Title(参考訳): 数学の自己形式化とコードの正確性:初等証明による実験
- Authors: Garett Cunningham, Razvan C. Bunescu, David Juedes
- Abstract要約: オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
- 参考スコア(独自算出の注目度): 5.045988012508899
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The ever-growing complexity of mathematical proofs makes their manual
verification by mathematicians very cognitively demanding. Autoformalization
seeks to address this by translating proofs written in natural language into a
formal representation that is computer-verifiable via interactive theorem
provers. In this paper, we introduce a semantic parsing approach, based on the
Universal Transformer architecture, that translates elementary mathematical
proofs into an equivalent formalization in the language of the Coq interactive
theorem prover. The same architecture is also trained to translate simple
imperative code decorated with Hoare triples into formally verifiable proofs of
correctness in Coq. Experiments on a limited domain of artificial and
human-written proofs show that the models generalize well to intermediate
lengths not seen during training and variations in natural language.
- Abstract(参考訳): 数学的証明の複雑さは、数学者による手作業による検証を非常に認知的に要求する。
自己形式化(autoformalization)は、自然言語で書かれた証明を対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することで、この問題に対処しようとしている。
本稿では,基本的な数学的証明を,対話型定理証明器の言語で等価な形式化に変換する,Universal Transformerアーキテクチャに基づく意味解析手法を提案する。
同じアーキテクチャは、hoareトリプルで装飾された単純な命令型コードを、coqの正しさの形式的検証可能な証明に変換するようにも訓練されている。
有限領域の人工的証明と人文的証明の実験は、モデルが訓練や自然言語の変化の間に見られない中間の長さにうまく一般化していることを示している。
関連論文リスト
- An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳(メタデータ) (2023-12-08T09:32:26Z) - A New Approach Towards Autoformalization [8.176989532546632]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳(メタデータ) (2023-10-12T00:50:24Z) - Trustworthy Formal Natural Language Specifications [3.8073142980733]
本稿では、自然言語の表現的サブセットで書かれた仕様を構築できることを示す。
モジュール的に形式化された英語のサブセットで仕様を提供する手段を実装し、それらを形式的なクレームに自動的に変換する。
我々は,各単語の解釈方法と文の構造を用いて意味を計算したことを示す証明証明書を作成した。
論文 参考訳(メタデータ) (2023-10-05T20:41:47Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳(メタデータ) (2023-02-24T03:28:46Z) - Tree-Based Representation and Generation of Natural and Mathematical
Language [77.34726150561087]
科学コミュニケーションと教育シナリオにおける数学的言語は重要であるが、比較的研究されている。
数学言語に関する最近の研究は、スタンドアローンな数学的表現や、事前訓練された自然言語モデルにおける数学的推論に焦点をあてている。
テキストと数学を共同で表現・生成するために,既存の言語モデルに対する一連の修正を提案する。
論文 参考訳(メタデータ) (2023-02-15T22:38:34Z) - 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) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳(メタデータ) (2021-11-23T17:49:00Z) - NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。
NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。
数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
論文 参考訳(メタデータ) (2021-03-24T03:14:48Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳(メタデータ) (2020-12-20T18:15:12Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。