Fugu-MT 論文翻訳(概要): On Computation Complexity of True Proof Number Search

論文の概要: On Computation Complexity of True Proof Number Search

arxiv url: http://arxiv.org/abs/2102.04907v1
Date: Mon, 8 Feb 2021 06:06:54 GMT
ステータス: 処理完了
システム内更新日: 2021-02-10 14:55:16.886372
Title: On Computation Complexity of True Proof Number Search
Title（参考訳）: 真証明数探索の計算複雑性について
Authors: Chao Gao
Abstract要約: 任意の有向非巡回グラフにおける証明数探索のための真エンフェスト数と真エンフェスト数の計算はNPハードであることを示す。この証明にはSATからの還元が必要であり、任意のDAGに対して真の証明/反証数を見つけることは、任意のSATインスタンスが満足できるかどうかを決定するのと同じくらい難しいことを証明している。
参考スコア（独自算出の注目度）: 19.376328966299322
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: We point out that the computation of true \emph{proof} and \emph{disproof} numbers for proof number search in arbitrary directed acyclic graphs is NP-hard, an important theoretical result for proof number search. The proof requires a reduction from SAT, which demonstrates that finding true proof/disproof number for arbitrary DAG is at least as hard as deciding if arbitrary SAT instance is satisfiable, thus NP-hard.
Abstract（参考訳）: 任意の有向非巡回グラフにおける証明数探索のための真の \emph{proof} と \emph{disproof} の計算はnp-hardであり、証明数探索の重要な理論的結果である。この証明は SAT の減少を必要とし、任意の DAG に対して真の証明/防止番号を見つけることは、少なくとも任意の SAT インスタンスが満足できるかどうかを決定するのと同じくらい困難であり、NP-hard であることが証明される。

関連論文リスト

MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
大規模言語モデル(LLM)は、高い精度で算術語問題を解くことができるが、訓練された言語よりも複雑な問題にどのように一般化するかは、ほとんど分かっていない。本研究では、任意に複雑な算術証明問題に対する LLM の評価フレームワーク、MathGAP を提案する。
論文参考訳（メタデータ） (2024-10-17T12:48:14Z)
ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
論文参考訳（メタデータ） (2024-10-07T05:14:18Z)
Unclonable Non-Interactive Zero-Knowledge [11.013799869152132]
非対話的ZK(NIZK)証明は、秘密を明かさずにNPステートメントの検証を可能にする。本稿では,クローン化が不可能なNIZK証明システムを構築するために,量子情報に頼ることが可能かどうかを問う。
論文参考訳（メタデータ） (2023-10-11T01:32:36Z)
SAT Requires Exhaustive Search [4.959974472811339]
本稿では,計算硬度を証明することは数学では難しくないことを示す。非常に難しい例では、徹底的な検索が唯一の選択肢かもしれない。これにより、SAT(長い節を持つ)と3-SATの分離は、3-SATと2-SATの分離よりもずっと簡単になります。
論文参考訳（メタデータ） (2023-02-19T09:04:17Z)
Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
論文参考訳（メタデータ） (2022-10-04T09:19:13Z)
Connes implies Tsirelson: a simple proof [91.3755431537592]
コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
論文参考訳（メタデータ） (2022-09-16T13:59:42Z)
Who Finds the Short Proof? An Exploration of variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers [62.997667081978825]
本稿では, 高階自動定理証明器を用いたブーロスの興味ある推論の変種探索について報告する。驚いたことに、手動で手書き表記する必要があったのは1つの短い手書き表記のみであった。短い証明を得るために必要な高次の補題はすべて、コンピュータによって自動的に発見される。
論文参考訳（メタデータ） (2022-08-14T16:31:04Z)
Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文参考訳（メタデータ） (2022-05-25T02:22:30Z)
Automating Reasoning with Standpoint Logic via Nested Sequents [0.0]
スタンドポイント論理は多面的アプローチを提唱し、多種多様で恐らく矛盾するスタンドポイントの選択による推論を許容する。非決定論的証明探索アルゴリズムを用いて視点推論を自動化する方法を示す。
論文参考訳（メタデータ） (2022-05-05T16:27:57Z)
multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文参考訳（メタデータ） (2021-06-02T17:58:35Z)
The Long, the Short and the Random [0.0]
アルゴリズムは、サブ指数時間における満足な割り当ての正確なカウントを計算する。このアルゴリズムは、すべてのCNF式が持つ優れた性質を使い、不満足な代入の個数をモノトーン部分形式の空間に関連付けている。
論文参考訳（メタデータ） (2020-11-03T12:00:07Z)

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