Python utilities for loading and working with the FormulationBench dataset. FormulationBench is a collection of 20 optimization problems with 116 mixed-integer linear programming (MILP) formulations. Each formulation has a natural language description, LaTeX formulation, GurobiPy implementation, and Lean representation. Furthermore, there are 96 pairs of formulations consisting of 70 positive reformulation examples and 26 negative examples. Each positive example has a machine-checked Lean 4 reformulation proof. See the documentation for details.
pip install formulation-benchDownload the dataset:
from formulation_bench import Dataset
ds = Dataset.load()Access a problem's formulations:
p1 = ds.problems[1]
p1a = p1.formulations["a"]Access reformulation pairs:
pos = [r for r in ds.reformulations if r.is_reformulation]
neg = [r for r in ds.reformulations if not r.is_reformulation]See AGENTS.md for development information.
TODO: Add arXiv article citation
