PaperlayerView exact revision on arXiv

Source-linked AI summary

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

arXiv:2610.29145v1math.OCcs.AIcs.SE

TL;DR

Evaluating an optimization answer alone cannot establish that its source requirements, written mathematics, solver code, and report describe the same problem. ORSMT uses exact SMT checks to verify those relations and guide reconstruction or revision. Across the reported benchmarks, it improves model–code matching, with protected selection raising aggregate match from 43.2% to 88.2%.

  • Problem

    Answer correctness and objective values do not establish agreement among optimization artifacts, and artifacts can agree while omitting a source requirement.

    Source: §1 · p. 1

  • Method

    ORSMT aligns observable decisions in a common exact representation, checks artifact relations with SMT, and uses counterexamples to guide reconstruction or revision before rechecking candidates.

    Source: §1 · p. 2

  • Results

    Model–code match rates improve in all 72 benchmark–generator combinations; protected selection raises aggregate match from 43.2% to 88.2%.

    Source: §1 · p. 2

  • Takeaways & Limitations

    ORSMT provides a modular verification and repair layer that improves correct-and-matched outputs when integrated with OptiMUS-0.3 and OptiMind.

    Source: §1 · p. 2

    Certificates are SMT-backed verdicts for encoded relations, not independently checked proof objects, and depend on translation, runtime capture, correspondence, source compilation, and the SMT backend.

    Source: §4.4 · p. 8

Abstract

from arXiv · show

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.

1. Introduction

ORSMT addresses the gap between checking an optimization answer and verifying that source requirements, mathematics, solver code, and reports describe the same problem. It uses exact SMT checks to guide reconstruction or revision, and improves model–code matching across the reported evaluations.

1. Introduction

  • A correct objective value does not establish that the implemented problem is right: different feasible regions can share an optimum, and equivalent models can use different auxiliary variables or constraints.Mathematics and code can also agree while both omit a natural-language requirement.Source: §1 · pp. 1–2
  • Behavioral tests and structural comparisons can miss semantic mismatches or reject equivalent models, motivating checks of feasible decisions, objective preferences, and source requirements.The introduction also identifies discrepancy localization and rechecking proposed repairs as necessary.Source: §1 · p. 2
  • ORSMT represents artifacts in a common exact form and uses SMT queries to certify or refute their relations, returning localized counterexamples that support reconstruction or revision.Every adopted candidate passes the required relation checks again.Source: §1 · p. 2
  • The framework is introduced as semantic verification across source requirements, mathematical formulations, solver code, and returned reports, with exact checks within an admitted affine rational core.Its decided relations receive certificates or localized counterexamples.Source: §1 · p. 2
  • The repair loop combines bidirectional reconstruction with counterexample-guided revision, then checks each candidate before adoption.Diagnosis, repair, and acceptance use the same verifier.Source: §1 · p. 2
  • Model–code match rates improve in all 72 benchmark–generator combinations; protected selection raises aggregate match from 43.2% to 88.2% and correct-and-matched outputs from 25.2% to 40.2%.ORSMT also improves correct-and-matched outputs when integrated with OptiMUS-0.3 and OptiMind.Source: §1 · p. 2

2. Related Work

Prior work develops optimization formulation and evaluation, broader feedback and repair, and formal semantic verification. The paper distinguishes ORSMT by checking whether source requirements, written models, executable models, and reports describe the same optimization problem.

2. Related Work

  • Formulation and pipeline work includes NL4Opt [Ramamonjison et al., 2022], OptiMUS and OptiMUS-0.3 [AhmadiTeshnizi et al., 2024b,a], and OptiMind [Zhang et al., 2025]; evaluation suites broaden the tasks studied.ORLM, LLMOPT, and ORThought generate or revise models, code, and solver outputs [Huang et al., 2025a; Jiang et al., 2025; Yang et al., 2026], while MAMO, OptiBench, and OPT Engine broaden evaluation [Huang et al., 2025b; Yang et al., 2025; Chen et al., 2026].Source: §2 · p. 2
  • Behavioral tests, structural judgments, semantic anchors, and solver-based testing provide repair signals, but ORSMT instead repairs instance-specific mathematical, executable, and report artifacts.The paper uses ReLoop and Opt-Verifier as repair comparisons.Source: §2 · p. 3
  • Formal methods range from denotational tests and arithmetic solvers to neural-symbolic query translation; ORSMT checks source requirements, feasible regions, objective preferences, and reports.Its evidence identifies missing, additional, and redundant restrictions and supports repair from either usable model.Source: §2 · p. 3

3. Problem Setting

The problem setting treats an autoformulation pipeline as producing written mathematics, an executable solver model, and a report from a source statement and instance data. ORSMT checks available relations among these artifacts and any formalized source requirements.

3. Problem Setting

  • An autoformulation pipeline maps a source statement and instance data to written mathematics, a solver program, and a report containing the returned solution, objective value, and status.The written formulation is lowered to model A, while the instantiated solver model is represented as B.Source: §3 · p. 3
  • A model comprises observable decisions, auxiliary variables, domains and constraints, an objective, and a minimization or maximization direction.A fixed correspondence aligns observable decisions; comparison projects out auxiliary variables.Source: §3 · p. 3
  • Semantic agreement preserves projected feasible decisions and their preference order, while absolute objective values are checked separately.Source satisfaction and report validity are also checked, with instance parameters substituted before comparison and existential completion for partial reports.Source: §3 · p. 3
  • The task is to return matched artifacts and evidence for required relations; either model can supply a missing representation, while a source counterexample can expose an omission shared by both.Each decided relation is certified or accompanied by a concrete refuting assignment.Source: §3 · p. 3

4. ORSMT: Verification, Repair and Matching

ORSMT translates artifacts into a common representation, checks their semantic relations, diagnoses refutations, and reconstructs or revises artifacts. Its selection policies adopt only candidates that pass the checks required by the active policy.

4. ORSMT: Verification, Repair and Matching

  • ORSMT translates mathematical and executable models into a common exact representation, checks their relations, and reapplies the same checks to repaired candidates before adoption.Figure 1 depicts source requirements, mathematics, solver code, and reports entering a shared representation, with SMT checks supporting reconstruction or revision.Source: §4 · p. 4, Figure 1 · p. 4
  • ORSMT supports affine models with rational coefficients over real, integer, and Boolean variables; certificates depend on translation, capture, correspondence, source compilation, and the SMT backend.Unsupported translation, ambiguous correspondence, timeout, or solver unknown yields an undecided result; certificates are not independently checked proof objects.Source: §4 · p. 4, §4.4 · p. 8

4.1. Model representation and bidirectional construction

  • Observable decisions are aligned by a one-to-one correspondence, while auxiliary variables are projected out so equivalent models need not match every solver variable.A contradiction, type mismatch, or unmatched observable decision leaves correspondence undecided; reconstruction can proceed from either the mathematical or executable model after normalization.Source: §4.1 · pp. 4–5
  • ORSMT can compile solver code from mathematics or export a captured executable model into mathematics, then compile, capture, and verify the resulting artifacts.The construction guarantee depends on normalization preserving projected semantics and faithful capture of the compiled model.Source: §4.1 · p. 5

4.2. Verification queries and diagnosis

  • SMT queries compare feasible regions and objective preferences; witnesses identify excluded decisions or preference conflicts, while unsatisfiable queries certify the tested relations.Row-level tests identify missing, additional, or redundant restrictions; source contracts can expose a requirement omitted by both equivalent artifacts.Source: §4.2 · pp. 5–6

4.3. Certificates and scalable exactness

  • Certificates cover encoded relations, and scalable checking uses sound query reduction and exact component slicing under their stated conditions.A reduced satisfiable query is reported as a counterexample only if its assignment extends to satisfy the full model while violating the obligation.Source: §4.3 · p. 7

4.4. Revision and Selection

  • Revision uses relation failures, counterexamples, implicated rows or domains, and linked source text; selection adopts only eligible candidates and otherwise retains the original artifacts.Certified voting requires at least two eligible candidates to agree on reported value, while protected selection preserves an available original finite result.Source: §4.4 · p. 7

5. Experiments

Across the full population, ORSMT leads all three reported outcomes; direct reconstruction improves model–code matching across every benchmark–generator combination. Controlled repairs and host integrations further assess match recovery and correct-and-matched outputs.

Checking efficiency

  • Automatic backend selection decides 94.6% of assigned problems under a ten-second limit, with a 0.647-second median.On FrontierOR, component slicing yields paired speedups of 29.3× and 27.8× for the reported row-size ranges.Source: §5 · pp. 8–9, Table 4 · p. 9

Direct reconstruction

  • Bidirectional reconstruction raises model–code matches from 7,867 to 15,724 without language model calls.It completes 6,590 programs from mathematics and 1,267 mathematical artifacts from programs; all 72 benchmark–generator cells improve, with a median gain of 47.2 percentage points.Source: §5 · p. 9, Table 5 · p. 10

Source revision

  • Source revision followed by exact reconstruction restores model–code matches for 1,607 refuted outputs (84.4%).The comparison gives every method the same refuted outputs and 14B reviser.Source: §5 · p. 9

Repair comparison

  • Certified voting makes 50.9% of outputs correct and matched, 6.1 points above ReLoop and 1.4 above Opt-Verifier.The comparison concerns the 1,905 refuted outputs.Source: §5 · p. 9, Table 7 · p. 10

Full-population outcomes

  • ORSMT leads all three reported outcomes in the full-population comparison.Table 6 reports outcomes over 3,034 problems and six generators.Source: §5 · p. 10, Table 6 · p. 10

Host integration

  • ORSMT adds 569 correct-and-matched outputs for OptiMUS-0.3 and 223 for OptiMind.OptiMind also gains 683 artifact matches, with gains chiefly improving agreement when host answers are already strong.Source: §5 · p. 10, Table 8 · p. 11

6. Conclusion

ORSMT closes the verification–repair loop with exact certificates, counterexamples, bidirectional reconstruction, and rechecking of adopted artifacts. Across the evaluated problems and generators, it improves model–code agreement and correct-and-matched outputs.

6. Conclusion

  • 43.2% to 88.2%: ORSMT raises aggregate model–code matches, while correct-and-matched outputs rise from 25.2% to 40.2%.These results cover 3,034 problems and six generator sizes (18,204 outputs).Source: §6 · p. 11
  • Among 1,905 refuted outputs, certified voting yields 50.9% correct-and-matched outputs, and source revision followed by reconstruction restores matches for 84.4% of refuted pairs.The analysis also finds code unavailable nearly twice as often as mathematics and more likely to add constraints than omit them.Source: §6 · p. 11

Contents of the Appendix

  • The appendix reports checking coverage, unresolved cases, error distributions, runtime, feedback quality, repair effects, and transfer to existing modeling systems.It also includes repair and source-review prompts, evaluation-criterion tests, and worked cases with exact witnesses.Source: Contents of the Appendix · pp. 14–15

A.1. Populations, metrics and scoring

The appendix fixes the experiment populations, representations, scoring rules, and formal procedures before reporting verification outcomes and unresolved cases. It specifies how artifacts and source requirements are represented and how relation checks support reconstruction and adoption.

A.1. Populations, metrics and scoring

  • The main experiment pairs twelve benchmarks with six Qwen2.5-Instruct generator sizes, retaining problem-level identifiers and grouping resampling by source problem.It scores correct answers, model–code matches, artifact matches, and correct-and-matched outputs; correctness uses a declared tolerance, and unavailable artifacts and failures remain in paired comparisons.Source: §A.1 · p. 15, Table 9 · p. 15

A.2. Artifact representations and capture

  • Accepted declarations encode real, integer, or Boolean variables, rational bounds, linear rows, and an objective; unsupported or malformed declarations produce typed translation failures.The historical panel uses real arithmetic symbols with integrality predicates for integer variables, while runtime capture records instantiated solver models and comparisons align variables by normalized names.Source: §A.2 · pp. 15–16
  • Source obligations retain supporting text, scope, variable roles, coefficients, relation, and applicability; admitted reference formulations check that contract rather than independently recovering author intent.Exact reconstruction compiles domains, rows, objective, and direction, projects added variables for comparison, and checks the reconstructed pair after redundancy deletion.Source: §A.2 · p. 16, §B.3 · p. 17

B. Formal Guarantees and Complete Procedures

  • Relation certificates use unsatisfiable difference queries to establish equality of projected feasible regions and strict preference relations, while satisfying queries return separating assignments or decision pairs.Source-obligation entailment, report checks, and optimality are likewise expressed as feasibility or violation queries.Source: §B.1 · p. 16

B.2. Constraint reduction and witness completion

  • Constraint reduction preserves soundness by making the full violation formula imply the reduced one, and exact component slicing is valid when omitted components share no variables with retained components or the obligation.Partial witnesses are extended and checked against the full model; the evidence record preserves assignments, violated rows, and the relation used for revision.Source: §B.2 · pp. 16–17

B.3. Reconstruction and adoption

  • Reconstruction compiles and captures normalized artifacts, then checks region inclusions and objective relations; sequential deletion preserves equivalence because each removed row is entailed by the retained rows.The adoption loop accepts only candidates whose required relation checks succeed and retains certified evidence when a later proposal fails.Source: §B.3 · p. 17

B.4. Construction and adoption procedures

  • The procedures select a readable mathematical artifact by default, construct its paired program and report, verify the result, and apply direct, certified-voting, or protected selection without changing candidate verification.Protected selection filters candidates by preservation requirements; if no record qualifies, the original state and evidence remain active.Source: §B.4 · p. 17, §C.1 · pp. 18–19

C.1. Checking coverage and unresolved cases

  • Checking coverage separates the first unsuccessful verification stage from potentially overlapping semantic findings, while redundant constraints are diagnosed separately by entailment.The reported tables distinguish artifact availability, discrepancies, and the full formal chain; Figure 2 covers outcomes and detected findings across generators.Source: §C.1 · p. 17, Table 10 · p. 19, Figure 2 · p. 19

C.3. Errors introduced during code generation

The appendix examines code-generation discrepancies, checking time, canonical requirements and redundancy, and larger-instance query behavior. It then frames the repair experiments around feedback quality, repair effects, and transfer.

C.3. Errors introduced during code generation

  • 32.9% of outputs have unavailable code versus 17.6% with unavailable written models; among 951 fully decided pairs, code adds restrictions in 546 and omits written restrictions in 415, with overlap.Redundancy appears only in code in 239 assignments and only in written models in 188; Table 15 defines reusable findings by checkable evidence.Source: §C.3 · p. 21, Table 15 · p. 21

C.4. Checking time on the controlled CPU panel

  • The complete audit decides 2,860 problems at a 0.397-second median, while automatic backend selection decides 2,869 at a 0.647-second median; both agree wherever both decide.Figure 3 compares checking time across benchmarks and constraint sizes, with unavailable models unresolved and timeouts included in medians.Source: §C.4 · p. 22, Figure 3 · p. 22

C.5. Canonical requirements and redundancy

  • Canonical requirements are checked through exact obligation queries, while row entailment supports sequential removal of redundant rows to produce a smaller equivalent basis.The tables cover 136,100 obligations in 1,806 models and 340,289 rows in 1,705 models, respectively.Source: §C.5 · p. 22, Table 18 · p. 23, Table 19 · p. 23

C.6. Constraint selection and larger instances

  • Full queries decide 658 larger-instance claims and agree with restricted queries on all 600 jointly decided claims; the largest models reach 5,768,230 rows and 3,302,127 variables.One 372,000-row model takes 283 seconds to encode and 108 seconds to establish an exact feasible base; a weakened row query takes 5,656 seconds in the complete solver versus 2.60 locally.Source: §C.6 · p. 24, Table 21 · p. 24
  • Independent Z3 and cvc5 encodings agree on all 110,366 query pairs decided by both, while at least one solver remains unresolved on 266,785 recorded pairs.The comparison records 377,151 of 377,280 assigned query pairs.Source: §C.6 · p. 24

D. Feedback Quality, Repair Effects and Transfer

  • The repair evaluation separates verifier feedback and returned evidence, repair under a shared data and budget setting, and effects on answers, matches, source requirements, and host integrations.Source: D. Feedback Quality, Repair Effects… · p. 24

D.1. Feedback coverage and error localization

The appendix compares verifier feedback, mechanical completion, language-model revision, candidate selection, and recorded repair costs. It also details how repair and source-review work is counted.

D.1. Feedback coverage and error localization

  • ORSMT provides certificates or separating assignments tied to rows, domains, or objective preferences; examples show ReLoop accepting unequal regions and Opt-Verifier rejecting a certified value using incorrect cost arithmetic.Feedback coverage is reported on 18,204 outputs, separating refuted from equivalent model–code pairs.Source: §D.1 · p. 25, Table 22 · p. 25

D.2. Direct reconstruction and completion routes

  • Mechanical completion reconstructs a program from a mathematical target or mathematics from a captured program, without language-model calls.Tables report completion routes across 18,204 outputs and outcomes for 10,337 initially uncertified outputs.Source: §D.2 · p. 25, Table 24 · p. 26, Table 25 · p. 26

D.3. LLM feedback, ablations and paired repair

  • Protected selection retains finite original results and reconstructs paired artifacts around them, while outputs without finite values receive value-changing revision; five-candidate voting groups certified finite values by exact equality.The fixed reviser receives the problem statement and evidence for its repair condition.Source: §D.3 · p. 27

D.3.1. Prompts used for language model revision

  • A one-round source revision followed by exact reconstruction is evaluated on the same 1,905 refuted outputs, using returned model–code matches as the comparison outcome.The comparison uses a shared 14B reviser.Source: §D.3.1 · p. 28, Table 26 · p. 28
  • The interval is above zero against ReLoop and overlaps zero against Opt-Verifier; the comparison distinguishes mechanical completion, verifier-feedback revision, and multi-candidate selection.Source: §D.3.1 · p. 28

D.4. LLM repair cost and recorded latency

  • 223.59 recorded seconds per intervention is the five-candidate generation duration; the 14B single-candidate mean is 56.20 seconds and the 32B mean is 136.81 seconds on the same assigned cohort.These are summed recorded operation durations, distinct from wall-clock experiment time.Source: §D.4 · p. 29, §D.4.1 · p. 29

D.4.1. Request and review accounting

  • Plan review adds 188 revision operations and 71 rechecks, while row review adds 783 revisions and 716 rechecks because it tests individual source requirements plan review can leave unexamined.Both approaches share 1,452 initial checks.Source: §D.4.1 · p. 30

D.5. Full before-and-after repair results

Across six generators, protected selection retained correct answers while increasing model–code matches; host-system integrations and source-review experiments separately tested transfer and shared omissions.

D.5. Full before-and-after repair results

  • 7,308 of 18,204 outputs were both correct and model–code matched under protected ORSMT selection, retaining 4,931 correct answers and adding 2,378.Answer counts use 18,192 numeric-reference outputs; match counts use all 18,204 assigned outputs.Source: §D.5 · p. 30, Table 32 · p. 30

D.6. Transfer to OptiMUS-0.3 and OptiMind

  • For OptiMUS-0.3, paired accounting added 825 artifact matches and 552 correct answers; outputs both correct and matched rose from 630 to 1,199 with no losses.ORSMT selected reconstructions or certified voting for 1,938 assignments and used shared fallback for the remaining 1,096.Source: §D.6 · p. 31, Table 33 · p. 31
  • For OptiMind, paired accounting over 3,034 assigned problems added 683 artifact matches and 19 correct answers, including 223 outputs satisfying both, with no losses.Source: §D.6 · p. 32, Table 34 · p. 32

D.7. Source requirements after repair

  • Among 654 source-requirement pairs, the audit admitted 4,614 typed obligations and produced 293 complete certificates, 54 explicit-source refutations, 75 symmetry-only refutations, and 232 undecided pairs.A separate revision cohort followed 1,452 finite repair candidates and 231 adopted row revisions.Source: §D.7 · p. 32, Table 35 · p. 33, Table 36 · p. 33

D.7.1. Prompts for source review and revision

  • Source reviews compare the problem statement with the certified model and computed plan, flag omitted or misstated requirements, then revise flagged programs using the source as the implementation target.Plan and row reviews use separate judgments; fixed parsing rules and review limits govern what is passed to revision.Source: §D.7.1 · pp. 32–33

D.8. Residual constraint errors after repair

The section measures residual constraint differences after repair, reports protected-selection outcomes by benchmark and generator, and tests semantic criteria against exact relations.

D.8. Residual constraint errors after repair

  • ORSMT introduced the fewest constraint differences and left fewer residual differences than either baseline across the 951 fully decided outputs, before protected adoption.Figure 5 shows row totals and each output’s direction of change.Source: §D.8 · p. 33, Figure 5 · p. 34, Table 37 · p. 34
  • The paired row comparison uses sequential entailment to remove redundant rows; its complete decisions require every relevant row query to decide.It examined 7,620 original and revised pairs using exact rational arithmetic and integer domains; eight records with unresolved row queries were excluded.Source: §D.8 · p. 34

D.9. Results by benchmark and generator

  • The 7,308 outputs satisfying both correctness and model–code match sum across benchmark and generator cells, with lower counts on two Text2Opt families and OptMATH.Table 39 reports the per-benchmark and per-generator counts after protected selection.Source: §D.9 · p. 35, Table 39 · p. 35

E.1. Controlled semantic edits and preserving rewrites

  • Of 640 applicable semantic edits, 562 were different, 67 equivalent, and 11 unresolved; each of five preserving rewrites produced 144 equivalent pairs.Outcome value, mapped optimum, structural matching, and falsification were evaluated against exact relation labels.Source: §E.1 · p. 35, Table 40 · p. 36
  • Four-point falsification gave the best balance between detecting changed pairs and accepting equivalent pairs among the compared criteria.The exact semantic relation supplied the reference partition.Source: §E.1 · p. 35, Table 41 · p. 36, Table 42 · p. 36

E.2. Large edit evaluation

Large semantic edits expose cases where weaker criteria miss changed models; the accompanying worked-case section connects formal counterexamples to repair outcomes.

E.2. Large edit evaluation

  • Outcome value missed 4,721 proved changes, while a test of only one region-inclusion direction missed 5,738.Constraint deletion and integrality relaxation often preserve the optimum; tightening requires the opposite inclusion direction to expose excluded decisions.Source: §E.2 · p. 37, Table 43 · p. 37

F. Worked Inconsistency and Repair Cases

  • The worked cases connect original artifacts, verification evidence, repairs, and subsequent checks to exact domains, objective directions, and constraint coefficients.Cases include region differences, shared omissions, domain errors, redundant rows, and an incorrect negative solution judgment.Source: F. Worked Inconsistency and Repair Cases · p. 37

F.1. A ReLoop pass with inconsistent feasible regions

The worked cases show how exact relation checks distinguish agreement between artifacts from agreement with source requirements, and how verified repairs address specific mismatches.

F.1. A ReLoop pass with inconsistent feasible regions

  • IndustryOR 71 had a correct value of 623 despite different feasible regions; either artifact could be reconstructed from the other, and both repair directions certified the pair.Two witnesses exposed the set differences, while a fresh replay checked the constructed programs and returned the same value.Source: §F.1 · pp. 37–38, Figure 6 · p. 37

F.2. Missing source requirements in two generated artifacts

  • In MAMO easy 20, model–code repair restored a missing capacity row but left the shared source omission; source review then restored both quality rows and a correct answer of 16,300.The initial zero decision remained optimal under the incomplete artifacts but violated both source quality requirements.Source: §F.2 · pp. 39–40

F.3. A domain mismatch and redundant constraints

  • In ComplexOR 3, changing code’s binary x to a nonnegative integer certified the pair, and deleting two duplicate rows preserved equivalence; the repaired generated model still had optimum two, not the released answer three.Restoring the source formulation would require indexed assignment variables and constraints.Source: §F.3 · p. 41, Figure 7 · p. 41

F.4. An incorrect Opt-Verifier judgment on a certified solution

  • In BWOR 18, the exact checks certified the model pair and value 34; Opt-Verifier’s alternative actually cost 37, so the certificate prevented unnecessary revision.The incorrect feedback arose from arithmetic, not model extraction or variable alignment.Source: §F.4 · p. 41

Related papers

Loading 2610.29145v1…