論文の概要: Investigations into Proof Structures

• arxiv url: http://arxiv.org/abs/2304.12827v3
• Date: Wed, 30 Oct 2024 09:55:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-31 14:22:34.737643
• Title: Investigations into Proof Structures
• Title（参考訳）: 証明構造の研究
• Authors: Christoph Wernhard, Wolfgang Bibel,
• Abstract要約: 我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。 これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
• 参考スコア（独自算出の注目度）: 0.8287206589886879
• License:
• Abstract: We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to {\L}ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of {\L}ukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.
• Abstract（参考訳）: 我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。 この最初のアプローチでは、形式主義は凝縮された分離によって特徴づけられる一階問題に制限される。 これは、コヒーレントで包括的な形式的な再構成と {\L}ukasiewicz による広く研究されている問題の歴史的証明の分析に例示的に適用される。 基礎となるアプローチは、探索の労力を減らし、より短い証明を見つけるために、証明探索の過程で補題を生成する新しい体系的な方法への扉を開く。 この線に沿って報告された多くの実験の中で、人間や機械によって発見されたどの証明よりもはるかに短いことが自動的に発見された。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• A Survey on Deep Learning for Theorem Proving [16.28502772608166]
  定理証明は数学の基本的な側面であり、自然言語における非公式な推論から形式体系における厳密な導出にまで及ぶ。 ディープラーニング、特に大きな言語モデルの出現は、定理証明のプロセスを強化するためにこれらの技術を探究する研究の顕著な急増を引き起こした。
  論文  参考訳（メタデータ） (2024-04-15T17:07:55Z)
• Rethinking Complex Queries on Knowledge Graphs with Neural Link Predictors [58.340159346749964]
  本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。 これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。 提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
  論文  参考訳（メタデータ） (2023-04-14T11:35:35Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• The Familiarity Hypothesis: Explaining the Behavior of Deep Open Set Methods [86.39044549664189]
  特徴ベクトルデータに対する異常検出アルゴリズムは異常を外れ値として識別するが、外れ値検出はディープラーニングではうまく機能しない。 本論文は, 新規性の有無ではなく, 慣れ親しんだ特徴の欠如を検知しているため, これらの手法が成功するというFamiliarity仮説を提案する。 本論文は,親しみやすさの検出が表現学習の必然的な結果であるかどうかを論じる。
  論文  参考訳（メタデータ） (2022-03-04T18:32:58Z)
• Formal Mathematics Statement Curriculum Learning [64.45821687940946]
  同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。 また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
  論文  参考訳（メタデータ） (2022-02-03T00:17:00Z)
• Structural Causal Models Reveal Confounder Bias in Linear Program Modelling [26.173103098250678]
  この現象が自然界においてより一般的なものなのか、つまり古典的な分類タスク以外の敵型攻撃なのかを考察する。 具体的には,線形プログラム(LP)の基本クラスを考える。 構造因果モデル(SCM)のその後のLP最適化に対する直接的な影響を示す。
  論文  参考訳（メタデータ） (2021-05-26T17:19:22Z)
• Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version) [4.111899441919164]
  本稿では,選択問題におけるグローバル特徴とその証明について検討する。 研究対象の課題は"axiom(s)"と" rule(s) imply goal(s)"の広義の形式である。
  論文  参考訳（メタデータ） (2021-04-28T09:09:20Z)
• Understanding the QuickXPlain Algorithm: Simple Explanation and Formal Proof [0.0]
  本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。 他のアルゴリズムを証明するためのガイダンスとして使用できる。 また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
  論文  参考訳（メタデータ） (2020-01-07T01:37:41Z)

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

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