論文の概要: Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

• arxiv url: http://arxiv.org/abs/2511.16637v1
• Date: Thu, 20 Nov 2025 18:43:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-21 17:08:52.791492
• Title: Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
• Title（参考訳）: 補助変数付き順序を用いたより高速な認証対称性の破れ
• Authors: Markus Anders, Bart Bogaerts, Benjamin Bogø, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan,
• Abstract要約: バグに対処する最も成功したアプローチは、標準フォーマットで正確性の数学的証明を出力するように、ソルバを認証することである。 これは証明の中で対称性の推論を正当化する必要があるが、このための効率的な方法の開発は長年のオープン・チャレンジのままである。 証明ロギングの実験を行い,SAT対称性の破れをチェックすることによって,理論と実践の両面でのオーダー・オブ・マグニチュード・スピードアップにつながることを示す。
• 参考スコア（独自算出の注目度）: 11.274339621648565
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Symmetry breaking is a crucial technique in modern combinatorial solving, but it is difficult to be sure it is implemented correctly. The most successful approach to deal with bugs is to make solvers certifying, so that they output not just a solution, but also a mathematical proof of correctness in a standard format, which can then be checked by a formally verified checker. This requires justifying symmetry reasoning within the proof, but developing efficient methods for this has remained a long-standing open challenge. A fully general approach was recently proposed by Bogaerts et al. (2023), but it relies on encoding lexicographic orders with big integers, which quickly becomes infeasible for large symmetries. In this work, we develop a method for instead encoding orders with auxiliary variables. We show that this leads to orders-of-magnitude speed-ups in both theory and practice by running experiments on proof logging and checking for SAT symmetry breaking using the state-of-the-art satsuma symmetry breaker and the VeriPB proof checking toolchain.
• Abstract（参考訳）: 対称性の破れは現代の組合せ解法において重要な技法であるが、正しく実装されているかどうかを確認することは困難である。 バグに対処する最も成功したアプローチは、解法を認証することであり、解法だけでなく標準形式での正当性の数学的証明も出力する。 これは証明の中で対称性の推論を正当化する必要があるが、このための効率的な方法の開発は長年のオープン・チャレンジのままである。 完全に一般的なアプローチは、Bogaerts et al (2023) によって最近提案されたが、大きな整数を持つ語彙順の符号化に依存しており、これはすぐに大きな対称性にとって不可能になる。 本研究では,代用変数で順序を符号化する手法を開発した。 このことは理論と実践の両方において、証明ロギングの実験と、最先端のサスマ対称性ブレーカとVeriPB証明チェックツールチェーンを用いてSAT対称性ブレーカのチェックを行うことによって、オーダー・オブ・マグニチュード・スピードアップにつながることを示す。

関連論文リスト

• Think Before You Accept: Semantic Reflective Verification for Faster Speculative Decoding [48.52389201779425]
  投機的復号化は、軽量モデルを使用して複数のドラフトトークンを生成し、それらを並列に検証することで推論を加速する。 既存の検証手法は、意味的正確性を見越しながら、分布の整合性に大きく依存している。 我々は,学習自由でセマンティックなアプローチであるリフレクティブ検証を提案し,正確性と効率のトレードオフを改善する。
  論文  参考訳（メタデータ） (2025-05-24T10:26:27Z)
• Let's Verify Math Questions Step by Step [29.69769942300042]
  MathQ-Verifyは、未定または未定の数学問題を厳格にフィルタリングするために設計された、新しいパイプラインである。 MathQ-Verifyはまず、冗長な命令を削除するためのフォーマットレベルのバリデーションを実行する。 その後、各質問を形式化し、それを原子状態に分解し、数学的定義に対して検証する。
  論文  参考訳（メタデータ） (2025-05-20T04:07:29Z)
• How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
  本稿では,最短解法を見つけるための分岐結合アルゴリズムを提案する。 この表現はすべての置換対称性を破り、それによって最先端の対称性の破れを改善する。 本実験により, SATコンペティション2002の事例では30～60%, 小型合成式では25～50%の短縮が可能であることが示唆された。
  論文  参考訳（メタデータ） (2024-11-12T17:31:35Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
  本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。 GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
  論文  参考訳（メタデータ） (2023-05-24T09:16:51Z)
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
  本研究では,対称性と支配的破壊が容易に表現可能な最適化問題に対する認証手法を開発した。 提案手法は,提案手法が幅広い問題に適用可能であることを示す概念実証として,最大斜め解法と制約法に適用する。
  論文  参考訳（メタデータ） (2022-03-23T08:45:35Z)
• E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
  逐次的変化検出のための基本的かつ汎用的なフレームワークを開発する。 私たちの手順は、平均走行距離のクリーンで無症状な境界が伴います。 統計的および計算効率の両方を達成するために,これらの混合物を設計する方法を示す。
  論文  参考訳（メタデータ） (2022-03-07T17:25:02Z)

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

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