Observational Equivalence for MILP Formulations: Behavioral Evaluation via Sketch-and-Prove Formal Verification

Mixed-integer linear programming (MILP) formulations are widely used in scheduling, logistics, finance, and other domains. The same optimization problem can be represented by different formulations, which makes automatic correctness evaluation difficult. To evaluate formulation equivalence more appropriately, we propose a behavioral evaluation criterion for MILP formulations, which, building on the notion of observational equivalence, compares two formulations through their observable optimality outcomes under any problem parameter. We realize this criterion with a sketch-and-prove process that produces a proof certified by Lean. The process first constructs an informal plan and a formal proof sketch, and then automatically identifies the unproved goals and proves them one by one. Finally, we extend the benchmark for MILP formulation equivalence verification with nine classes of model transformations. Experiments show that our evaluation criterion overcomes key limitations of existing evaluation methods by assessing formulation correctness at the formulation level through the observable optimal outcomes. This makes the criterion suitable for the practical evaluation of both automatically optimization modelling and their subsequent transformations.