Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables

• URL: http://arxiv.org/abs/2511.16637v1
• Date: Thu, 20 Nov 2025 18:43:05 GMT
• Title: Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables
• 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 summary: Most successful approach to deal with bugs is to make solvers certify, so that they output a mathematical proof of correctness in a standard format.<n>This requires justifying symmetry reasoning within the proof, but developing efficient methods for this has remained a long-standing open challenge.<n>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.
• Score: 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.

Related papers

• Online Learnability of Chain-of-Thought Verifiers: Soundness and Completeness Trade-offs [34.168578803480116]
  We propose an online learning framework for learning chain-of-thought verifiers.<n>We show how our learned verifiers can be used to boost the accuracy of a collection of weak provers.
  arXiv  Detail & Related papers  (2026-03-03T21:50:14Z)
• Orbitopal Fixing in SAT [0.688204255655161]
  We present a practical static symmetry breaking approach based on orbitopal fixing.<n>Our methods deliver consistent speedups on symmetry-rich benchmarks with negligible regressions elsewhere.
  arXiv  Detail & Related papers  (2026-01-23T16:01:48Z)
• HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs [32.234133057592935]
  Hermes is a tool-assisted agent that interleaves informal reasoning with verified proof steps in Lean systems.<n>We evaluate Hermes on four challenging mathematical reasoning benchmarks using LLMs of varying parameter scales.
  arXiv  Detail & Related papers  (2025-11-24T04:50:18Z)
• Verifying a Sparse Matrix Algorithm Using Symbolic Execution [51.56484100374058]
  We outline how symbolic execution can be used to write tests similar to traditional unit tests.<n>We provide stronger verification guarantees and apply this methodology to a sparse matrix algorithm.
  arXiv  Detail & Related papers  (2025-10-15T11:23:32Z)
• How Many Code and Test Cases Are Enough? Evaluating Test Cases Generation from a Binary-Matrix Perspective [51.30005925128432]
  evaluating test cases automatically generated by Large Language Models (LLMs) is a critical yet challenging task.<n>Existing benchmarks suffer from high computational costs, score inflation, and a bias towards trivial bugs over rare, critical faults.<n>We introduce a framework that formalizes benchmark construction as finding an optimal diagnostic basis in a binary code-test matrix.
  arXiv  Detail & Related papers  (2025-10-09T18:29:24Z)
• Broken Tokens? Your Language Model can Secretly Handle Non-Canonical Tokenizations [83.93566096400723]
  We find that instruction-tuned models retain up to 93.4% of their original performance when given a randomly sampled tokenization.<n>Character-level segmentation improves string manipulation and code understanding tasks by up to +14%.<n>Right-aligned digit grouping enhances large-number arithmetic by +33%.
  arXiv  Detail & Related papers  (2025-06-23T18:02:26Z)
• Think Before You Accept: Semantic Reflective Verification for Faster Speculative Decoding [48.52389201779425]
  Speculative decoding accelerates inference by generating multiple draft tokens using a lightweight model and verifying them in parallel.<n>Existing verification methods rely heavily on distributional consistency while overlooking semantic correctness.<n>We propose Reflective Verification, a training-free and semantics-aware approach that achieves a better trade-off between correctness and efficiency.
  arXiv  Detail & Related papers  (2025-05-24T10:26:27Z)
• Let's Verify Math Questions Step by Step [29.69769942300042]
  MathQ-Verify is a novel pipeline designed to rigorously filter ill-posed or under-specified math problems.<n>MathQ-Verify first performs format-level validation to remove redundant instructions.<n>It then formalizes each question, decomposes it into atomic conditions, and verifies them against mathematical definitions.
  arXiv  Detail & Related papers  (2025-05-20T04:07:29Z)
• Critical Thinking: Which Kinds of Complexity Govern Optimal Reasoning Length? [72.70486097967124]
  We formalize a framework using deterministic finite automata (DFAs)<n>We show that there exists an optimal amount of reasoning tokens such that the probability of producing a correct solution is maximized.<n>We then demonstrate an implication of these findings: being able to predict the optimal number of reasoning tokens for new problems and filtering out non-optimal length answers results in consistent accuracy improvements.
  arXiv  Detail & Related papers  (2025-04-02T17:45:58Z)
• How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization [1.4796543791607086]
  This paper proposes a novel branch-and-bound algorithm for finding the shortest resolution proofs. We show that this representation breaks all permutational symmetries, thereby improving upon the state-of-the-art symmetry-breaking. Our experiments suggest that the proofs from state-of-the-art solvers could be shortened by 30-60% on the instances from SAT Competition 2002 and by 25-50% on small synthetic formulas.
  arXiv  Detail & Related papers  (2024-11-12T17:31:35Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)
• GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
  We propose Guiding chain-of-thought ReAsoning with a CorrectnEss Discriminator (GRACE) to steer the decoding process towards producing correct reasoning steps. GRACE employs a discriminator trained with a contrastive loss over correct and incorrect steps, which is used during decoding to score next-step candidates.
  arXiv  Detail & Related papers  (2023-05-24T09:16:51Z)
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
  We develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. We apply our method to maximum clique solving and constraint as a proof of concept that the approach applies to a wider range of problems.
  arXiv  Detail & Related papers  (2022-03-23T08:45:35Z)
• E-detectors: a nonparametric framework for sequential change detection [86.15115654324488]
  We develop a fundamentally new and general framework for sequential change detection. Our procedures come with clean, nonasymptotic bounds on the average run length. We show how to design their mixtures in order to achieve both statistical and computational efficiency.
  arXiv  Detail & Related papers  (2022-03-07T17:25:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.