Source-linked AI summary
From Errors to Proofs: Minimal-Core-Guided Repair for Neuro-Symbolic Constraint Solving
Dipankar Sarkar
TL;DR
Language-model translations of constraint problems can be wrong even when they run, leaving standard repair pipelines without a diagnosis. This paper replaces bare solver errors with minimal unsatisfiable cores and finds faithful translation on six of seven domains, while the symbolic route’s main value is certification and refusal to fabricate rather than higher accuracy.
Problem
Language-model translations can misformalize constraint problems without crashing, making solver feedback unable to distinguish flawed encodings from genuinely infeasible problems.
Method
The system repairs unsatisfiable formalizations by extracting a minimal unsatisfiable core from the model’s own constraints and asking the model to reconcile that conflict with the problem text.
Results
Translation to Answer Set Programming is faithful on six of seven domains, while a strong chain-of-thought baseline matches the symbolic route on accuracy.
Takeaways & Limitations
The symbolic route’s distinctive value is proof-backed certification of optimality and infeasibility together with refusal to fabricate solutions.
Takeaways & Limitations
The core’s benefit over a bare error message is demonstrated on only one of the two models, and the stronger model shows no difference between them.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper addresses unfaithful language-model formalizations by replacing solver error messages with minimal unsatisfiable cores that localize conflicting constraints. Experiments show ASP translation is faithful across most domains, while symbolic offloading’s main value is certification and robustness rather than accuracy.
- Translation failure: Language-model translations fail through malformed programs or well-formed but unfaithful constraints that add, drop, or misstate requirements.Existing self-correction pipelines primarily react to parse or grounding errors.
- Minimal-core-guided repair: Minimal unsatisfiable cores identify the smallest set of model-generated integrity constraints that cannot hold simultaneously, providing a structural, leakage-free repair signal.The method encodes decisions with a single assign(Var,Value) relation in ASP and computes cores with clingo.
- Autoformalization fidelity: Six of seven domains have faithful ASP translations, with failures concentrated in aggregate-coverage scheduling rather than spread uniformly across the benchmark.The benchmark contains 77 problems across seven domains and uses an exact programmatic oracle.
- When offloading helps: A strong chain-of-thought baseline matches the symbolic route on accuracy, shifting the route’s value toward certificates and robustness.The introduction frames symbolic offloading as a nuanced rather than uniformly superior strategy.
- When offloading helps: Direct prompting fabricates solutions for infeasible problems 21% of the time, whereas the symbolic route never fabricates an infeasible solution.Minimal-core repair provides a larger benefit for weaker models and negligible benefit for stronger models that rarely err.
2 Background and Related Work
This work combines solver-based faithful reasoning, autoformalization, self-correction, and conflict explanation. It focuses on using minimal unsatisfiable cores as a proof-based signal for repairing formal translations.
- Faithful reasoning by offloading to solvers: Solver-based reasoning delegates inference to external systems after translating natural-language problems into symbolic specifications.Examples include Logic-LM, SatLM, LINC, and program-aided prompting.
- Autoformalization is the bottleneck: Translation fidelity remains the bottleneck because solver accuracy is bounded by the correctness of autoformalization.The related work includes natural-language-to-mathematics studies and optimization systems such as NL4Opt and OptiMUS.
- Autoformalization is the bottleneck: Answer Set Programming is a poor vehicle for large numeric optimization, so optimization instances are kept small enough to certify optima.This limitation is stated as a known boundary of the approach.
- Self-correction and the signal it uses: Existing self-correction methods use verbal critiques, execution results, or solver error messages rather than proofs explaining why constraints conflict.Self-Refine and Reflexion use verbal critique; Self-Debugging uses execution; Logic-LM uses solver errors.
- Conflict explanation and minimal unsatisfiable cores: Minimal unsatisfiable cores identify small constraint sets responsible for unsatisfiability, extending classical conflict-explanation methods into Answer Set Programming debugging.QuickXplain computes preferred minimal conflicts by divide and conquer, while deletion-based filtering is a simpler related method.
3 Approach
The approach makes model-to-solver translation robust through an iterative pipeline that classifies solver outcomes and returns typed diagnostics. For UNSAT programs, it extracts a leakage-free minimal unsatisfiable core that identifies conflicting constraints for targeted repair.
- Pipeline: The model produces an ASP encoding, clingo solves it, failures receive typed diagnostics, and the model revises the encoding for up to K iterations.The pipeline has four stages: structured encoding, program execution, outcome classification with diagnostics, and model revision.
- Encoding contract: A uniform assign(Var,Value) contract represents decisions across domains, enabling one solution notion and oracle to evaluate different systems.Facts encode data, rules generate candidate decisions and enforce requirements, and an optional optimize directive may be included.
- Outcome classification: The solver distinguishes OK, SYNTAX ERROR, EMPTY, and UNSAT, with UNSAT posing the key challenge because it provides no cause for an over-constrained translation.OK is the only terminating outcome; SYNTAX ERROR is already localized by clingo, while EMPTY indicates satisfiability without assign/2 atoms.
- Minimal-core extraction: For UNSAT, deletion filtering computes a minimal unsatisfiable subset of the model’s integrity constraints while keeping the satisfiable base program fixed.The core remains unsatisfiable with the base program, but removing any core constraint makes it satisfiable.
- UNSAT repair: The core is structural and leakage-free: it names constraints that cannot coexist without revealing the correct answer, guiding the model to repair or preserve genuine infeasibility.The UNSAT repair prompt lists core constraints verbatim and asks whether they misformalize the text or faithfully encode an infeasible problem.
4 Benchmark
The benchmark contains 77 instances across seven constraint-solving domains, with descriptions fully specifying their structured constraints. Independent encoders and oracles determine feasibility, optimality, and assignment correctness across multiple instance tiers.
- Benchmark construction: 77 instances span seven domains, including graph coloring, knapsack, team assignment, seating, timetabling, duty scheduling, and Latin squares.Each instance pairs a natural-language description with a structured specification over assign/2.
- Evaluation: Independent deterministic components compute ground-truth feasibility and optimization optima, while a separate oracle scores constraint satisfaction, feasibility, and objective quality.The description states every specification constraint, so systems are not penalized for unavailable information.
- Instance tiers: Instances are labeled feasible, tight, infeasible, stress, or xl, with xl restricted to feasibility-only evaluation because clingo certifiesThe benchmark includes 14 infeasible instances for fabricated-feasibility measurement.
5 Experimental Setup
The experiments compare two open-weight models across direct, chain-of-thought, and ASP-based systems, including generic-error and typed minimal-core repair. Evaluation measures feasibility, constraint satisfaction, fabrication, optimization quality, and repair effort.
- Systems: Five systems span direct answering, chain-of-thought, unrepaired ASP, generic-error repair, and typed minimal-core repair.The repair variants are compared within the ASP pipeline.
- Metrics: Evaluation covers feasibility accuracy, constraint-satisfaction rate, fabricated feasibility, optimality gap, and average repair iterations.Per-system token counts are omitted because shared response caching confounds the three pipeline settings.
6 Results
The results show that ASP translation is reliable on six of seven domains, with failures concentrated in aggregate-coverage scheduling, while repair improves performance safely. The symbolic pipeline provides certificates and avoids fabrication, whereas chain-of-thought achieves strong accuracy without solver guarantees.
- Accuracy: 98.7% feasibility accuracy and zero fabrications make chain-of-thought strong, versus 74.0% accuracy and 21.4% fabrication for direct prompting.Chain-of-thought handled almost every instance without a solver.
- Domain results: Six of seven domains reach 100% feasibility accuracy without repair; coloring exceeds chain-of-thought at 100% versus 94.7%, while scheduling scores 0%.The deficit is attributed to aggregate-coverage and per-worker-cap counting constraints.
- Repair: 89.6% accuracy after self-repair improves on 84.4%, converting four first-attempt failures into successes without breaking any of 77 instances.Fifty-four instances solved initially; exhausted repair budgets were exactly scheduling cases.
- Certificates: 0% fabricated infeasible solutions and zero optimality gap distinguish the pipeline's solver-backed guarantees from prompted answers.Clingo either returns an answer set or proves none exists, and optimization outputs are provably optimal.
- Scale: 90% is chain-of-thought's xl-tier accuracy; it violates one edge on a 90-node graph, while the pipeline fails on a 120-variable scheduling instance.At solver-certifiable sizes, neither method dominates the other on accuracy.
7 Discussion
The discussion argues that solver-based constraint reasoning should be justified by guarantees and robustness, not accuracy alone. Although a strong chain-of-thought baseline is difficult to beat on accuracy, it cannot certify infeasibility or optimality, while direct prompting fabricates feasibility often enough to matter when errors are costly.
- Discussion: Solver-based constraint reasoning should be justified by guarantees and robustness, not accuracy alone.The discussion frames certification and robustness as the relevant reasons to offload reasoning to a solver.
- Discussion: A strong chain-of-thought baseline is hard to beat on accuracy at scales where a solver can also certify the answer.Accuracy alone therefore does not establish the solver route's value.
- Discussion: 21% direct-prompting fabrication of feasibility is consequential wherever wrong answers are costly.Unlike a solver, direct prompting does not provide certification of infeasibility or optimality.
8 Limitations
The study’s conclusions are limited by templated, discrete benchmarks, ASP’s difficulty with large numeric instances, and solver-only repair that misses satisfiable but invalid encodings. The core’s advantage is demonstrated only for weaker, fabrication-prone models, not as a universal gain.
- Benchmark and solver scope: The benchmark uses templated descriptions and a single assign/2 relation, limiting coverage to discrete constraint and optimization problems rather than derived numeric quantities.ASP also cannot quickly certify large numeric optima or infeasibility, limiting scale while preserving exact ground truth.
- Repair coverage: Solver-intrinsic repair signals miss satisfiable but invalid encodings, leaving missing-constraint errors to oracle evaluation rather than repairing them in the loop.The paper identifies an in-loop verifier as the natural next step.
- Threats to validity: The core’s benefit over a bare error message appears in one of two models; on the stronger model, the two feedback types are indistinguishable.This identifies a regime of weaker, fabrication-prone models rather than a universal gain, motivating confirmation on more models.
9 Conclusion
The pipeline replaces solver error messages with minimal unsatisfiable cores, giving the model a proof over its own constraints. Across 77 problems and two open-weight models, it is faithful on six of seven domains, repairs monotonically, and uses cores where weaker models would otherwise hallucinate feasibility.
- Conclusion: Minimal unsatisfiable cores replace error messages in the language-model–solver repair loop, providing a proof over the generated program’s own constraints.The core is handed to the model when the generated program is unsatisfiable.
- Conclusion: On 77 constraint and optimization problems, the pipeline is faithful on six of seven domains and repairs monotonically.The evaluation used two open-weight models.
- Conclusion: The pipeline uses minimal cores exactly where weaker models would otherwise hallucinate feasibility.This identifies the core’s role in preventing weaker models from fabricating feasible solutions.
A Repair feedback and a worked trace
The repair settings differ only in their UNSAT feedback: a bare solver verdict versus a minimal conflicting core and its implied decision. A worked infeasible coloring trace shows that the bare verdict produces an invalid solution, while the core preserves the true constraint and yields the correct infeasibility judgment.
- Repair feedback: The generic setting returns only the raw UNSAT verdict, “clingo found no answer set (unsatisfiable),” while sharing the same pipeline, model, and iteration budget as typed-core repair.The two settings differ only in feedback returned on an UNSAT outcome.
- Repair feedback: The typed-core setting returns a minimal set of jointly unsatisfiable integrity constraints together with the decision they imply.The feedback identifies a minimal conflicting set rather than only reporting unsatisfiability.
- Worked trace: On the four-node, three-color clique, generic repair weakens the coloring constraint and reports an invalid coloring in which adjacent nodes n3 and n4 share c1.The instance is genuinely infeasible because a four-node clique requires four colors.
- Worked trace: Minimal-core repair repeatedly identifies the single coloring constraint as conflicting, leaves it unchanged as faithful, and correctly reports the instance infeasible.Each solve remains unsatisfiable throughout the iteration budget.
- Repair feedback: A bare verdict invites dropping a true constraint, whereas a core supports recognizing that the problem itself is infeasible.This mechanism explains the aggregate repair outcomes described in the section.