Formal Optimisation Python MIT

savanty

savanty investigates whether natural language can reliably interface with mathematical solvers. It implements a pipeline from English problem descriptions to formally provable solutions, studying the gap between human intent and mathematical guarantees that pure LLM output cannot provide.

Technologies

Primary use case

Describe optimisation problems in English and get mathematically guaranteed solutions from a formal solver.

How it compares

savanty is one option in a category that includes Z3, OR-Tools, MiniZinc, Gurobi , and NL-to-constraint research. Our Compare page has the full side-by-side.