論文の概要: Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning
- arxiv url: http://arxiv.org/abs/2607.17047v1
- Date: Sun, 19 Jul 2026 03:23:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.344134
- Title: Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning
- Title（参考訳）: ソルバーハードはモデルハードではない: LLM制約推論のための硬度制御診断
- Authors: Lucky Verma,
- Abstract要約: LLM制約推論器は、ランダム-SAT相転移、共起密度、ソルバ硬度付近でしばしば評価される。
証明ハード展開器と証明易解なラダー・ティチン公式,ハトホールアンカー,密度ミスマッチ制御を比較した。
3つのモデルのうち、ほぼ一致した密度の精度のギャップは、-32$から+20$ポイントまで様々である。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: LLM constraint reasoners are often evaluated near the random-SAT phase transition, confounding density and solver hardness. We test instance-level transfer while near-matching clause density. At aligned size bins, with near-matched density and matched maximum clause width, we compare proof-hard expander-Tseitin and proof-easy ladder-Tseitin formulas, pigeonhole anchors, and density-mismatched controls. Theory separates their resolution hardness; a solver-specific Glucose mean-conflict proxy differs by up to $51\times$, and five other solvers preserve the direction. Across three included models (243 instances each; a fourth is excluded for abstention), the near-matched-density accuracy gaps range from $-32$ to $+20$ points, with a pooled gap of $+1.7$ points ($p=0.74$) and a wrong-signed correctness-versus-conflict association ($r=+0.15$). A proof-preserving relabeling lowers accuracy in all five clusters for one model (mean $-93$ points) but not another, exposing model-surface sensitivity. In a preregistered extension, provider-reported completion-token spend does not consistently increase with the proxy after accounting for formula length and censoring. At 16k, the reasoning model spends more on proof-easy matched formulas and exhausts its budget on the solver-easiest UNSAT family; the 32k C1 gap is absent. These scoped dissociations concern verdict accuracy and observed token spend, not certificate solving, exact proof length, or allocation efficiency.
- Abstract（参考訳）: LLM制約推論器は、ランダム-SAT相転移、共起密度、ソルバ硬度付近でしばしば評価される。
我々は、近マッチング節密度でインスタンスレベルの転送をテストする。
ほぼ整合した密度と最大節幅の整合した大きさのビンでは,証明ハード展開器と証明イージーなラグ・ティチン式,ハトホールアンカー,密度ミスマッチした制御を比較検討した。
解法固有のGlucose平均競合プロキシは、最大で511\times$と異なり、他の5つの解法は方向を保っている。
3つのモデル(それぞれ243のインスタンス)、ほぼ一致した密度の精度のギャップは、$-32$から$+20$ポイント、プールされたギャップは$+1.7$ポイント(p=0.74$)、間違った符号の正確さと矛盾の関連(r=+0.15$)である。
証明保存レザベリングは、1つのモデル(平均$-93$ポイント)の5つのクラスタすべてにおいて精度を低下させるが、もう1つのモデル表面感度を露呈するものではない。
事前登録された拡張では、プロバイダが報告した完了トークンの費用は、公式の長さと検閲を考慮した後、プロキシによって一貫して増加しない。
推理モデルでは16kでは、より証明し易い公式に費やし、解決し易いUNSATファミリーの予算を浪費している。
これらのスコープ化された解離は、証明書の解決、正確な証明の長さ、割当効率などではなく、正確さの検証と観察されたトークンの支出に関するものである。
関連論文リスト
- AI-Assisted Discovery of Convex Relaxations via Dual Agents [56.60366723277675]
すべての許容関数に対して下界が成り立ち、より強い境界を与える凸緩和から従うことを示す。
理論は各エージェントを検証し、反例を検索し、報告されたすべての境界はインターバルにおける明示的な二重実現可能な点によって認証される。
論文 参考訳（メタデータ） (2026-06-30T06:10:25Z) - Why Do Few-Step Text Latents Fail When Image Latents Work? Non-Commitment at Sharp Categorical Readouts [1.1760370831826417]
滑らかで規則性に制限された決定論的写像は、シャープなカテゴリーの読み出しの前に離散的な分岐選択を解決できないことを示す。
実テキストオートエンコーダの重なり合う状態において、後平均終端ステップが決定境界の周囲に$O(s(t)$チューブで潜在質量の速度でトークンを反転させることを示す。
論文 参考訳（メタデータ） (2026-06-29T14:20:57Z) - Auditing Combinatorial Randomness from Finite Transcripts [0.2864713389096699]
我々は、$m$ラベルから$k$-subsetのブラックボックス監査を、正確にuniform-with-out-replacement nullの下で研究する。
構造的欠陥に対しては, 境界型チ二乗, ペア最大値, シリアルオーバーラップ, アンカードボックスパルション, 低次元差分を用いて, ハイパープレックス上でのNull-Agnostic auditsを構築する。
観測および基準ソース監査全体において、偽発見訂正後の統計は有意なものではない。
論文 参考訳（メタデータ） (2026-06-20T13:17:44Z) - Adaptive Consensus in LLM Ensembles via Sequential Evidence Accumulation: Automatic Budget Identification and Calibrated Commit Signals [0.0]
DASEは、ベンチマークをまたいで一般化するコミット型ルーティングパーティションを生成する。
インジェクション帯域ではなく、適応的な停止が正確さを駆動する。
インジェクションベースの手法は、逆Uの精度-vs-推論軌道を示す。
論文 参考訳（メタデータ） (2026-05-05T19:24:10Z) - A Closed-Form Persistence-Landmark Pipeline for Certified Point-Cloud and Graph Classification [0.0]
PLACE(Persistence-Landmark Analytic Classification Engine)は、点雲とグラフを分類するためのクローズドフォームパイプラインである。
3つの量的保証 -- マージンベースの過剰リスク率、クローズドフォーム記述子選択ルール、プレディションごとの証明書 -- は、トレーニングラベルのみから導かれる。
論文 参考訳（メタデータ） (2026-05-04T17:15:01Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳（メタデータ） (2026-04-20T13:25:40Z) - Criterion-referenceability determines LLM-as-a-judge validity across physics assessment formats [0.01116979912801043]
我々は、GPT-5.2、Grok 4.1、Claude Opus 4.5、DeepSeek-V3.2、Gemini Pro 3、および盲目、解答、偽解、そして模範的な条件下でのヒトマーカーに対する委員会集計を比較した。
n=771ドルのブラインド大学試験の質問に対して、モデルは差別的妥当性の強い分数平均絶対誤差(fMAE)$approx 0.22$を達成する。
$n=55$スクリプト全体において、盲目のAIマーキングは人間のマーキングよりも厳格で可変的であり、差別的妥当性はすでに貧弱である。
論文 参考訳（メタデータ） (2026-03-16T02:09:06Z) - Sample Smart, Not Hard: Correctness-First Decoding for Better Reasoning in LLMs [72.82403830490084]
我々は、復号規則は正確さによって校正されるべきであり、自信だけではならないと論じている。
Greedy-Threshold はこの目標を達成するための単純な戦略を提案します。
この結果から,不確実性の下での復号化が問題視され,数学や一般推論のベンチマークで有意な差がみられた。
論文 参考訳（メタデータ） (2025-10-07T14:46:12Z) - Large Language Monkeys: Scaling Inference Compute with Repeated Sampling [81.34900892130929]
モデルから候補解を繰り返しサンプリングする簡単な手法を用いて、推論計算をスケーリングのための別の軸として検討する。
複数のタスクやモデルにまたがって、カバレッジは4桁以上のサンプル数でスケールする。
コードや形式的証明のようなドメインでは、回答が自動的に検証されるので、カバレッジの増加は直接的にパフォーマンスの向上につながります。
論文 参考訳（メタデータ） (2024-07-31T17:57:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。