LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean

• URL: http://arxiv.org/abs/2607.28459v1
• Date: Thu, 30 Jul 2026 16:21:58 GMT
• Title: LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
• Abstract summary: Constraint programming is a core technology for solving complex problems in scheduling, planning, configuration, and verification.<n>We introduce a framework that addresses both verification levels in the Lean theorem prover.<n>It can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints.
• Score: 22.962110170304594
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Constraint programming is a core technology for solving complex combinatorial problems in scheduling, planning, configuration, and verification. Trusting its results therefore demands guarantees at two levels: that reformulations applied beforehand are semantics-preserving, and that solvers produce correct answers. In this work, we introduce a framework that addresses both verification levels in the Lean theorem prover: it can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families; and to check solver-produced certificates for individual instances via translation backends to external formats such as MiniZinc, SMT-LIB, and OPB. Combining both levels yields an end-to-end workflow that establishes the satisfiability or unsatisfiability of a constraint problem without trusting the external solver. Experimental results show that our framework's verified symmetry breaking also pays off in practice: a single parametric proof per problem family, reused across all instance sizes, reduces solver search effort by a factor of up to 2x10^7, while the entire in-Lean certification stays affordable, taking at most a few minutes for our largest instances.

Related papers

• Constraint-First Reasoning: A Training-Free Protocol for Exploiting Answer-Space Constraints in Mathematical Problem Solving [11.900982999786287]
  Routed-CFR activates the two-stage protocol only when a text-only router detects restrictive cues.<n>Across AIME, CMIMC, BRUMO, and AIMO_AMC, the method improves direct CoT on multiple backbones.
  arXiv  Detail & Related papers  (2026-08-05T16:18:41Z)
• STAIF: A Stage-wise Optimization for Complex Instruction Following [50.48101504556211]
  STAIF is a stage-wise optimization framework that decouples the alignment of subjective (soft) constraints from the optimization of objectively verifiable (hard) constraints.<n>To support this method, we construct STAINSTRUCT, a high-quality bilingual (English, Chinese) dataset of approximately 31,000 complex multi-constraint instructions.
  arXiv  Detail & Related papers  (2026-06-26T06:14:07Z)
• Certified Program Synthesis with a Multi-Modal Verifier [5.998029529040967]
  LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean.<n>It combines dynamic validation, automated proofs, and interactive proof scripting in one foundational framework.<n>We evaluate LeetProof on benchmarks derived from prior work on certified synthesis.
  arXiv  Detail & Related papers  (2026-04-17T14:56:45Z)
• Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
  LLMs must invoke multiple dependent APIs in the correct order while propagating intermediate outputs.<n>Training models to handle such faces two obstacles: existing environments focus on simple per-turn function calls with simulated data, and binary rewards.<n>We present a framework addressing both challenges. First, we construct a reinforcement learning environment backed by a large-scale cache of real API responses, enabling a data synthesis pipeline that samples valid multi-step orchestration traces.<n>Second, we propose a graduated reward design that decomposes correctness into atomic validity and orchestration.
  arXiv  Detail & Related papers  (2026-03-25T18:31:39Z)
• Conformal Mixed-Integer Constraint Learning with Feasibility Guarantees [0.3058340744328236]
  Conformal Mixed-Integer Constraint Learning provides probabilistic feasibility guarantees for data-driven constraints in optimization problems.<n>We show that C-MICL consistently achieves target rates, maintains competitive objective performance, and significantly reduces computational cost compared to existing methods.
  arXiv  Detail & Related papers  (2025-06-04T03:26:31Z)
• Fully Stochastic Trust-Region Sequential Quadratic Programming for Equality-Constrained Optimization Problems [62.83783246648714]
  We propose a sequential quadratic programming algorithm (TR-StoSQP) to solve nonlinear optimization problems with objectives and deterministic equality constraints. The algorithm adaptively selects the trust-region radius and, compared to the existing line-search StoSQP schemes, allows us to utilize indefinite Hessian matrices.
  arXiv  Detail & Related papers  (2022-11-29T05:52:17Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Tensor Completion with Provable Consistency and Fairness Guarantees for Recommender Systems [5.099537069575897]
  We introduce a new consistency-based approach for defining and solving nonnegative/positive matrix and tensor completion problems. We show that a single property/constraint: preserving unit-scale consistency, guarantees the existence of both a solution and, under relatively weak support assumptions, uniqueness.
  arXiv  Detail & Related papers  (2022-04-04T19:42:46Z)
• Certified Symmetry and Dominance Breaking for Combinatorial Optimisation [13.333957453318744]
  We develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. We apply our method to maximum clique solving and constraint as a proof of concept that the approach applies to a wider range of problems.
  arXiv  Detail & Related papers  (2022-03-23T08:45:35Z)
• An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
  We introduce a divide-and-conquer based diagnosis algorithm (FastDiag) which identifies minimal sets of faulty constraints in an over-constrained problem. We compare FastDiag with the conflict-directed calculation of hitting sets and present an in-depth performance analysis.
  arXiv  Detail & Related papers  (2021-02-17T19:55:42Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  Security-constrained optimal power flow (SCOPF) is fundamental in power systems. Modeling of APR within the SCOPF problem results in complex large-scale mixed-integer programs. This paper proposes a novel approach that combines deep learning and robust optimization techniques.
  arXiv  Detail & Related papers  (2020-07-14T12:38:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.