論文の概要: SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas

• arxiv url: http://arxiv.org/abs/2505.14615v2
• Date: Mon, 22 Sep 2025 08:20:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-23 14:36:45.08625
• Title: SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
• Title（参考訳）: SATBench:SAT式からの自動ノズル生成によるLCMの論理推論のベンチマーク
• Authors: Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, Alex Aiken,
• Abstract要約: 本稿では,大規模言語モデルの論理的推論能力を評価するベンチマークであるSATBenchを紹介する。 SATBenchの各インスタンスはSAT式から生成され、LLMを使用してパズルに変換される。 実験によると、最強のモデルであるo4-miniでさえ、ハードUNSAT問題において65.0%の精度しか達成していない。
• 参考スコア（独自算出の注目度）: 33.329938165116886
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce SATBench, a benchmark for evaluating the logical reasoning capabilities of large language models (LLMs) through logical puzzles derived from Boolean satisfiability (SAT) problems. Unlike prior work that focuses on inference rule-based reasoning, which often involves deducing conclusions from a set of premises, our approach leverages the search-based nature of SAT problems, where the objective is to find a solution that fulfills a specified set of logical constraints. Each instance in SATBench is generated from a SAT formula, then translated into a puzzle using LLMs. The generation process is fully automated and allows for adjustable difficulty by varying the number of clauses. All 2100 puzzles are validated through both LLM-based and solver-based consistency checks, with human validation on a subset. Experimental results show that even the strongest model, o4-mini, achieves only 65.0% accuracy on hard UNSAT problems, close to the random baseline of 50%. Our error analysis reveals systematic failures such as satisfiability bias, context inconsistency, and condition omission, highlighting limitations of current LLMs in search-based logical reasoning. Our code and data are publicly available at https://github.com/Anjiang-Wei/SATBench
• Abstract（参考訳）: 本稿では,大規模言語モデル(LLM)の論理的推論能力を評価するベンチマークであるSATBenchを紹介する。 前提条件の集合から結論を導出することを伴う推論規則に基づく推論に重点を置く従来の作業とは異なり,本手法はSAT問題の探索に基づく性質を利用しており,その目的は論理的制約の集合を満たす解を見つけることである。 SATBenchの各インスタンスはSAT式から生成され、LLMを使用してパズルに変換される。 生成プロセスは完全に自動化され、節数を変えて調整可能な難易度を実現する。 2100のパズルはすべて、LLMベースとソルバベースの両方の一貫性チェックを通じて検証され、サブセット上で人間による検証が行われる。 実験結果によると、最強のモデルであるo4-miniでさえ、強いUNSAT問題に対して65.0%の精度しか達成していない。 我々の誤り解析は, 検索に基づく論理的推論において, 現在のLLMの限界を浮き彫りにして, 満足度バイアス, コンテキスト不整合, 条件不整合などの系統的障害を明らかにする。 私たちのコードとデータはhttps://github.com/Anjiang-Wei/SATBenchで公開されています。

関連論文リスト

• Logic-of-Thought: Empowering Large Language Models with Logic Programs for Solving Puzzles in Natural Language [67.51318974970985]
  自然言語でパズルを解くことは、AIにおける長年の課題である。 本稿では,大規模言語モデルを論理プログラミングでブリッジするフレームワークであるLogic-of-Thoughtを提案する。 動作を含む様々なグリッドパズルや動的パズルについて評価し、全てのタスクにおいてほぼ完璧な精度を示す。
  論文  参考訳（メタデータ） (2025-05-22T01:37:40Z)
• SolSearch: An LLM-Driven Framework for Efficient SAT-Solving Code Generation [13.056487325961688]
  Satisfiability(SAT)問題は、ソフトウェア工学における重要な応用において、中核的な課題である。 本稿では,大規模言語モデル(LLM)を利用してSAT解決戦略の自動発見と最適化を行う新しいフレームワークであるSolSearchを提案する。
  論文  参考訳（メタデータ） (2025-02-20T07:25:21Z)
• On Memorization of Large Language Models in Logical Reasoning [70.94164038947078]
  大きな言語モデル(LLM)は、挑戦的な推論ベンチマークで優れたパフォーマンスを達成するが、基本的な推論ミスを発生させることもできる。 1つの仮説は、より高度でほぼ飽和した性能は、類似した問題の記憶が原因ではないかというものである。 微調整は暗記を重くするが,常に一般化性能を向上することを示す。
  論文  参考訳（メタデータ） (2024-10-30T15:31:54Z)
• General Method for Solving Four Types of SAT Problems [12.28597116379225]
  既存の方法は、様々なタイプのブール適合性問題(SAT)に対して様々なアルゴリズムを提供する。 本研究では,整数計画法と強化学習法(RL)に基づく統合フレームワークDCSATを提案する。
  論文  参考訳（メタデータ） (2023-12-27T06:09:48Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。 われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
  論文  参考訳（メタデータ） (2023-06-09T22:53:16Z)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  大規模言語モデル(LLM)は人間のような推論能力を示しているが、それでも複雑な論理的問題に悩まされている。 本稿では,論理問題の解法を改善するために,LLMとシンボリックソルバを統合した新しいフレームワークであるLogic-LMを紹介する。
  論文  参考訳（メタデータ） (2023-05-20T22:25:38Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• 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)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。 SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。 SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。 実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
  論文  参考訳（メタデータ） (2022-09-02T11:17:39Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。 DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
  論文  参考訳（メタデータ） (2022-05-27T03:20:42Z)
• 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)

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

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