論文の概要: Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
- arxiv url: http://arxiv.org/abs/2610.02444v1
- Date: Thu, 01 Oct 2026 20:13:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-06 00:14:30.076238
- Title: Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
- Title（参考訳）: 擬似記号検証による反例生成--擬似ハルトと強化修復の場合
- Abstract要約: 我々は、決定論的なPython検証に対して、制約付き目撃放射として反例生成を行う。
我々は,4,707個の偽の学部代数と実解析予想のコーパスであるSymCEをそれぞれ,実行可能な検証器と組み合わせてリリースする。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.
- Abstract（参考訳）: 大規模な言語モデルは、しばしば定理を前方に解くが、密接に関連する偽の定理を解けない: 教師付き微調整が閉じず、活発に悪化するファルシフィケーションギャップ。
我々は,決定論的なPython検証者に対して制約付き証人放射として反例生成を行い,実行可能検証者と組み合わせて,4,707個の偽の学部生と実解析予想のコーパスであるSymphCEをリリースする。
検証は報酬関数としても機能し、SymCEをトレーニング環境にする。
反例のみのSFTは真理論認識を0.27から0.00に崩壊させ、RLVRは少ない結果のみの報酬でこれを修復し、ベースを0.66に越える。
崩壊は4つの種子とGemma-3-4Bに複製される。
スパースと密度の高い報酬は、統計的に区別できないドメイン内成功をもたらすが、保持されたキャリブレーションプローブの33ポイントはばらばらになる。
我々の4Bモデルは、評価された7Bオープンウェイト数学のスペシャリストよりも優れており、6つのフロンティア商用APIと競合し続けており、GSM8K、MATH-500、MMLU-college-mathへの転送は変わらない。
177の検証者決定の人間監査では、97.7%の精度がある。
コード、データ、検証モジュール、アノテーション:https://github.com/ce-rlvr/SymCE。
関連論文リスト
- AG-CoT: Verified Algorithmic Traces for LLM Program Synthesis on Clifford Circuits [39.938021660593975]
本稿では,量子誤り訂正に使用される安定化器状態を作成するクリフォード回路の言語モデル合成における問題点について検討する。
筆者らのフレームワークでは,各ターゲットはコンパクトな符号付き安定化器生成器として与えられ,正確な検証器が生成したOpenQASM回路をチェックする。
論文 参考訳（メタデータ） (2026-09-27T04:19:00Z) - Efficient Branch-and-Bound Testing and Verification of zkVMs [26.60003840008197]
完全自動検証およびバグ検出フレームワークであるZEBRAを提案する。
ZEBRAは、zkVM検証を標準トレース空間上の解集合濃度問題に還元する。
ZEBRAは11のゼロデイバグを発見した。
論文 参考訳（メタデータ） (2026-09-14T04:35:11Z) - IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。
提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。
IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
論文 参考訳（メタデータ） (2026-09-09T17:59:04Z) - Bilevel Coordinated Reflection: A Game-Theoretic Approach to Multi-Agent LLM Systems [40.47928908205563]
マルチエージェントLLMシステムは、一般的にオーケストレータを使用して、労働者のチームのためにタスクを分解し、テキストリフレクションによって改善する。
強い実証結果にもかかわらず、これらのシステムには調整、メモリ改善、外部検証の役割の統一的な説明が欠けている。
我々は,評価のための信頼ゲーティングと,断片的な静止環境に対する保証の再集計を行う。
実験では、これらのオブジェクトを環境条件付きメトリクスでインスタンス化し、予測調整法則とドリフト法則をテストする。
論文 参考訳（メタデータ） (2026-09-02T15:50:10Z) - MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
MemToCは、実行時ツールによるポストツール-リターン仲裁のベンチマークである。
MemToCは、542の質制御された事実質問から構築された6,504回の評価エピソードで構成されている。
オープンウェイトな7-9Bモデルでは、ツールが強く支配的なクローズドブックの回答を返す。
論文 参考訳（メタデータ） (2026-08-26T18:22:03Z) - Silent Failures in Quantized LLM Reasoning: A Taxonomy-Based Analysis of Hollow Convergence and Failure Mode Shifts [0.0]
学習後の量子化は,タスク精度が保存されている場合でも,大きな言語モデルがどのように推論するかを静かに変更できることを示す。
3つの量子化精度で5つの命令調整LDMから3万のチェーン・オブ・シント出力を分類する。
精度は精度で高いが,Hollow Convergence は NF4 で大きく依存的な変化を示す。
論文 参考訳（メタデータ） (2026-07-10T21:55:05Z) - DeFAb: A Verifiable Benchmark for Defeasible Abduction in Foundation Models [6.628401122676601]
ルールベースの論理解法は、ベンチマークの全インスタンスを50マイクロ秒未満で100%精度で解決する。
データセットと生成パイプラインであるDeFAb(Defeasible Abduction Benchmark)を紹介します。
論文 参考訳（メタデータ） (2026-06-17T00:13:40Z) - Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。
個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。
構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
論文 参考訳（メタデータ） (2026-05-15T17:08:27Z) - Teaching LLMs Program Semantics via Symbolic Execution Traces [0.7046782561282057]
SV-COMP 2025上に構築された500 C 検証タスクの評価フレームワークを提案する。
6家族の14モデルを評価し,総合的精度の高いマスクが致命的な弱点であることを確認した。
わずか$sim$3,000のバグトレースと、推論時の連鎖推論を組み合わせることで、違反検出を17ポイント以上改善する。
論文 参考訳（メタデータ） (2026-05-07T13:01:06Z) - CARE What Fails: Contrastive Anchored-REflection for Verifiable Multimodal [84.71254539482369]
検証可能な報酬を伴うグループ相対的強化学習(RLVR)は、しばしば、すでに失敗している最も情報に富むデータを浪費する。
エラーを監督するマルチモーダル推論のための,障害中心のポストトレーニングフレームワークであるCAREを提案する。
CAREは正確さを改善し、スムーズさをトレーニングすると同時に、障害からの学習信号のシェアを明示的に増やします。
論文 参考訳（メタデータ） (2025-12-22T16:34:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。