FLARE¶

Note

This is the official implementation of FLARE and FLARE-NL, introduced by FLARE: Verifying MILP Reformulations with LLM-Based Formal Proof Synthesis

FLARE (Formulation-Level Automated Reformulation Evaluation) uses an LLM-based agent and the Lean proof assistant to verify mixed-integer linear program (MILP) reformulations according to the FormulationBench definition of reformulation. FLARE-NL is a Large Language Model (LLM) proxy for FLARE that trades off formal guarantees for speed and cost.

The milp-flare Python package is the official implementation of both methods. See below for installation instructions, user guides, and the API reference.

Contents

Installation
- Install the package
- Quickstart
User Guides
- Docker
- Running FLARE on FormulationBench
Agent Harnesses
Prompts
- FLARE Agent Prompt
- FLARE-NL Prompt
Agent Skills
- lean-milp-formulation
- lean-milp-reformulation
API Reference