Note

FormulationBench was introduced by FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

FormulationBench is a dataset of 20 optimization problems (see Problems) with 109 MILP formulations. Each formulation includes a description, LaTeX formulation, GurobiPy code, and Lean encoding.

The dataset also includes 89 reformulation pairs (63 positive and 26 negative examples), with a machine-checked Lean 4 reformulation proof for every positive pair.

The formulation-bench Python package is the ideal interface for working with the dataset. See below for installation instructions, user guides, and the API reference.

Contents

• Installation
• User Guides
• Problems
• Dataset Schema
• Definitions
• API Reference
• Citations