論文の概要: Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability

• arxiv url: http://arxiv.org/abs/2605.28602v1
• Date: Wed, 27 May 2026 15:18:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-28 17:38:56.15684
• Title: Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
• Title（参考訳）: LLMによる満足度判定:推論能力の整合性評価
• Authors: Leizhen Zhang, Shuhan Chen, Sheng Chen,
• Abstract要約: 大規模言語モデル (LLM) は、暗黙的にBoolean satisfiability (SAT) に還元されるタスクに、ますます使われている。 本稿では,2-SATと3-SATのLCMについて,Vertex Coverと離散3Dパッキングの2つの標準化とともに系統的研究を行った。
• 参考スコア（独自算出の注目度）: 8.964195566025824
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) are increasingly used for tasks that implicitly reduce to Boolean satisfiability (SAT), yet their reasoning ability on SAT remains unclear. We present a systematic study of LLMs on 2-SAT and 3-SAT, together with two canonical reductions, Vertex Cover and discrete 3D packing, to probe representation-invariant reasoning. We first evaluate models using conventional metrics, including accuracy, precision, recall, and F1, as well as the SAT phase-transition setting. We find that these metrics can be misleading: many models obtain high scores by over-predicting satisfiable formulas, fail to reproduce the classical easy-hard-easy signature around the 3-SAT threshold, and degrade sharply as the number of variables grows. To address this problem, we introduce a paired-formula protocol based on minimally different satisfiable and unsatisfiable instances, together with Accurate Differentiation Rate (ADR), which requires both members of each pair to be classified correctly. ADR separates reasoning-oriented models from heuristic ones and correlates with witness validity. Beyond CNF, we test cross-representation consistency by converting CNF to Vertex Cover and 3-SAT to discrete 3D packing. Model decisions on CNF and on the corresponding graph or packing instances agree for most models on more than 80 percent of instances, suggesting stable decision rules across representations. Overall, our results show that SAT is a conservative probe for LLM reasoning, and that paired evaluation with ADR provides a more faithful and representation-robust assessment than conventional metrics.
• Abstract（参考訳）: 大規模言語モデル (LLMs) は、暗黙的にBoolean satisfiability (SAT) に還元されるタスクにますます使われているが、SAT上での推論能力は未だ不明である。 本研究では, 2-SAT と 3-SAT 上の LLM について, 2-SAT と 3-SAT の2つの正準還元,Vertex Cover と離散3D のパッキングを用いて,表現不変推論の探索を行う。 まず、SAT位相遷移設定だけでなく、精度、精度、リコール、F1といった従来の測定値を用いてモデルを評価する。 多くのモデルは、満足できる式を過度に予測することで高いスコアを得ることができ、3SATしきい値の周りで古典的な難解なシグネチャを再現することができず、変数の数が増加するにつれて急激に減少する。 この問題に対処するために、各ペアの双方のメンバを正しく分類する必要がある精度微分率(ADR)とともに、最小限に異なる満足度と不満足度を持つインスタンスをベースとしたペア形式プロトコルを導入する。 ADRは推論指向モデルとヒューリスティックモデルとを分離し、証人正当性と相関する。 CNF以外にも、CNFをVertex Cover、3SATを離散3Dパッキングに変換することで、相互表現整合性をテストする。 CNFと対応するグラフやパッキングインスタンスのモデル決定は、80%以上のインスタンス上のほとんどのモデルで一致しており、表現全体で安定した決定ルールが提案されている。 以上の結果から,SATはLCM推論の保守的調査であり,ADRと組み合わせた評価により,従来の測定値よりも忠実で表現力に富んだ評価が得られた。

関連論文リスト

• Ensemble-Based Uncertainty Estimation for Code Correctness Estimation [36.53771380869671]
  本研究では,モデルアンサンブル全体で集約されたサンプルの一貫性を評価することにより,不確実性を推定するEnsemble Semantic Entropy (ESE)を提案する。 LiveCodeBenchの実験では、ESEはシングルモデルセマンティックエントロピーよりもプログラムの正確性に強く関連している。 また、単一モデルスケーリングと比較してFLOPを64.9%削減しながら性能を維持できるカスケーディングテストタイムスケーリングフレームワークCasを提案する。
  論文  参考訳（メタデータ） (2026-03-28T02:37:36Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• Evaluating Robustness of Reasoning Models on Parameterized Logical Problems [20.78623024814435]
  LogicはLSMベースの推論を評価するための制御されたテストベッドを提供する。 SATスタイルの標準ベンチマークでは、表面の難易度(長さ、単語、節順)を実際に満足度を決定する構造現象と区別することが多い。 構造化2-CNF式をパラメータ化して構築した2-SATの診断ベンチマークを提案する。
  論文  参考訳（メタデータ） (2026-02-13T06:54:25Z)
• RoParQ: Paraphrase-Aware Alignment of Large Language Models Towards Robustness to Paraphrased Questions [0.0]
  大規模言語モデル(LLM)は、パラフレーズ付き質問に答えるときに矛盾する振る舞いを示すことが多い。 クローズドブック多重選択QAにおけるクロスパラフレーズ一貫性を評価するベンチマークであるRoParQを紹介する。 また、モデルのロバスト性を定量化する新しい評価指標XParaConを提案する。
  論文  参考訳（メタデータ） (2025-11-26T16:40:53Z)
• DistJoin: A Decoupled Join Cardinality Estimator based on Adaptive Neural Predicate Modulation [11.506172695239576]
  多自己回帰モデルを用いた効率的な分布予測に基づく結合濃度推定器DistJoinを紹介する。 DistJoinは、データ更新に対する高い正確性、堅牢性、汎用性、および既存のメソッドに対する同等の更新と推論速度を緩和することを示した。
  論文  参考訳（メタデータ） (2025-03-12T02:07:08Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  意味的妥当性を評価するため,LogProbsの有効性と基本的なプロンプトを評価した。 LogProbsは、直接ゼロショットプロンプトよりも、より信頼性の高いセマンティックな妥当性を提供する。 我々は,プロンプトベースの評価の時代においても,LogProbsは意味的妥当性の有用な指標である,と結論付けた。
  論文  参考訳（メタデータ） (2024-03-21T22:08:44Z)
• Noisy-Correspondence Learning for Text-to-Image Person Re-identification [50.07634676709067]
  本稿では,雑音対応においても頑健な視覚関係を学習するための新しいロバスト二重埋め込み法(RDE)を提案する。 提案手法は,3つのデータセット上での合成ノイズ対応と非合成ノイズ対応を両立させる。
  論文  参考訳（メタデータ） (2023-08-19T05:34:13Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
  確率感性決定図は、解離ゲートの入力が確率値によってアノテートされる論理回路である。 我々は、局所確率を質量関数のクレーダル集合に置き換えることができる確率の一般化である、クレーダル感性決定図を開発する。 まず,ノイズの多い7セグメント表示画像に基づく簡単なアプリケーションについて検討する。
  論文  参考訳（メタデータ） (2020-08-19T16:04:34Z)

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

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