Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.29145

ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization

Rui Zhang·Chenyu Zhou·Jianghao Lin·Yaoxin Wu·Dongdong Ge·Wen Song
View original source ↗Read source document ↗Export metadata ↓

Abstract

Large language models increasingly automate optimization modeling from natural language problems, producing written mathematics, solver code and a returned report. Verifying one optimization problem across these artifacts requires semantic comparison: unequal models can attain the same objective, equivalent models can use different auxiliary variables, and mutually consistent artifacts can omit the same source requirement. ORSMT provides a typed semantic interface and exact SMT relation queries. It aligns observable decisions, projects auxiliary variables, proves or refutes feasible region and objective relations, localizes refutations to implicated rows or domains and links source texts when available. It then reconstructs one artifact from another, and each adopted candidate passes the required relation checks. Across 3,034 problems and six generator sizes, ORSMT improves the model-code match rate in all 72 benchmark and generator combinations before selection. Protected selection raises the aggregate rate from 43.2% to 88.2% and the share that are both correct and matched from 25.2% to 40.2%. On the 1,905 refuted outputs, certified voting under the shared fallback makes 50.9% of outputs correct and matched, compared with 44.8% for ReLoop and 49.4% for Opt-Verifier. A separate one-round source revision followed by exact reconstruction restores a model-code match for 84.4% of the refuted pairs.

Explore related subjects

math.OCcs.AIcs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Rui Zhang, Chenyu Zhou, Jianghao Lin, Yaoxin Wu, Dongdong Ge, Wen Song. 2026-10-21. ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization. https://arxiv.org/abs/2610.29145

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Common Noise by Random Measures: Constructing Mean-Field Equilibria for Competitive Investment and Hedging

We construct Nash equilibria in mean-field portfolio games of optimal investment and hedging under relative performance concerns with exponential (CARA) utility preferences. Common noise dynamics are modeled by integer-valued random measures, for instance Poisson random measures, in addition to Brownian motions. Agents differ in individual risk aversions, competition weights, and initial capital endowments, while their contingent claim liabilities depend on both common and idiosyncratic risk factors. Mean-field equilibria are characterized by solutions to McKean-Vlasov backward stochastic differential equations with jumps, for which we prove existence and uniqueness of solutions, without assuming mean-field interaction to be small. Moreover, we show how the equilibrium can be constructed from the optimal strategy of a single-agent optimization problem (without mean-field interaction) via an appropriate projection. Using successive changes of measure, our derivation provides a decomposition of the equilibrium strategy into three components with clear interpretations. Finally, we show how a limiting mean-field game of quadratic (instead of utility-based) hedging with relative performance concerns arises for vanishing risk aversion.

math.OC↗
arXiv2026

Riemannian EXTRA: Communication-efficient decentralized optimization over compact submanifolds with data heterogeneity

We consider decentralized optimization over a compact Riemannian submanifold in a network of $n$ nodes, where each node $i$ owns a smooth nonconvex local objective $f_i$ defined by its private data, and the goal is to minimize the global objective $F(x)=\frac{1}{n}\sum_{i=1}^n f_i(x)$ using only local communications. A naive Riemannian extension of EXTRA leaves the auxiliary normal-space error uncontrolled and does not inherit the Euclidean convergence guarantees. We develop projection-based Riemannian EXTRA (REXTRA) and a retraction-based counterpart that incorporate a normal correction into both the communicated variable and the auxiliary update, while using only one local-variable-sized message per optimization iteration. By jointly controlling consensus, tangent, and normal errors, our analysis interprets the update as a network-based Riemannian inexact-gradient step. For projection-based REXTRA, a sufficiently small constant stepsize and a local initialization yield vanishing consensus, stationary accumulation points, and an $\mathcal O(1/k)$ best-iterate stationarity--consensus bound. For the retraction-based method, we prove that its difference from the projection update is uniformly second order and establish the same convergence properties and rate under a local initialization. Numerical experiments on representative manifold-valued learning tasks demonstrate the communication efficiency of the REXTRA updates.

math.OC↗
arXiv2026

Quantification of Tail-trimming Effects for Interval CVaR Based Nonlinear Regression

The tail trimming strategy is widely adopted for robustness against outlier contamination in statistical learning and operations research. However, it generally lacks the thorough understanding that to what extent the tail-trimming technique is effective for nonlinear regression. In this paper, we address the robust nonlinear regression based on the so-called interval conditional value-at-risk (In-CVaR), which is introduced to guard against outliers by trimming extreme losses. We first analyze the trimming effect of the In-CVaR based estimator under distributional perturbation. Our first finding is that the In-CVaR based estimator is qualitatively robust under distributional perturbation in terms of the Prokhorov metric if and only if the largest portion of losses is trimmed. Furthermore, under sample contamination, we derive a probably approximately correct (PAC) bound for the In-CVaR based estimator, showing that the preliminary covariate filtering that is customary in the literature is not needed for In-CVaR based regression. The nonconvexity of the In-CVaR objective, together with unboundedness of covariates, responses and parameter space create the technical challenges for our developed theory, and thus necessitate the new treatment of the qualitative robustness and PAC analysis. Overall, this study rigorously analyzes robustness properties of In-CVaR based nonlinear regression models, which illustrates to what extent the right tail-trimming of the loss by In-CVaR risk measure is essential and effective for robust nonlinear regression. These theoretical findings are further supported by numerical experiments.

math.OC↗