論文の概要: The Computational Complexity of Formal Reasoning for Encoder-Only Transformers

• arxiv url: http://arxiv.org/abs/2405.18548v1
• Date: Tue, 28 May 2024 19:30:43 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-30 21:53:22.910072
• Title: The Computational Complexity of Formal Reasoning for Encoder-Only Transformers
• Title（参考訳）: エンコーダオンリー変圧器の形式推論の計算複雑性
• Authors: Marco Sälzer, Eric Alsmann, Martin Lange,
• Abstract要約: エンコーダのみの変圧器(EOT)の形式推論の課題と可能性について検討する。 EOTを考えるとSATは決定不可能であり,表現性コミュニティでは一般的に考慮されている。 自明なケースの他に、量子化されたEOT、すなわち固定幅の算術で制限されたEOTは、その注意力の制限によりSATの決定可能性に繋がる。
• 参考スコア（独自算出の注目度）: 4.096453902709292
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We investigate challenges and possibilities of formal reasoning for encoder-only transformers (EOT), meaning sound and complete methods for verifying or interpreting behaviour. In detail, we condense related formal reasoning tasks in the form of a naturally occurring satisfiability problem (SAT). We find that SAT is undecidable if we consider EOT, commonly considered in the expressiveness community. Furthermore, we identify practical scenarios where SAT is decidable and establish corresponding complexity bounds. Besides trivial cases, we find that quantized EOT, namely those restricted by some fixed-width arithmetic, lead to the decidability of SAT due to their limited attention capabilities. However, the problem remains difficult, as we establish those scenarios where SAT is NEXPTIME-hard and those where we can show that it is solvable in NEXPTIME for quantized EOT. To complement our theoretical results, we put our findings and their implications in the overall perspective of formal reasoning.
• Abstract（参考訳）: 本研究では,エンコーダのみの変圧器(EOT)の形式的推論の課題と可能性について検討する。 本稿では,自然発生型満足度問題(SAT)の形で,関連する形式的推論タスクを凝縮する。 EOTを考えるとSATは決定不可能であり,表現性コミュニティでは一般的に考慮されている。 さらに,SATが決定可能な現実シナリオを特定し,それに対応する複雑性境界を確立する。 自明なケースの他に、量子化されたEOT、すなわち固定幅の算術で制限されたEOTは、その注意力の制限によりSATの決定可能性に繋がる。 しかし、SAT が NEXPTIME ハードなシナリオと、量子化された EOT に対して NEXPTIME で解決可能であることを示すシナリオを確立することは困難である。 理論的結果を補完するため, フォーマルな推論の全体的視点において, 研究結果とその意義を考察した。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation [1.5201992393140886]
  並列量子SATソルバは,線形時間 O(m) から定数時間 O(1) までの繰り返しの時間複雑性を,余分な絡み合った量子ビットを用いて低減する。 我々は、我々のアプローチの正しさを証明し、シミュレーションでそれらを実証した。
  論文  参考訳（メタデータ） (2023-08-07T06:52:06Z)
• Evolutionary Diversity Optimisation in Constructing Satisfying Assignments [20.386139395296215]
  本稿では,EDOの文脈におけるブール充足可能性問題(SAT)について検討する。 SATは計算機科学において非常に重要であり、KPやTSPといったEDO文献で研究されている他の問題とは異なる。 本稿では,SAT解の集合間の多様性を明示的に最大化するために,よく知られたSATソルバを用いた進化的アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-05-19T06:26:10Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  振幅増幅アルゴリズムは、可変代入を満たすために非構造化探索に適用することができる。 Quantum Approximate Optimization Algorithm (QAOA)は、ノイズのある中間量子デバイスのための3SATを解くための有望な候補である。 振幅増幅によるQAOAの変種を導入し、3SATの成功確率を改善する。
  論文  参考訳（メタデータ） (2023-03-02T11:52:39Z)
• 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)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。 ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
  論文  参考訳（メタデータ） (2022-03-02T05:14:12Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Comprehensible Counterfactual Explanation on Kolmogorov-Smirnov Test [56.5373227424117]
  我々は,KSテストに失敗するテストデータに対して,反実的説明を生成する問題に対処する。 我々は、KSテストに失敗したテストセットの指数的なサブセット数を列挙し、チェックするのを避ける効率的なアルゴリズムMOCHEを開発した。
  論文  参考訳（メタデータ） (2020-11-01T06:46:01Z)
• Pareto Probing: Trading Off Accuracy for Complexity [87.09294772742737]
  我々は,プローブの複雑性と性能の基本的なトレードオフを反映したプローブ計量について論じる。 係り受け解析による実験により,文脈表現と非文脈表現の統語的知識の幅広いギャップが明らかとなった。
  論文  参考訳（メタデータ） (2020-10-05T17:27:31Z)

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

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