SynCode is efficient (<10% overhead) and provably sound in generating syntactical LLM output for any LR(1) grammar. Currently supports built-in grammars for Python, Go, Java, JSON, SQL, first-order logic, and support for many grammars is WIP.
It would be interesting if these constraints could be extended to give even more guarantees, like type safety. Such constraints probably need some kind of backtracking.
We have added some interesting notebooks with miscellaneous grammars here: https://github.com/uiuc-focal-lab/syncode/tree/main/notebook...
The arXiv version of the paper is available here: https://arxiv.org/abs/2403.01632