論文の概要: The Refutation Gap: Certifying Both Halves of an Optimality Claim

• arxiv url: http://arxiv.org/abs/2609.20873v1
• Date: Wed, 16 Sep 2026 06:01:22 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-21 18:40:16.728894
• Title: The Refutation Gap: Certifying Both Halves of an Optimality Claim
• Title（参考訳）: The Refutation Gap: 最適なクレームの両半分を認証する
• Abstract要約: 組合せ最適化はこの非対称性を何十年にもわたって認識しており、主にこの問題に対処してきた。 しかし、最小のXOR回路に対して発行されたゲートカウントは、クレームの半分の証明書を提供しない。 我々は、GF(2)上の最小線形直線プログラムを合成するパイプラインでギャップを埋める。そこでは、決定的なUNSAT応答が独立のサードパーティチェッカーによってチェックされたDRAT証明を出力する。
• 参考スコア（独自算出の注目度）: 1.7273335171181035
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The upper bound, "a program of size m exists", is witnessed by an artifact that can be re-executed, proved equivalent to its specification, and shipped with a machine-checked certificate. The lower bound, "no program of size m-1 exists", has no witness and is discharged by running a solver until it reports UNSAT. Combinatorial optimization has known this asymmetry for decades and has largely addressed it: certifying algorithms make it explicit (McConnell et al., 2011), and pseudo-Boolean proof logging can certify optimality end to end with a formally verified checker (Bogaerts et al., 2023; Koops et al., 2025). That discipline has not reached circuit minimization. We call this the refutation gap: published gate counts for minimal XOR circuits provide no certificate for either half of the claim, and neither did 121 optimality results we ourselves produced. We close the gap with a pipeline that synthesizes minimal linear straight-line programs over GF(2), where every decisive UNSAT answer emits a DRAT proof checked by an independent third-party checker. We certify all 121 optimality results established by the project, across n = 6 to 9: 111 carry independently verified refutations, 10 are closed by a free counting bound, and none disagrees with the uncertified value. The median proof is 1.1 MB and checking costs 1.9x solving. We give five case studies where verification caught defects that code review did not, report two interface obstacles that push practitioners toward the uncertified path, and describe an adversarial audit that revealed a failure tail we were about to attribute to the problem was actually caused by our own budget.
• Abstract（参考訳）: 合成パイプラインは、プログラムが正しいだけでなく、最適であると主張する。 このような主張には、根本的に異なる検証ストーリーを持つ2つのハーフがある。 上界の「サイズ m のプログラム」は、再実行可能で、その仕様と同等であることが証明され、マシンチェックされた証明書と共に出荷されるアーティファクトによって目撃される。 サイズ m-1 のプログラムは存在しない」という下界には目撃者がおらず、UNSATを報告するまで解決器を走らせることで退避する。 証明アルゴリズムは明示する(McConnell et al , 2011)し、疑似ブール証明ロギングは、正式に証明されたチェッカー(Bogaerts et al , 2023; Koops et al , 2025)で最適性を終端まで証明することができる。 その規律は回路の最小化に達していない。 最小のXOR回路のゲートカウントは、クレームの半分の証明書を提供しておらず、私たち自身が作成した121の最適性結果も提供していません。 我々は、GF(2)上の最小線形直線プログラムを合成するパイプラインでギャップを埋める。そこでは、決定的なUNSAT応答が独立のサードパーティチェッカーによってチェックされたDRAT証明を出力する。 我々は、n = 6 から 9: 111 にまたがって、n = 6 から 9: 111 にまたがる全ての 121 最適性の結果を認定する。 中央値の証明は1.1MBであり、チェックコストは1.9倍である。 コードレビューが行わなかった欠陥を検証した5つのケーススタディ、未確認のパスに向かって実践者をプッシュする2つのインターフェース障害を報告し、問題の原因となった障害の尾が実際に当社の予算によって引き起こされたことを明らかにする敵対的な監査について説明した。

関連論文リスト

• Proof-Carrying Cognition: Closing the Verification Gap with Reality-Settled Reward [0.0]
  言語モデル推論のフロンティアゲインは、推論トレースに関する強化学習によって得られる。 我々は、フィールドの束縛制約が検証ギャップであると主張する。
  論文  参考訳（メタデータ） (2026-09-09T06:24:53Z)
• PRIMUS: Identity, Governance, and Verification for Multi-Agent Federations [0.0]
  マルチエージェント・フェデレーションは、敵対的な条件下での3つの質問に答えるガバナンスを必要とする。 本稿では,BLSアグリゲートシグネチャと主パワーIDを結合したPRIMUSについて述べる。 PRIMAのバイナリアーティファクト-忠実性判定は、グレード付きフィットネス信号に変換できるかどうかを問う。
  論文  参考訳（メタデータ） (2026-09-07T19:21:49Z)
• A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver [3.8048003898069975]
  SAIR Mathematics Distillation Challenge on Equational Theories では、あるマグマが別のマグマの同一性を意味するかどうかを解き明かす。 我々は,最も安価な第1カスケードとして構成された単一ファイル解決器を提案する。 その偽分岐は、構造化代数族上の係数テスト、有界有限モデル探索、明示的な中心群群証人、およびいくつかの無限キャリア証人を組み合わせたものである。
  論文  参考訳（メタデータ） (2026-09-01T04:34:00Z)
• The geometry of AI validation: Exact certification limits for iid best-of-N search [0.0]
  信頼性面上での検証とデプロイメントのルールをカーネルとして表現する。 B_m,N=1+2sum_r=1m(-1)rcos2Nr/[(m+1)]$
  論文  参考訳（メタデータ） (2026-08-21T15:18:11Z)
• Judging Is Not Enumerating: Silent Omissions in LLM-Authored Acceptable Sets [13.85834524293015]
  私たちは、ロールが想定する能力を測定し、通常、ロールが配置されるプロトコルの下でそれを欠いていることを見つけます。 モデルは、その候補がセット自体の作者よりもはるかに優れているかどうかを判断する。
  論文  参考訳（メタデータ） (2026-08-02T05:00:44Z)
• AI-Assisted Discovery of Convex Relaxations via Dual Agents [56.60366723277675]
  すべての許容関数に対して下界が成り立ち、より強い境界を与える凸緩和から従うことを示す。 理論は各エージェントを検証し、反例を検索し、報告されたすべての境界はインターバルにおける明示的な二重実現可能な点によって認証される。
  論文  参考訳（メタデータ） (2026-06-30T06:10:25Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。 本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
  論文  参考訳（メタデータ） (2022-08-11T10:31:28Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)

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

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