From LLM Suggestions to Lean Proofs: Verified Redundant Constraints for MiniZinc

Abstract

The performance of constraint models strongly depends on the formulation used. Redundant constraints, which are logically implied by the model, can strengthen propagation and speed up solving, but finding effective ones requires substantial expertise. Recent work has shown that Large Language Models (LLMs) can generate performance-improving constraints for MiniZinc models. However, such approaches offer no soundness guarantees and the generated constraints may exclude optimal solutions or render instances infeasible. We present a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification. At its core is a novel formalization of a supported MiniZinc subset for verifying redundancy of a constraint schema over all instances by translating MiniZinc models to Lean 4 theorems. We handle MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model. We evaluate the approach on three constraint optimization problems from the literature, starting from published expert-crafted models. The augmented models show a clear improvement on one problem, improved MiniZinc Challenge scores with metric trade-offs on another, and small but non-significant changes on the third.