論文の概要: Can Transformers Reason Logically? A Study in SAT Solving

• arxiv url: http://arxiv.org/abs/2410.07432v2
• Date: Sat, 08 Feb 2025 02:12:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-11 14:26:37.371628
• Title: Can Transformers Reason Logically? A Study in SAT Solving
• Title（参考訳）: トランスフォーマーは論理的に推論できるか?SATソルビングの研究
• Authors: Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee,
• Abstract要約: 本研究では,デコーダのみのトランスフォーマーの論理的推論能力について,SAT問題の観点から検討する。 我々は,デコーダのみのトランスフォーマーが,Chain-of-Thought (CoT) によるバックトラックとデダクションを用いて,一様でない計算モデルで 3-SAT を決定できることを示す。
• 参考スコア（独自算出の注目度）: 17.15701291424892
• License:
• Abstract: We formally study the logical reasoning capabilities of decoder-only Transformers in the context of the boolean satisfiability (SAT) problem. First, we prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, using backtracking and deduction via Chain-of-Thought (CoT). %We prove its correctness by showing trace equivalence to the well-known DPLL SAT-solving algorithm. Second, we implement our construction as a PyTorch model with a tool (PARAT) that we designed to empirically demonstrate its correctness and investigate its properties. Third, rather than \textit{programming} a transformer to reason, we evaluate empirically whether it can be \textit{trained} to do so by learning directly from algorithmic traces (``reasoning paths'') from our theoretical construction. The trained models demonstrate strong out-of-distribution generalization on problem sizes seen during training but has limited length generalization, which is consistent with the implications of our theoretical result
• Abstract（参考訳）: 本稿では,復号器のみの変換器の論理的論理的推論能力について,論理的論理的論理的論理的推論能力について,論理的論理的論理的論理的論理的論理的論理的解法(SAT)を用いて研究する。 まず,デコーダのみのトランスフォーマーが,Chain-of-Thought (CoT) によるバックトラックとデダクションを用いて,一様でない計算モデルで 3-SAT を決定できることを示す。 % DPLL SAT-solving アルゴリズムにトレース等価性を示すことにより,その正当性を証明した。 第二に、我々はPyTorchモデルをツール(PARAT)で実装し、その正しさを実証的に証明し、その特性を調査するように設計した。 第3に, 理論的構成からアルゴリズム的トレース (`reasoning paths'') から直接学習することで, 解析が可能であるかどうかを実証的に評価した。 訓練されたモデルは、トレーニング中に見られる問題サイズに強い分布の一般化を示すが、我々の理論的結果に一致する長さの一般化を持つ。

関連論文リスト

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  高速SAT問題生成のためのハードウェアアクセラレーションアルゴリズムと幾何SAT符号化を導入する。 これらの進歩により、何千もの変数と数万の節でSAT問題へのアプローチをスケールできます。 私たちの研究の基本的な側面は、SATデータの本質と、機械学習モデルのトレーニングに適合する可能性に関するものです。
  論文  参考訳（メタデータ） (2024-10-18T22:25:54Z)
• Can Transformers Learn $n$-gram Language Models? [77.35809823602307]
  2種類のランダムな$n$-gram LMを学習するトランスフォーマーの能力について検討する。 例えば、$n$-gram LMに対する古典的な推定手法として、add-$lambda$ smoothing outperform transformerがある。
  論文  参考訳（メタデータ） (2024-10-03T21:21:02Z)
• Chain of Thought Empowers Transformers to Solve Inherently Serial Problems [57.58801785642868]
  思考の連鎖(CoT)は、算術や記号的推論タスクにおいて、大きな言語モデル(LLM)の精度を向上させるための非常に効果的な方法である。 この研究は、表現性のレンズを通してデコーダのみの変換器に対するCoTのパワーを理論的に理解する。
  論文  参考訳（メタデータ） (2024-02-20T10:11:03Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Learning Reliable Logical Rules with SATNet [7.951021955925275]
  我々は、入力出力の例から基礎となるルールを学習する差別化可能なMaxSATソルバSATNetの上に構築する。 基礎的真理規則に対して有効な検証手法をいくつか導入する。 ストリームトランスフォーメーションとスドク問題に関する実験は、デコードされたルールが信頼性が高いことを示している。
  論文  参考訳（メタデータ） (2023-10-03T15:14:28Z)
• Tracr: Compiled Transformers as a Laboratory for Interpretability [15.76027393879609]
  人間の読みやすいプログラムをデコーダのみのトランスフォーマーモデルに"コンパイル"する方法を示す。 コンパイラであるTrcrは、既知の構造を持つモデルを生成する。 マルチステップアルゴリズムを実行する変換器の「重ね合わせ」について検討する。
  論文  参考訳（メタデータ） (2023-01-12T14:59:19Z)
• Transformers Learn Shortcuts to Automata [52.015990420075944]
  低深度変換器は任意の有限状態オートマトンを計算できる。 我々は,$O(log T)$レイヤを持つ変換器が,長さ$T$の入力シーケンス上で,オートマトンを正確に再現可能であることを示す。 さらに、これらの解の脆性について検討し、潜在的な緩和を提案する。
  論文  参考訳（メタデータ） (2022-10-19T17:45:48Z)
• 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)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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