Paper deep dive
From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
Dipankar Sarkar
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 8/18/2026, 4:37:59 AM
Summary
This paper introduces a minimal-core-guided repair mechanism for neuro-symbolic constraint solving, where language models translate natural language problems into Answer Set Programming (ASP). Instead of relying on generic solver error messages, the system extracts a minimal unsatisfiable core (MUC) to localize faults in the model's generated constraints. Evaluated on a benchmark of 77 problems, the approach significantly reduces solution fabrication (from 79% to 7% on weaker models) and improves feasibility accuracy, though strong chain-of-thought baselines remain competitive in accuracy. The primary value of the symbolic route is its ability to provide certificates of infeasibility and avoid hallucination.
Entities (8)
Relation Signals (6)
Answer Set Programming → usedfor → Constraint solving
confidence 98% · translation to Answer Set Programming is faithful on six of seven domains
Minimal-unsatisfiable core → usedin → Neuro-symbolic constraint solving
confidence 95% · We replace the error message with a proof: when the generated program is unsatisfiable, we extract a minimal unsatisfiable core
Minimal-unsatisfiable core → reduces → Fabrication
confidence 92% · A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions... cutting fabrication from 79% to 7%
Clingo → usedby → Answer Set Programming
confidence 90% · solve with clingo
Scheduling → challenges → Translation fidelity
confidence 88% · fails only on aggregate-coverage scheduling, which concentrates the translation tax in one diagnosable pattern
Chain-of-Thought → matches → Symbolic route
confidence 85% · A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Making language models solve constraint problems reliably often means having them translate the problem into a formal specification and delegating the search to a sound solver. But the translation is itself a language-model task, and an unfaithful translation makes the solver faithfully solve the wrong problem. Existing pipelines repair only translations that crash, returning the solver's error message and falling silent when the program runs but is wrong. We replace the error message with a proof: when the generated program is unsatisfiable, we extract a minimal unsatisfiable core over the model's own constraints and hand it back the exact set that cannot hold together, a leakage-free signal that localizes the fault. On a new benchmark of 77 problems with an exact oracle, translation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate coverage scheduling, which concentrates the translation tax in one diagnosable pattern. A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions to infeasible problems, cutting fabrication from 79% to 7%. A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy, so the route's value is not accuracy but certificates and its refusal to fabricate.
Tags
Links
- Source: https://arxiv.org/abs/2608.14771v1
- Canonical: https://arxiv.org/abs/2608.14771v1
Trouble viewing inline? Open PDF directly →
Full Text
36,713 characters extracted from source content.
Expand or collapse full text
From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving Dipankar Sarkar Independent Researcher dipankar@skelfresearch.com Abstract Making language models solve constraint prob- lems reliably often means having them translate the problem into a formal specification and dele- gating the search to a sound solver. But the trans- lation is itself a language-model task, and an un- faithful translation makes the solver faithfully solve the wrong problem. Existing pipelines repair only translations that crash, returning the solver’s error message and falling silent when the program runs but is wrong. We replace the error message with a proof: when the generated program is unsatisfi- able, we extract a minimal unsatisfiable core over the model’s own constraints and hand it back the exact set that cannot hold together, a leakage-free signal that localizes the fault. On a new bench- mark of 77 problems with an exact oracle, trans- lation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate- coverage scheduling, which concentrates the trans- lation tax in one diagnosable pattern. A minimal core, rather than a bare error, is what stops a weaker model from fabricating solutions to infeasible prob- lems, cutting fabrication from 79% to 7%. A strong chain-of-thought baseline meanwhile matches the symbolic route on accuracy, so the route’s value is not accuracy but certificates and its refusal to fabri- cate. 1 Introduction Language models are increasingly asked to solve discrete reasoning problems such as scheduling, seating, assignment, and packing. Left to free-form generation they return flu- ent answers that often violate the stated constraints, be- cause autoregressive decoding has no mechanism to enforce a global combinatorial constraint. A standard remedy sepa- rates translation from search: the model converts the natural language problem into a formal specification, and a sound solver does the reasoning [ Pan et al., 2023; Ye et al., 2023; Olausson et al., 2023; Gao et al., 2023 ] . The solver supplies the guarantee the model cannot. This recipe is only as good as the translation, and language- model translations fail in two different ways. Some are mal- formed and the solver reports a parse or grounding error. Others are well formed but unfaithful: they add a constraint the problem never stated, which can make a solvable prob- lem report as unsatisfiable; they drop a stated constraint, which admits an invalid solution; or they misstate the ob- jective. The self-correction in current language-model plus solver pipelines, exemplified by the self-refinement in Logic- LM [ Pan et al., 2023 ] , reacts to the first kind: it returns the solver’s error message and asks the model to try again. When the solver does not error, the loop is silent, and the well formed but unfaithful encoding survives. We propose to repair with a proof rather than an error. We encode every decision as a single assign(Var,Value) relation in Answer Set Programming [ Lifschitz, 2008; Geb- ser et al., 2012 ] and solve with clingo [ Gebser et al., 2019 ] . When the program is unsatisfiable, we do not report “no so- lution”; we compute a minimal unsatisfiable core over the model’s own integrity constraints, the smallest subset that cannot all hold at once, and hand that set to the model. The core is a proof artifact: it localizes the conflict to a few con- straints, which is exactly the information a generic error mes- sage withholds. It is computed from the model’s own pro- gram rather than from ground truth, so it adds no oracle leak- age. We then ask an empirical question the literature rarely tests: at the scales where a solver can also certify the an- swer, how much does symbolic offloading actually help, rel- ative to plain prompting and to chain-of-thought, and where does it help. We answer it on a new benchmark of 77 prob- lems across seven domains with a programmatic oracle, on two open-weight models. The answer is nuanced rather than a uniform win. Translation is faithful on most domains and the symbolic route matches or beats chain-of-thought there, but a single domain breaks it; a strong chain-of-thought base- line is hard to beat on accuracy; and the distinctive payoff of the symbolic route is that it certifies optimality and infeasibil- ity and never fabricates a solution, which prompting cannot promise. Contributions. • Minimal-core-guided repair (Section 3): we repair a language model’s formalization with a minimal unsatis- 0 Accepted as a poster at the IJCAI-ECAI 2026 Workshop on Logic and Symbolic Reasoning (LogiSymb). arXiv:2608.14771v1 [cs.AI] 14 Aug 2026 fiable core over its own constraints rather than a solver error message. The signal is structural and leakage-free, it ports the conflict-explanation idea from constraint pro- gramming and answer set programming [ Junker, 2004; Gebser et al., 2008 ] into the repair loop, and we iso- late its effect with a controlled error-message baseline [ Pan et al., 2023 ] . The benefit is conditional: large on a weaker model, negligible on a stronger one that rarely errs. • A diagnosis of autoformalization fidelity (Section 6): with an exact oracle we show translation to ASP is faithful on six of seven domains and collapses only on aggregate-coverage scheduling, localizing the transla- tion tax to a formalization pattern rather than the model. • A recalibration of when offloading helps (Sections 6 and 7): a strong chain-of-thought baseline matches the symbolic route on accuracy, so its value is certificates and robustness; the route never fabricates a solution for an infeasible problem, whereas direct prompting does so 21% of the time. We release the benchmark and oracle. 2 Background and Related Work Our work sits at the meeting point of four lines: tool- augmented reasoning, autoformalization, self-correction, and conflict explanation. We take the method from the last and apply it to the problem raised by the first three. Faithful reasoning by offloading to solvers. A growing body of work makes language-model reasoning faithful by delegating inference to an external system. Logic-LM [ Pan et al., 2023 ] translates a problem into one of several sym- bolic languages and calls a matching solver; SatLM [ Ye et al., 2023 ] generates a declarative specification for a satisfiability- modulo-theories solver; LINC [ Olausson et al., 2023 ] maps text to first-order logic and calls a theorem prover; program- aided prompting [ Gao et al., 2023 ] offloads arithmetic to a Python interpreter. These methods target deductive question answering, on datasets such as ProofWriter, FOLIO, and AR- LSAT, or arithmetic word problems. We target combinatorial constraint satisfaction and optimization over Answer Set Pro- gramming, where correctness means feasibility or optimality of an assignment rather than the truth of an entailment, and where the relevant failure is silent over-constraint or under- constraint rather than a wrong proof step. Autoformalization is the bottleneck. Once search is del- egated, accuracy is bounded by the fidelity of the transla- tion. Autoformalization studies this translation directly, from natural language to formal mathematics [ Wu et al., 2022 ] . For optimization specifically, the NL4Opt competition [ Ra- mamonjison et al., 2023 ] and OptiMUS [ AhmadiTeshnizi et al., 2024 ] map word problems to mixed-integer linear pro- grams. Consistent with that line, we find that the bottleneck is the formalization rather than the search, and that it is uneven across problem types: faithful on most constraint domains, brittle on the one that needs aggregate-coverage reasoning. We also confirm a known boundary, that Answer Set Pro- gramming is a poor vehicle for large numeric optimization, and keep optimization instances small enough for the solver to certify optima. Self-correction and the signal it uses. Iterative self- correction improves model outputs, and the methods differ mainly in what signal drives the next attempt. Self-Refine [ Madaan et al., 2023 ] and Reflexion [ Shinn et al., 2023 ] use the model’s own verbal critique; Self-Debugging [ Chen et al., 2024 ] uses program execution results; Logic-LM [ Pan et al., 2023 ] uses the solver’s error message. All of these react to an observed event: a critique, a failed test, a crash. None uses a proof of why the current attempt is inconsistent. Our repair signal is exactly such a proof, and our controlled comparison shows that what matters is not that repair happens but what information it carries. Conflict explanation and minimal unsatisfiable cores. Identifying a small set of constraints responsible for unsat- isfiability is a classical problem in constraint programming and satisfiability. Junker’s QuickXplain [ Junker, 2004 ] com- putes preferred minimal conflicts for over-constrained prob- lems by divide and conquer, and deletion-based filtering is the simplest member of that family. In Answer Set Program- ming the same idea underlies debugging of inconsistent pro- grams [ Gebser et al., 2008 ] and core-guided optimization in- side modern solvers [ Gebser et al., 2019 ] . Our contribution is to carry this proof artifact across the boundary into the language-model repair loop: instead of asking the model to debug from a flat error string, we hand it the minimal con- flicting subset that a solver-side conflict analysis produces. To our knowledge, minimal unsatisfiable cores have not been used as the feedback signal for repairing a language model’s formalization. 3 Approach Our system follows the standard division of labor between a language model and a solver, but it makes the translation step robust instead of assuming it correct. The model is responsi- ble only for turning a natural language problem into a formal specification; a sound solver does all of the search. Our con- tribution is the loop that sits between them. When the solver reports that the specification has no solution, we neither ac- cept that verdict at face value nor restart the model blindly. We extract a proof of the inconsistency, in the form of a min- imal unsatisfiable core, and ask the model to reconcile that proof with the problem text. A problem passes through four stages. First, the model produces a structured ASP encoding over a fixed decision re- lation. Second, the encoding is assembled into a program and run through clingo. Third, the solver outcome is classified into one of four categories, and if it is not a clean success a typed diagnostic is constructed from the solver state. Fourth, the diagnostic is returned to the model, which revises the en- coding; the second through fourth stages then repeat up to K times. Only the first stage uses the model creatively. The rest are deterministic and grounded in the solver, so every correc- tion the loop applies is justified by a concrete solver artifact rather than by another free-form guess. % facts (problem data) node(n1). node(n2). node(n3). color(red). color(green). color(blue). % choice rule: one colour per node 1 assign(N,C) : color(C) 1 :- node(N). % integrity constraints: % adjacent nodes get different colours :- assign(n1,C), assign(n2,C). :- assign(n2,C), assign(n3,C). % harness appends: #show assign/2. Figure 1: A complete assign/2 encoding of a three-node graph- coloring problem. The choice rule generates one colour per node; each integrity constraint forbids an edge from being monochromatic. 3.1 The decision contract The model emits a JSON object with three fields: facts, which encode the problem data; rules, which contain a choice rule that generates candidate decisions together with the integrity constraints that enforce the requirements; and an optional optimize directive. We impose a single contract on this output. Every decision is expressed through one rela- tion, assign(Var,Value), in which each decision vari- able Var is bound to exactly one Value by a choice rule, and every requirement is expressed as an integrity constraint, a rule that begins with :- and forbids the combinations that violate it. The harness appends #show assign/2. and calls clingo. Figure 1 shows a complete encoding for a small graph-coloring instance. This contract serves three purposes, and each matters for the rest of the method. First, it gives a single, uniform notion of a solution across every domain, so that one oracle can score the output of any system, whether it is the symbolic pipeline or a prompting baseline, without domain-specific parsing; a coloring, a roster, a seating, and a knapsack packing are all just sets of assign atoms. Second, it keeps the encoding compact and stable in size as the problem grows, because the decision logic lives in a constant number of rules while only the facts scale; a graph with three nodes and a graph with ninety nodes share the same choice rule and the same constraint schemas. Third, and most important for repair, it cleanly separates the part of the program the model might get wrong, the integrity constraints, from the part that is fixed by the data, the facts and the choice rule, which is exactly the separation the core extraction in Section 3.3 exploits. To keep the comparison fair, every system in our study, including the prompting baselines, is given the same decision variables and their allowed values, so no system is advantaged or penalized by the output format and all of them are judged purely on whether they reason to a correct assignment. 3.2 Compiling and classifying the outcome Assembling and solving an encoding yields exactly one of four outcomes, and the loop reacts to each differently. An outcome is OK when clingo returns an answer set that con- tains assign/2 atoms; this is the only terminating out- come, and the atoms become the assignment. It is SYN- TAX ERROR when grounding or parsing fails, which happens when the model writes a malformed rule or an unsafe vari- able. It is EMPTY when the program is satisfiable but pro- duces no assign/2 atoms, which happens when the model Algorithm 1 Minimal unsatisfiable core (deletion filtering) Require: base B, constraints C; B∪ C unsatisfiable 1: C ⋆ ← C 2: for all c∈ C do 3:if B∪ (C ⋆ \c) is UNSAT then 4:C ⋆ ← C ⋆ \cdrop c 5:end if 6: end for 7: return C ⋆ forgets the choice rule or models its decisions under some other predicate. It is UNSAT when the program is well formed and grounds cleanly but has no answer set. The four outcomes are not equally informative, and the asymmetry is the reason the rest of the method exists. A SYN- TAX ERROR is loud: clingo points at the offending rule, and prior error-message refinement already handles this case well. The dangerous outcome is UNSAT, because it is silent about its cause. An over-constrained translation of a perfectly solv- able problem, for instance one that hallucinates a constraint the text never stated, produces a program with no answer set, and that program is indistinguishable, from the bare verdict alone, from a faithful translation of a genuinely infeasible problem. The model that reads only “no answer set” cannot tell whether it should fix its own constraints or report that the problem has no solution. Resolving that ambiguity is what the core provides. 3.3 Repair with a minimal unsatisfiable core On UNSAT we localize the conflict before asking the model to act. Let C = c 1 , . . . , c m be the integrity constraints the model produced and B the base program made of the facts and the choice rule. Because B is satisfiable on its own (the choice rule alone always has models), the inconsistency must come from a subset of C. We compute a minimal unsatisfi- able subset C ⋆ ⊆ C, defined by the property that B ∪ C ⋆ is unsatisfiable while B ∪ (C ⋆ \c) is satisfiable for every c ∈ C ⋆ , so that every constraint in C ⋆ is necessary for the conflict and none is redundant. We obtain it by deletion filter- ing (Algorithm 1), the simplest member of the QuickXplain family of conflict-extraction procedures [ Junker, 2004 ] : start- ing from the full set, we tentatively remove each constraint and keep the removal whenever the remainder is still unsatis- fiable. The procedure issues at most m satisfiability checks, each a fast call on a small program, and for the instance sizes in our benchmark its cost is negligible next to a single model call. Two properties of this signal matter. It is structural: C ⋆ is a proof that those constraints cannot coexist, not a report that something went wrong, and it names the exact constraints to reconsider rather than leaving the model to search its whole program. It is leakage-free: every satisfiability check in Al- gorithm 1 runs on the model’s own program, with the ob- jective removed, and at no point does the procedure consult the ground-truth answer, the oracle, or the reference encoder. The core therefore tells the model where its translation is in- ternally inconsistent, which is information the model is en- titled to, without telling it what the correct answer is, which it is not. This distinction is what lets us use the core during inference without contaminating the evaluation. The repair prompt for UNSAT lists the constraints in C ⋆ verbatim and frames the choice the core makes explicit: ei- ther one of these constraints misformalizes the problem, in which case the model should correct or remove it, or the named constraints all faithfully encode the text and the prob- lem is genuinely infeasible, in which case the model should leave the encoding unchanged so that the system reports in- feasibility. This is the central design point. By naming the conflict, the core makes “the problem is infeasible” a legiti- mate and well supported answer, which is the answer a model is likely to abandon when it is told only that the solver found nothing. The other two failure types take simpler prompts: SYNTAX ERROR carries the grounder message and asks for a parse fix, and EMPTY asks the model to add the choice rule so that decisions surface as assign/2. After any repair the program is re-solved, and the loop runs up to K = 3 times. Example 1 traces the loop on a real instance from our bench- mark. Example 1 (Repairing an over-constrained roster) On a six-worker, five-day roster, the model’s first encoding is unsatisfiable. Deletion filtering returns a minimal core of seven constraints: the coverage requirement for the final day together with the six per-worker caps that, taken together, leave no worker free to staff that day. The repair prompt lists exactly these seven constraints. The model recognizes that it had encoded the final-day coverage more strictly than the text required, relaxes that one constraint, and the next solve returns a valid roster, in a single repair iteration. A generic error message for the same instance would have said only that the program had no answer set, and, as Section 6 shows, a weaker model given that message tends to keep editing until it returns a roster for a problem that has none. 3.4 Isolating the signal: a faithful error-message baseline To attribute any effect to the core rather than to the act of re- pairing, we build a second repair setting that is identical in ev- ery respect except the feedback. It uses the same pipeline, the same model, the same iteration budget, and the same decision contract, but on any failure it returns only the raw solver mes- sage, with no core and no per-failure guidance. This recon- structs the error-message self-refinement of prior language- model plus solver systems [ Pan et al., 2023 ] inside our setup. We refer to the two settings as TYPED+CORE and GENERIC. Because they differ only in the information content of the feedback, any difference in their behavior is attributable to the core, and Section 6 reports that the difference is small on a strong model and large on a weak one. 4 Benchmark We generate 77 instances over seven domains: graph color- ing, knapsack, team assignment, seating, timetabling, duty scheduling, and Latin squares. Each instance pairs a descrip- tion with a structured specification over assign/2; the de- scription states every constraint in the specification, so a sys- tem is never penalized for information it was not given. A SystemFeas. acc. CSR Fabr. Iters Direct74.084.521.40.00 Chain-of-thought98.799.80.00.00 ASP, no repair84.485.00.00.00 ASP, generic repair88.391.30.00.78 ASP, typed+core repair89.691.30.00.87 Table 1: Primary model (gemma4:31b), 77 instances, percent. Higher is better except fabricated feasibility (Fabr.), measured over the 14 infeasible instances. deterministic encoder, independent of the language model, computes ground-truth feasibility and, for optimization in- stances, the optimum; a separate oracle scores any assign- ment for constraint satisfaction, feasibility, and objective. In- stances carry one of five labels: feasible, tight (numerically tight but solvable), infeasible (the correct behavior is to re- port unsatisfiability), stress (larger), and xl (60 to 120 deci- sion variables). The xl tier is feasibility-only, because clingo certifies one model quickly at that size but cannot certify large numeric optima or large infeasibility quickly. 5 Experimental Setup Models. We use two open-weight models, gemma4:31b as the primary model and deepseek-v3.2, served through a hosted inference provider with greedy decoding. Both are run with the same pipeline and prompts. Systems. (B1) direct: the model outputs the assignment. (B2) chain-of-thought [ Wei et al., 2022 ] : reason then answer. (B3) the ASP pipeline with no repair. (B4) the pipeline with Logic-LM-style generic-error repair. (B5) the pipeline with typed plus minimal-core repair. Metrics. Feasibility accuracy (a valid assignment on feasi- ble instances, or a correct unsatisfiability report on infeasi- ble ones); constraint-satisfaction rate; fabricated feasibility, a committed solution for an infeasible problem; optimality gap on optimization instances; and average repair iterations. We omit per-system token counts, because shared response caching across the three pipeline settings confounds them. 6 Results Table 1 reports the primary model over all 77 instances. Direct prompting is unreliable;chain-of-thought is strong. Direct prompting reaches 74.0% feasibility accu- racy and fabricates a solution on 3 of 14 infeasible instances (21.4%).Chain-of-thought reaches 98.7% and fabricates none. At the scales in this benchmark, an explicit reason- ing chain solves, optimizes, and recognizes infeasibility for almost every instance without any solver. The translation tax is concentrated in one domain. The pooled pipeline numbers understate what is happening per domain. Table 2 shows that on six of seven domains the no-repair pipeline already reaches 100% feasibility accuracy, and on coloring it exceeds chain-of-thought (100% versus 94.7%). The entire deficit comes from scheduling, where the model must encode aggregate coverage and per-worker caps DomainCoTASP no rep.ASP +core graph coloring94.7100.0100.0 knapsack100.0100.0100.0 Latin square100.0100.0100.0 seating100.0100.0100.0 team assignment100.0100.0100.0 timetabling100.0100.0100.0 scheduling100.00.033.3 Table 2: Feasibility accuracy by domain, primary model. The pipeline matches or beats chain-of-thought everywhere except scheduling, which needs aggregate-coverage encoding. with counting constraints, and where the no-repair pipeline scores 0%. In other words, language-model translation to ASP is faithful wherever the constraints are local, and breaks on the one domain that needs global counting. This is a sharper statement than “the pipeline is less accurate”: it tells us which formalization patterns the model can be trusted to produce. Repair is monotone and a core helps where it is needed. Self-repair lifts the pipeline from 84.4% to 89.6% on the primary model. The improvement is safe: across all 77 instances, repair turned four first-attempt failures into suc- cesses and broke none. Fifty-four instances solved on the first attempt; the rest entered the loop, and the instances that exhausted the budget are exactly the scheduling cases the model cannot encode. On the primary model, typed plus minimal-core repair (89.6%) edges generic repair (88.3%), but the gap is within noise for a model this strong (paired sign test p = 1.0): a model that rarely produces a spurious unsatisfiability rarely needs the core. The difference is stark on a weaker model. On deepseek-v3.2, generic error- message repair fabricates a solution on 11 of 14 infeasible instances (79%), because, told only that the program has no answer set, it deletes a real constraint until the solver returns a model; minimal-core repair fabricates on 1 of 14 (7%), a difference that is significant by a two-sided Fisher exact test (p < 10 −3 , Table 3). Appendix A traces both behaviors on one infeasible instance. Naming the conflicting constraints is what prevents the model from fabricating a solution. Certificates and robustness. No pipeline setting ever fab- ricates a solution for an infeasible problem (0% in Table 1), against 21.4% for direct prompting, because clingo either re- turns an answer set or proves there is none. On optimization instances the returned solution is provably optimal (zero op- timality gap), whereas a prompted answer is optimal only by inspection. These are guarantees that a prompting system, however accurate in aggregate, cannot make about any single answer. Scale. Figure 2 breaks the primary model down by problem-size tier. Chain-of-thought stays at or near 100% through the stress tier and drops only to 90% on the xl tier. The clearest accuracy crossover is a single xl instance, a 90- node three-colorable graph, where chain-of-thought violates an edge while the core pipeline returns a valid coloring. The pipeline has its own scale failure on a 120-variable schedul- SmallStressXL 0 20 40 60 80 100 Feasibility accuracy (%) gemma4:31b: accuracy by problem-size tier Direct Chain-of-thought ASP, no repair ASP, generic repair ASP, typed+core Figure 2: Feasibility accuracy by problem-size tier on the primary model (smalln=56, stressn=11, xln=10). The pipeline beats direct prompting throughout but does not overtake chain-of-thought, whose only visible drop is on the xl tier. ModelDirectGeneric repairCore repair gemma4-31b2100 deepseek-v3.20797 Table 3: Fabricated feasibility, the rate at which a system commits to a solution for an infeasible problem, over the 14 infeasible instances, by model and repair signal. Generic error-message repair drives a weaker model to fabricate; a minimal core does not. ing instance, the same domain that fails at small scale. At the sizes a solver can certify quickly, neither method dominates the other on accuracy. 7 Discussion We draw three lessons. First, offloading constraint reason- ing to a solver should be justified by guarantees and robust- ness, not by accuracy alone: a strong chain-of-thought base- line is hard to beat on accuracy at the scales where a solver can also certify the answer, but it cannot certify infeasibility or optimality, and direct prompting fabricates feasibility of- ten enough (21% here) to matter wherever a wrong answer is costly. Second, the fidelity of language-model autoformal- ization is uneven and the unevenness is structured: it is near- perfect for local constraints and breaks on global counting, which suggests that the right unit of trust is the formalization pattern, not the model. Third, the form of the repair signal matters most when the model is weak; a minimal core tells the model which constraints conflict, which discourages the fabrication that a flat error message can induce. The broader message for symbolic reasoning with language models is that solver-side artifacts, not just solver verdicts, are useful feed- back, and minimal cores are one such artifact. 8 Limitations The benchmark uses templated descriptions and a single assign/2 decision relation, which fits discrete constraint and optimization problems but not problems with derived nu- meric quantities. Answer Set Programming cannot certify large numeric optima or large infeasibility quickly, which bounds how far we can push scale while keeping exact ground truth, and the accuracy crossover is therefore a single in- stance. Repair is driven by solver-intrinsic signals only, so a missing constraint that yields a satisfiable but invalid encod- ing is caught by the oracle at evaluation rather than repaired in the loop; a verifier in the loop is the natural next step. Threats to validity. Four caveats bound our conclusions. First, the benefit of the core over a bare error message is demonstrated on one of our two models; on the stronger model the two are indistinguishable, so the result identifies a regime, weaker and fabrication-prone models, in which feed- back shape matters, rather than a universal gain. Confirming the effect on more models is the most important next step, which we leave to future work. Second, every system is given the decision variables and their allowed values, which makes the task easier than open-ended translation and, if anything, flatters the prompting baselines and understates the symbolic route’s relative value. Third, the symbolic pipeline issues sev- eral model calls per problem against one or two for prompt- ing, so its accuracy parity comes at a compute premium that we do not chart in detail. Fourth, the scheduling failure is reported under a fixed prompt, and a different prompt or a worked counting example might narrow it, so the per-domain diagnosis should be read as a property of this configuration rather than a law of autoformalization. 9 Conclusion We replaced the error message in a language-model plus solver repair loop with a proof: when the generated program is unsatisfiable, we hand the model a minimal unsatisfiable core over its own constraints. On 77 constraint and opti- mization problems and two open-weight models, the resulting pipeline is faithful on six of seven domains, repairs monoton- ically, and uses the core exactly where weaker models would otherwise hallucinate feasibility. The same study shows that symbolic offloading does not beat a strong chain-of-thought baseline on accuracy at verifiable scales; its value is that it never fabricates a solution and certifies the answers it does re- turn. We read these results as an argument to treat solver-side proof artifacts as first-class feedback for language-model for- malization, and we release the benchmark and oracle to make the scale question sharper. A Repair feedback and a worked trace The two repair settings share the pipeline, the model, and the iteration budget, and differ only in the feedback returned on an UNSAT outcome. The generic setting returns the raw ver- dict: clingo found no answer set (unsatisfiable). The typed-core setting returns the minimal core and the deci- sion it implies: The following integrity constraints are JOINTLY UNSATISFIABLE (a minimal conflicting set): - :- assign(X,C),assign(Y,C),border(X,Y). If one of them misformalizes the problem, correct or remove it; if the problem is genuinely infeasible, leave it unchanged. Trace on an infeasible instance. The instance is a four-node clique, every pair of nodes adjacent, with three colors, which is genuinely infeasible because a clique of four needs four colors. On deepseek-v3.2: • Generic repair.The first solve is unsatisfiable and the model receives only “no answer set.”It respondsbyweakeningitscoloringconstraint, which makes the program satisfiable,and re- turns assign(n3,c1), assign(n4,c1), assign(n2,c2), assign(n1,c3).Nodes n3 and n4 are adjacent yet share color c1: the system reports an invalid coloring as a solution. • Minimal-core repair. Each solve is unsatisfiable, and each time the feedback names the single coloring con- straint as the conflict. The model judges that constraint to be a faithful encoding of adjacency, leaves it un- changed, and after the iteration budget reports the in- stance infeasible, which is correct. This is the mechanism behind the aggregate numbers: a bare verdict invites the model to dissolve the conflict by dropping a true constraint, while the core makes “the problem is infea- sible” the better-supported response. References [ AhmadiTeshnizi et al., 2024 ] Ali AhmadiTeshnizi, Wenzhi Gao, and Madeleine Udell.OptiMUS: Scalable opti- mization modeling with (MI)LP solvers and large lan- guage models.In Proceedings of the 41st Interna- tional Conference on Machine Learning (ICML), 2024. arXiv:2402.10172. [ Chen et al., 2024 ] Xinyun Chen, Maxwell Lin, Nathanael Sch ̈ arli, and Denny Zhou. Teaching large language mod- els to self-debug. In International Conference on Learning Representations (ICLR), 2024. arXiv:2304.05128. [ Gao et al., 2023 ] Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. PAL: Program-aided language models. In Proceedings of the 40th International Conference on Machine Learning (ICML), 2023. arXiv:2211.10435. [ Gebser et al., 2008 ] Martin Gebser, J ̈ org P ̈ uhrer, Torsten Schaub, and Hans Tompits. A meta-programming tech- nique for debugging answer-set programs. In Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI), pages 448–453, 2008. [ Gebser et al., 2012 ] Martin Gebser, Roland Kaminski, Ben- jamin Kaufmann, and Torsten Schaub. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. [ Gebser et al., 2019 ] Martin Gebser, Roland Kaminski, Ben- jamin Kaufmann, and Torsten Schaub. Multi-shot ASP solving with clingo. Theory and Practice of Logic Pro- gramming, 19(1):27–82, 2019. arXiv:1705.09811. [ Junker, 2004 ] Ulrich Junker. QUICKXPLAIN: Preferred explanations and relaxations for over-constrained prob- lems. In Proceedings of the 19th National Conference on Artificial Intelligence (AAAI), pages 167–172, 2004. [ Lifschitz, 2008 ] Vladimir Lifschitz. What is answer set pro- gramming? Proceedings of the AAAI Conference on Arti- ficial Intelligence, 2008. [ Madaan et al., 2023 ] Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Kather- ine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self- feedback. In Advances in Neural Information Processing Systems (NeurIPS), 2023. arXiv:2303.17651. [ Olausson et al., 2023 ] Theo Olausson, Alex Gu, Ben Lip- kin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. LINC: A neurosymbolic ap- proach for logical reasoning by combining language mod- els with first-order logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natural Lan- guage Processing (EMNLP), 2023. [ Pan et al., 2023 ] Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Com- putational Linguistics: EMNLP 2023, pages 3806–3824, 2023. arXiv:2305.12295. [ Ramamonjison et al., 2023 ] Rindra Ramamonjison, Timo- thy T. Yu, Raymond Li, Haley Li, Giuseppe Carenini, Bissan Ghaddar, Shiqi He, Mahdi Mostajabdaveh, Amin Banitalebi-Dehkordi, Zirui Zhou, and Yong Zhang. NL4Opt competition: Formulating optimization problems based on their natural language descriptions. In Proceed- ings of the NeurIPS 2022 Competitions Track, PMLR vol. 220, 2023. arXiv:2303.08233. [ Shinn et al., 2023 ] Noah Shinn, Federico Cassano, Edward Berman, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: Language agents with verbal re- inforcement learning. In Advances in Neural Information Processing Systems (NeurIPS), 2023. arXiv:2303.11366. [ Wei et al., 2022 ] Jason Wei, Xuezhi Wang, Dale Schuur- mans, Maarten Bosma, Brian Ichter, Fei Xia, Ed Chi, Quoc Le, and Denny Zhou. Chain-of-thought prompting elic- its reasoning in large language models. In Advances in Neural Information Processing Systems (NeurIPS), 2022. arXiv:2201.11903. [ Wu et al., 2022 ] Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Advances in Neural Information Processing Systems (NeurIPS), 2022. arXiv:2205.12615. [ Ye et al., 2023 ] Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SatLM: Satisfiability-aided language mod- els using declarative prompting.In Advances in Neu- ral Information Processing Systems (NeurIPS), 2023. arXiv:2305.09656.