論文の概要: Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems

• arxiv url: http://arxiv.org/abs/2005.02576v1
• Date: Wed, 6 May 2020 03:29:34 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-06 06:18:48.564417
• Title: Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems
• Title（参考訳）: G\"odel's Two Uncompleteness Theoremsの簡潔で機械的な証明に向けて
• Authors: Elijah Malaby, Bradley Dragun, John Licato
• Abstract要約: 我々は、特異な論理に容易に適応したり、新たな推論プロセスを統合するように設計された、自動定理のための新しいフレームワークMATRを提案する。 我々はMATRの高レベル設計と実装の詳細について説明する。 次に、G"odelの不完全性定理の証明に適した形式化されたメタロジックを記述し、MATRにおける我々のメタロジックを用いて、第一不完全性定理と第二不完全性定理の両方の証明を半自動生成する進捗について報告する。
• 参考スコア（独自算出の注目度）: 3.222802562733787
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: There is an increasing interest in applying recent advances in AI to automated reasoning, as it may provide useful heuristics in reasoning over formalisms in first-order, second-order, or even meta-logics. To facilitate this research, we present MATR, a new framework for automated theorem proving explicitly designed to easily adapt to unusual logics or integrate new reasoning processes. MATR is formalism-agnostic, highly modular, and programmer-friendly. We explain the high-level design of MATR as well as some details of its implementation. To demonstrate MATR's utility, we then describe a formalized metalogic suitable for proofs of G\"odel's Incompleteness Theorems, and report on our progress using our metalogic in MATR to semi-autonomously generate proofs of both the First and Second Incompleteness Theorems.
• Abstract（参考訳）: AIの最近の進歩を自動推論に適用することへの関心が高まっており、一階述語、二階述語、メタ論理学のフォーマリズムを推論する上で有用なヒューリスティックを提供する可能性がある。 そこで本研究では,不規則な論理に容易に適応したり,新たな推論プロセスを統合するように設計された,自動定理のための新しいフレームワークMATRを提案する。 MATRは形式主義に依存しず、モジュール性が高く、プログラマフレンドリーである。 我々は、matrのハイレベルな設計と実装の詳細について説明する。 matrの有用性を示すために、g\"odelの不完全性定理の証明に適した形式化されたメタロジーを記述し、matrのメタロジーを用いて半自律的に第一不完全性定理と第二不完全性定理の両方の証明を生成する。

関連論文リスト

• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Automated Planning Techniques for Elementary Proofs in Abstract Algebra [5.379968204052965]
  抽象代数学における基本証明を構築するための計画法について検討する。 我々は、決定論的領域と非決定論的領域の両方において、基本的な意味、平等、および規則を実装している。 この初期実装の成功は、自動計画で見られる確立されたテクニックが、比較的新しい自動定理証明分野に適用可能であることを示唆している。
  論文  参考訳（メタデータ） (2023-12-11T16:17:43Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [11.096348678079574]
  LAMBADAと呼ばれる逆チェインアルゴリズムは、推論を4つのサブモジュールに分解する。 LAMBADAは最先端のフォワード推論手法よりも精度が向上することを示す。
  論文  参考訳（メタデータ） (2022-12-20T18:06:03Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof [0.0]
  フォーミュラマクロは複雑な公式やタスクを構成するのに使用される。 G"odelの存在論的証明とバリエーションは形式化され、自動ツールで分析される。
  論文  参考訳（メタデータ） (2021-10-21T12:50:23Z)
• 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)

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

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