# FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

arXiv: https://arxiv.org/abs/2012.14235 · HTML: https://mlsanity.com/paper/2012.14235/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Dec 2020.

## Built on by (most cited first, 2 of 2)

- [Generating Pragmatic Examples to Train Neural Program Synthesizers](https://mlsanity.com/paper/2311.05740/) (2023)
- [Extracting Explainable Dates From Medical Images By Reverse-Engineering UNIX Timestamps](https://mlsanity.com/paper/2505.11451/) (2025)

## Abstract (arXiv)

Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users. We present FOREST, a regular expression synthesizer for digital form validations. FOREST produces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs. We evaluated FOREST on real-world form-validation instances using regular expressions. Experimental results show that FOREST successfully returns the desired regular expression in 72% of the instances and outperforms REGEL, a state-of-the-art regular expression synthesizer.