論文の概要: CD Tools -- Condensed Detachment and Structure Generating Theorem
Proving (System Description)
- arxiv url: http://arxiv.org/abs/2207.08453v1
- Date: Mon, 18 Jul 2022 09:15:08 GMT
- ステータス: 処理完了
- システム内更新日: 2022-07-19 18:20:08.527508
- Title: CD Tools -- Condensed Detachment and Structure Generating Theorem
Proving (System Description)
- Title(参考訳): CDツール -- 凝縮した剥離と理論証明を生成する構造(システム記述)
- Authors: Christoph Wernhard
- Abstract要約: CD Toolsは、一階ATPの凝縮した剥離の実験のためのPrologライブラリである。
一階ATPの観点からすると、凝縮した分枝は比較的単純だが本質的な特徴と真剣な応用を持つ設定を提供する。
ATPでよく研究される歴史的な問題のために、既知のものよりもはるかに短い新しい証明を生み出した。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: CD Tools is a Prolog library for experimenting with condensed detachment in
first-order ATP, which puts a recent formal view centered around proof
structures into practice. From the viewpoint of first-order ATP, condensed
detachment offers a setting that is relatively simple but with essential
features and serious applications, making it attractive as a basis for
developing and evaluating novel techniques. CD Tools includes specialized
provers based on the enumeration of proof structures. We focus here on one of
these, SGCD, which permits to blend goal- and axiom-driven proof search in
particularly flexible ways. In purely goal-driven configurations it acts
similarly to a prover of the clausal tableaux or connection method family. In
blended configurations its performance is much stronger, close to
state-of-the-art provers, while emitting relatively short proofs. Experiments
show characteristics and application possibilities of the structure generating
approach realized by that prover. For a historic problem often studied in ATP
it produced a new proof that is much shorter than any known one.
- Abstract(参考訳): CD Toolsは、一階ATPの凝縮した剥離を実験するためのPrologライブラリである。
一階ATPの観点から見ると、凝縮した分枝は比較的単純だが本質的な特徴と真剣な応用をもち、新規技術の開発と評価の基礎として魅力的である。
cdツールは証明構造の列挙に基づく特殊なプロバーを含んでいる。
SGCDは、ゴールと公理駆動の証明検索を、特に柔軟な方法で組み合わせることを可能にします。
純粋に目標駆動の構成では、これはクローサルテーブルまたは接続メソッドファミリの証明器と同様に振る舞う。
ブレンド構成では、その性能はより強く、最先端のプローバーに近いが、比較的短い証明を出力する。
実験は, その証明者が実現した構造生成手法の特性と応用可能性を示す。
ATPでよく研究される歴史的な問題のために、既知のものよりもはるかに短い新しい証明を生み出した。
関連論文リスト
- Navigating the Structured What-If Spaces: Counterfactual Generation via
Structured Diffusion [20.20945739504847]
本稿では,構造データ中の反現実的説明を生成するために拡散を利用した最初のプラグアンドプレイフレームワークであるStructured Counterfactual diffuser(SCD)を紹介する。
実験の結果, 既存の最先端技術と比較して高い妥当性を示すだけでなく, 近接性や多様性も著しく向上していることがわかった。
論文 参考訳(メタデータ) (2023-12-21T07:05:21Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - Investigations into Proof Structures [2.7412662946127755]
我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。
これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
論文 参考訳(メタデータ) (2023-02-14T12:29:39Z) - Decoding Structure-Spectrum Relationships with Physically Organized
Latent Spaces [6.36075035468233]
構造スペクトル関係の発見のための半教師付き機械学習手法を開発し,実証した。
本手法は,個々の構造記述子とスペクトル傾向の1対1マッピングを構成する。
RankAAE法は連続的かつ解釈可能な潜在空間を生成し、各次元は個々の構造記述子を追跡することができる。
論文 参考訳(メタデータ) (2023-01-11T21:30:22Z) - Generating Compressed Combinatory Proof Structures -- An Approach to
Automated First-Order Theorem Proving [0.0]
ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。
このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
論文 参考訳(メタデータ) (2022-09-26T11:23:17Z) - Entailment Tree Explanations via Iterative Retrieval-Generation Reasoner [56.08919422452905]
我々はIRGR(Iterative Retrieval-Generation Reasoner)と呼ばれるアーキテクチャを提案する。
本モデルでは,テキストの前提からステップバイステップの説明を体系的に生成することにより,与えられた仮説を説明することができる。
前提条件の検索と細分化木の生成に関する既存のベンチマークを上回り、全体の正しさはおよそ300%向上した。
論文 参考訳(メタデータ) (2022-05-18T21:52:11Z) - METGEN: A Module-Based Entailment Tree Generation Framework for Answer
Explanation [59.33241627273023]
複数のモジュールと推論コントローラを備えたモジュールベースのEntailment Tree GENフレームワークMETGENを提案する。
質問に対して、METGENは、別々のモジュールで単一ステップのエンタテインメントを実行し、コントローラで推論フローを選択することで、エンタテインメントツリーを反復的に生成することができる。
実験の結果,METGENは従来の最先端モデルよりも9%のパラメータで優れていた。
論文 参考訳(メタデータ) (2022-05-05T12:06:02Z) - GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
本稿では,ジェネレーション方式で証拠を検索する最初のシステムであるGEREを提案する。
FEVERデータセットの実験結果は、GEREが最先端のベースラインよりも大幅に改善されていることを示している。
論文 参考訳(メタデータ) (2022-04-12T03:49:35Z) - A convergent inflation hierarchy for quantum causal structures [1.6758573326215689]
因果構造は、確率変数間の関数的依存関係の記述である。
インフレ技術は因果構造を、ますます厳密な互換性テストの階層に関連付ける。
本稿では,量子インフレーション階層の最初のバージョンを構築する。
論文 参考訳(メタデータ) (2021-10-27T18:00:02Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳(メタデータ) (2021-06-02T17:58:35Z) - Searching Central Difference Convolutional Networks for Face
Anti-Spoofing [68.77468465774267]
顔認識システムにおいて、顔の反偽造(FAS)が重要な役割を担っている。
最先端のFASメソッドの多くは、スタック化された畳み込みと専門家が設計したネットワークに依存している。
ここでは、中央差分畳み込み(CDC)に基づくフレームレベルの新しいFAS手法を提案する。
論文 参考訳(メタデータ) (2020-03-09T12:48:37Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。