論文の概要: 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でよく研究される歴史的な問題のために、既知のものよりもはるかに短い新しい証明を生み出した。
関連論文リスト
- Analogous Alignments: Digital "Formally" meets Analog [0.0]
本稿では,デジタルブロックとアナログブロックを組み合わせた混合信号知的特性(IP)の実用的形式検証に着目する。
Digital and Analog Mixed-Signal (AMS)設計は、本質的に異なるが、形式的な検証設定でシームレスに統合される。
論文 参考訳（メタデータ） (2024-09-23T13:38:31Z) - 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) - Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
本稿では,メルクル木包摂証明のためのOR論理に基づく新しい証明集約手法を提案する。
木内の葉の数に依存しない証明サイズを実現し、有効な葉のハッシュ1つを用いて検証を行う。
提案手法は,ゼロ知識証明システムのスケーラビリティ,効率,柔軟性を著しく向上させる可能性がある。
論文 参考訳（メタデータ） (2024-05-13T17:15:38Z) - 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) - Large-scale Pre-trained Models are Surprisingly Strong in Incremental Novel Class Discovery [76.63807209414789]
我々は,クラスiNCDにおける現状問題に挑戦し,クラス発見を継続的に,真に教師なしで行う学習パラダイムを提案する。
凍結したPTMバックボーンと学習可能な線形分類器から構成される単純なベースラインを提案する。
論文 参考訳（メタデータ） (2023-03-28T13:47:16Z) - Investigations into Proof Structures [0.8287206589886879]
我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。
これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
論文 参考訳（メタデータ） (2023-02-14T12:29:39Z) - Generating Compressed Combinatory Proof Structures -- An Approach to
Automated First-Order Theorem Proving [0.0]
ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。
このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
論文 参考訳（メタデータ） (2022-09-26T11:23:17Z) - GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
本稿では,ジェネレーション方式で証拠を検索する最初のシステムであるGEREを提案する。
FEVERデータセットの実験結果は、GEREが最先端のベースラインよりも大幅に改善されていることを示している。
論文 参考訳（メタデータ） (2022-04-12T03:49:35Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。