SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

• URL: http://arxiv.org/abs/2609.00728v1
• Date: Tue, 01 Sep 2026 05:05:12 GMT
• Title: SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
• Abstract summary: We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification.<n>We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs.
• Score: 2.6426981014417046
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective-order preservation for mixed-integer linear formulations, while dReal provides tolerance-aware feasibility/range and $ε$-argmin checks for continuous nonlinear formulations. We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.

Related papers

• FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving [15.609601435289973]
  We develop a constructive definition of MILP reformulation that can be formalized in Lean and machine-checked.<n>To evaluate our approach, we introduce FormulationBench, a dataset of 20 problems and 109 formulations.<n>FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench.
  arXiv  Detail & Related papers  (2026-08-25T23:19:41Z)
• FormuEvo: LLM-Guided Evolution for Discovering Solver-Efficient Mixed-Integer Programming Formulations [66.32852384262038]
  Mixed-integer programming (MIP) lies at the core of operations research and industrial optimization.<n>We propose FormuEvo, an evolutionary framework for automated discovery of solver-efficient MIP formulations.<n>FormuEvo frames MIP formulation design as evolutionary optimization over the symbolic space of MIP formulations.
  arXiv  Detail & Related papers  (2026-08-24T15:01:28Z)
• CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
  CktFormalizer is a framework that redirects hardware generation through a dependently-typed HDL embedded in Lean 4.<n>On VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems), CktFormalizer achieves simulation pass rates competitive with direct Verilog generation.
  arXiv  Detail & Related papers  (2026-05-08T14:20:06Z)
• LIMSSR: LLM-Driven Sequence-to-Score Reasoning under Training-Time Incomplete Multimodal Observations [53.20772659095155]
  This paper tackles the more challenging setting of IML under training-time incomplete observations.<n>We propose LIMSSR (LLM-Driven Incomplete Multimodal Sequence-to-Score Reasoning), a framework that reformulates this challenge as a conditional sequence reasoning task.
  arXiv  Detail & Related papers  (2026-05-01T06:11:42Z)
• OpenSanctions Pairs: Large-Scale Entity Matching with LLMs [0.9131359219276399]
  We release OpenSanctions Pairs, a large-scale entity matching benchmark derived from real-world international sanctions aggregation and analyst deduplication.<n>The dataset contains 755,540 labeled pairs spanning 293 heterogeneous sources across 31 countries.<n>Off-the-shelf LLMs substantially outperform the production rule-based baseline.
  arXiv  Detail & Related papers  (2026-02-24T06:25:49Z)
• ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
  Large language models (LLMs) can translate natural language into optimization code, but silent failures pose a critical risk.<n>We introduce ReLoop, addressing silent failures from two complementary directions.
  arXiv  Detail & Related papers  (2026-02-17T20:20:33Z)
• Constructing Industrial-Scale Optimization Modeling Benchmark [26.61380804019141]
  A key bottleneck is the lack of benchmarks that align natural-language specifications with reference formulations/solver code grounded in real optimization models.<n>We introduce MIPLIB-NL, built via a structure-aware reverse construction methodology from real mixed-integer linear programs.<n>Experiments show substantial performance degradation on MIPLIB-NL for systems that perform strongly on existing benchmarks.
  arXiv  Detail & Related papers  (2026-02-11T02:45:31Z)
• From Abstract to Contextual: What LLMs Still Cannot Do in Mathematics [79.81905350372067]
  We study gap through contextual mathematical reasoning.<n>We introduce ContextMATH, a benchmark that repurposes AIME and MATH-500 problems into two contextual settings.<n>Open-source models decline by 13 and 34 points on SG and CS, while proprietary models drop by 13 and 20.
  arXiv  Detail & Related papers  (2026-01-30T14:56:04Z)
• The Hidden Cost of Approximation in Online Mirror Descent [56.99972253009168]
  Online mirror descent (OMD) is a fundamental algorithmic paradigm that underlies many algorithms in optimization, machine learning and sequential decision-making.<n>In this work we initiate a systematic study into inexact OMD, and uncover an intricate relation between regularizer smoothness and robustness to approximation errors.
  arXiv  Detail & Related papers  (2025-11-27T10:09:07Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• High Accuracy, Less Talk (HALT): Reliable LLMs through Capability-Aligned Finetuning [84.52940628494879]
  Large Language Models (LLMs) currently respond to every prompt.<n>LLMs can produce incorrect answers when they lack knowledge or capability.<n>We propose post-training an LLM to generate content only when confident in its correctness and to otherwise abstain.
  arXiv  Detail & Related papers  (2025-06-04T15:16:21Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  In large language models (LLMs), identifying sources of uncertainty is an important step toward improving reliability, trustworthiness, and interpretability. In this paper, we introduce an uncertainty decomposition framework for LLMs, called input clarification ensembling. Our approach generates a set of clarifications for the input, feeds them into an LLM, and ensembles the corresponding predictions.
  arXiv  Detail & Related papers  (2023-11-15T05:58:35Z)

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.