論文の概要: Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

• arxiv url: http://arxiv.org/abs/2104.13645v1
• Date: Wed, 28 Apr 2021 09:09:20 GMT
• ステータス: 処理完了
• システム内更新日: 2021-04-29 12:42:24.274338
• Title: Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
• Title（参考訳）: L}ukasiewicz と Meredith から学ぶ:証明構造の研究(拡張版)
• Authors: Christoph Wernhard and Wolfgang Bibel
• Abstract要約: 本稿では,選択問題におけるグローバル特徴とその証明について検討する。 研究対象の課題は"axiom(s)"と" rule(s) imply goal(s)"の広義の形式である。
• 参考スコア（独自算出の注目度）: 4.111899441919164
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by {\L}ukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.
• Abstract（参考訳）: 本論文で提示された資料は,自動推論の実質的進歩に不可欠な基礎を確立するのに寄与する。 選択された問題のグローバル特徴と、より直接的な方法で証明探索を導く可能性を提供するそれらの証明を特定し、研究する。 研究された問題は、"axiom(s)" と " rule(s) imply goal(s)" の広義の形式である。 その特徴には、よく知られたレムマの概念が含まれる。 そのため、選択された定理の人間的証明と自動証明の両方が密接に比較検討される。 同時にこの研究は、キュカシエヴィチ、メレディスらによる歴史的著作の一貫性と包括的な形式的な再構築を論じている。 この研究から得られた最初の実験は、様々な家族の自動化された一階述語を補う新しい補題生成法を示し、特に短い証明を見つける能力を強化した。

関連論文リスト

• Theoretical Foundations of Conformal Prediction [15.884682750072399]
  コンフォーマルな予測と関連する推論技術は、多様なタスクの配列で有用である。 コンフォーマル予測の主な魅力は、正式な有限サンプル保証を提供する能力である。 本書の目的は、共形予測を研究する際に生じる基本的な技術的議論について読者に教えることである。
  論文  参考訳（メタデータ） (2024-11-18T18:44:00Z)
• Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
  I-FKGC(inductive few-shot knowledge graph completion)と呼ばれる課題に焦点をあてる。 帰納的推論(inductive reasoning)の概念に着想を得て,I-FKGCを帰納的推論問題とした。 本稿では,仮説の連成分布をモデル化したニューラルプロセスに基づく仮説抽出器を提案する。 第2のモジュールでは、この仮説に基づいて、クエリセットのトリプルが抽出された仮説と一致するかどうかをテストするグラフアテンションベースの予測器を提案する。
  論文  参考訳（メタデータ） (2024-08-03T13:37:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Class-wise Activation Unravelling the Engima of Deep Double Descent [0.0]
  二重降下は、機械学習領域内の反直観的な側面を示す。 本研究では,二重降下現象を再考し,その発生状況について考察した。
  論文  参考訳（メタデータ） (2024-05-13T12:07:48Z)
• A Survey on Deep Learning for Theorem Proving [16.28502772608166]
  定理証明は数学の基本的な側面であり、自然言語における非公式な推論から形式体系における厳密な導出にまで及ぶ。 ディープラーニング、特に大きな言語モデルの出現は、定理証明のプロセスを強化するためにこれらの技術を探究する研究の顕著な急増を引き起こした。
  論文  参考訳（メタデータ） (2024-04-15T17:07:55Z)
• Seeing Unseen: Discover Novel Biomedical Concepts via Geometry-Constrained Probabilistic Modeling [53.7117640028211]
  同定された問題を解決するために,幾何制約付き確率的モデリング処理を提案する。 構成された埋め込み空間のレイアウトに適切な制約を課すために、重要な幾何学的性質のスイートを組み込む。 スペクトルグラフ理論法は、潜在的な新規クラスの数を推定するために考案された。
  論文  参考訳（メタデータ） (2024-03-02T00:56:05Z)
• Machine learning assisted exploration for affine Deligne-Lusztig varieties [3.7863170254779335]
  本稿では,ADLV(Affine Deligne-Lusztig variety)の幾何学を探索するために,機械学習支援フレームワークを活用した学際研究を提案する。 主な目的は, ADLVの既約成分の空白パターン, 寸法, 列挙について検討することである。 我々は、ある下界の次元に関する新たに特定された問題の完全な数学的証明を提供する。
  論文  参考訳（メタデータ） (2023-08-22T11:12:53Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。 これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。 提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
  論文  参考訳（メタデータ） (2023-04-14T11:35:35Z)
• Investigations into Proof Structures [0.8287206589886879]
  我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。 これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
  論文  参考訳（メタデータ） (2023-02-14T12:29:39Z)
• Alchemy: A structured task distribution for meta-reinforcement learning [52.75769317355963]
  本稿では,構造的リッチネスと構造的透明性を組み合わせたメタRL研究のための新しいベンチマークを提案する。 Alchemyは3Dビデオゲームで、エピソードからエピソードまで手続き的に再サンプリングされる潜伏した因果構造を含んでいる。 本稿では,アルケミーの強力なRL剤について検討し,その1つについて詳細な分析を行った。
  論文  参考訳（メタデータ） (2021-02-04T23:40:44Z)
• Summarizing Text on Any Aspects: A Knowledge-Informed Weakly-Supervised Approach [89.56158561087209]
  文書に関連する任意の側面を要約する。 監視データがないため、我々は新しい弱い監督構築法とアスペクト・モデリング・スキームを開発した。 実験により,本手法は実文書と合成文書の両方を要約することで,性能の向上を図っている。
  論文  参考訳（メタデータ） (2020-10-14T03:20:46Z)

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

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