Source-linked AI summary

Multi-modal Synthesis of Regular Expressions

Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, Isil Dillig

arXiv:1908.03316v3cs.PL

TL;DR

Regex synthesis is difficult because natural-language descriptions are ambiguous and examples alone may not fully specify user intent. The paper combines both modalities by parsing English into hierarchical sketches that guide a programming-by-example engine, with symbolic regexes and SMT constraints for pruning. Regel solves 80% of 322 benchmarks, outperforming NLP-only and example-only baselines, while also improving user success and synthesis speed.

  • Problem

    Regex synthesis lacks a reliable single modality because natural language is ambiguous and examples may not fully convey user intent.

    Source: §1 · p. 1, §2 · p. 2
  • Method

    The method parses English into hierarchical sketches that guide a programming-by-example engine’s search and deduction.

    Source: §1 · p. 1
  • Results

    80% of 322 benchmarks were solved within four interaction steps, versus 43% for NLP-only and 26% for example-only synthesis.

    Source: §1 · p. 2, §11 · p. 13
  • Takeaways & Limitations

    Regel provides a practical multi-modal synthesis approach evaluated against multiple baselines and in a user study.

    Source: §1 · p. 2

    The user study was preliminary, involving mostly computer science students from one university and StackOverflow tasks rather than participants’ own real-world tasks.

    Source: §9.3 · p. 12

Abstract

from arXiv · show

In this paper, we propose a multi-modal synthesis technique for automatically constructing regular expressions (regexes) from a combination of examples and natural language. Using multiple modalities is useful in this context because natural language alone is often highly ambiguous, whereas examples in isolation are often not sufficient for conveying user intent. Our proposed technique first parses the English description into a so-called hierarchical sketch that guides our programming-by-example (PBE) engine. Since the hierarchical sketch captures crucial hints, the PBE engine can leverage this information to both prioritize the search as well as make useful deductions for pruning the search space. We have implemented the proposed technique in a tool called Regel and evaluate it on over three hundred regexes. Our evaluation shows that Regel achieves 80% accuracy whereas the NLP-only and PBE-only baselines achieve 43% and 26% respectively. We also compare our proposed PBE engine against an adaptation of AlphaRegex, a state-of-the-art regex synthesis tool, and show that our proposed PBE engine is an order of magnitude faster, even if we adapt the search algorithm of AlphaRegex to leverage the sketch. Finally, we conduct a user study involving 20 participants and show that users are twice as likely to successfully come up with the desired regex using Regel compared to without it.

1 Introduction

Existing regex synthesizers use either natural-language descriptions or examples, but each modality has important limitations. The paper combines both modalities through hierarchical sketches and a sketch-guided PBE engine, implemented in Regel and evaluated against multiple baselines.

1 Introduction

  • Natural-language methods have low accuracy, while example-based methods restrict the regexes they can synthesize.Reported restrictions include limited Kleene-star use or binary alphabets.Source: §1 · p. 1
  • Examples and natural language complement each other because descriptions express high-level tasks while examples clarify ambiguities.Users commonly provide both modalities when communicating regex intent.Source: §1 · p. 1
  • Regel parses English into hierarchical sketches that guide PBE search and deduction.The sketch’s compositional structure also supports semantic parsing with non-data-hungry NLP techniques.Source: §1 · p. 1
  • The PBE engine uses sketch hints to prioritize search, perform deductions, and prune candidates with symbolic regular expressions and SMT solving.These mechanisms are presented as components of the proposed regex synthesis technique.Source: §1 · pp. 1–2
  • 80% of 300+ regex benchmarks were solved by Regel, versus 43% for NLP-only and 26% for pure-PBE baselines.The benchmarks came from two different sources.Source: §1 · p. 2
  • The paper contributes a multi-modal regex synthesizer, hierarchical sketches, a new PBE engine, benchmark evaluation, and a user study.The user study evaluates Regel’s benefits with statistical significance tests.Source: §1 · p. 2

2 Overview

The overview illustrates how Regel combines ambiguous English descriptions and examples by generating hierarchical sketches and completing them with sketch-guided search. Symbolic regexes and SMT constraints further prune the search while retaining feasible completions.

2 Overview

  • The motivating decimal-regex task is ambiguous because the description confuses period with comma and does not clarify whether pure integers are allowed.Examples alone also leave uncertainty about whether digit 0 is permitted.Source: §2 · p. 2
  • A semantic parser converts the English description into a ranked list of hierarchical sketches capturing the target regex’s high-level structure.One sketch includes digit or comma components and a one-to-three-digit repetition.Source: §2 · p. 2
  • The PBE engine performs top-down sketch-guided enumerative search over partial regex ASTs, expanding unknown sketch-labeled nodes.Expansions can reduce the allowed sketch depth for newly created nodes.Source: §2 · p. 2
  • Sketch-derived over- and under-approximations let the engine reject partial regexes inconsistent with examples without compromising completeness.The approximations are more precise because they incorporate natural-language hints.Source: §2 · pp. 2–3
  • Symbolic regexes replace explicit enumeration of integer constants with SMT constraints that prune infeasible candidates.Because the constraints over-approximate regex semantics, SMT models prune candidates rather than directly determine all constants.Source: §2 · p. 3
  • The synthesis algorithm produces a correct regex with digit repetition bounded from 1 to 15 and an optional decimal suffix with digit repetition bounded from 1 to 3.Source: §2 · p. 3
  • The regex DSL includes repetition, character classes, conjunction, and negation, with k as a positive integer and c as a character class.Programs in the DSL are expressible as standard regexes, including constructs requiring automaton-level operations.Source: Figure 4 · p. 3, §2 · p. 3

3 Regex Language

The regex DSL provides character classes, containment, concatenation, logical operators, and repetition, while hierarchical sketches extend it with structured holes and symbolic integers.

  • The DSL supports character classes for individual characters and predefined families such as digits, letters, alphanumerics, and hexadecimal characters.Source: §3 · p. 3
  • Containment operators test whether a regex matches a prefix, suffix, or substring of the input.Source: §3 · p. 3
  • Concatenation requires the input to split into substrings matched by the component regexes.Source: §3 · p. 3
  • Logical operators provide negation, conjunction, disjunction, and optional matching through regex composition.Source: §3 · p. 3
  • Repetition operators express exact, bounded, at-least, and Kleene-star repetition, with positive integer bounds.Source: §3 · p. 3
  • The language is extended by hierarchical-sketch syntax whose concrete regexes and symbolic integers guide synthesis.Source: Figure 5 · p. 4, Figure 6 · p. 4

4 Hierarchical Sketches

Hierarchical sketches represent families of regexes through constrained holes, DSL operators, and symbolic repetition counts, allowing natural-language hints to constrain synthesis.

  • An h-sketch represents a family of regexes that conform to a high-level structure.Source: §4 · p. 4
  • Constrained holes require a descendant leaf to match one nested sketch within a configurable depth, and holes may be nested.Source: §4 · p. 4
  • H-sketches compose DSL operators, including repetition operators whose integer arguments are represented by positive symbolic integers.Source: §4 · p. 4
  • For example, a concatenation sketch can require one component to contain a digit or comma and another to contain a bounded digit repetition or comma.Source: §4 · p. 4
  • The explicit hole-depth parameter defines the formal semantics, while the semantic parser's sketches use a configurable search-tree depth.Source: §4 · p. 4

5 Regex Synthesis from H-Sketches

The synthesis procedure searches for regexes consistent with h-sketches and examples, prunes infeasible partial programs using approximations, and solves symbolic repetition constants with SMT.

5 Regex Synthesis from H-Sketches

  • The synthesizer maintains a worklist of partial regex ASTs, expands open h-sketch nodes, and returns a concrete regex satisfying the sketch and positive/negative examples.Source: §5 · pp. 4–5

5.1 Pruning infeasible partial regexes

  • Approximation safely rejects a partial regex when its over-approximation misses a positive example or its under-approximation matches a negative example.Source: §5.1 · p. 5
  • H-sketch hints make these over- and under-approximations more precise, while nested deep holes may use the coarse pair ⟨⊤, ⊥⟩ to limit overhead.Source: §5.1 · pp. 5–6

5.2 Solving Symbolic Regexes with SMT

  • Symbolic regexes replace explicit enumeration of repetition constants with SMT constraints derived from matched-string lengths.Source: §5.2 · pp. 6–7
  • The encoding can introduce nonlinear constraints for repetition, but the authors report that Z3 efficiently handles the generated formulas.Source: §5.2 · p. 7
  • InferConstants incrementally assigns symbolic integers from solver models, checks partial assignments for infeasibility, and retains alternatives using blocking clauses.Source: §5.2 · pp. 6–8
  • The SMT-based InferConstants procedure is correct: every concrete regex consistent with the examples appears among its returned candidates.Source: §5.2 · p. 8

6 From English Text to H-Sketches

Regel converts English descriptions into hierarchical sketches through semantic parsing, then ranks candidate derivations so a PBE engine can use the most suitable sketches. Its grammar composes sketches from lexical and compositional rules, while learned features and beam search manage ambiguity and scale.

6.1 Background on semantic parsing

  • Semantic parsing frames English-to-sketch generation as mapping ambiguous utterances to ranked hierarchical sketches rather than a single fixed interpretation.Regel uses a CFG and a machine-learning model, while remaining agnostic to the particular NLP technique used for parsing.Source: §6 · p. 8, §6.1 · p. 8

6.2 Grammar-based sketch composition

  • Lexical rules map words to DSL concepts, while compositional rules combine derivations into larger sketches with holes or concrete regex programs.The grammar distinguishes $SKETCH objects containing holes from $PROGRAM objects representing concrete regexes.Source: §6.2 · p. 8
  • Bottom-up dynamic programming applies lexical rules to spans and compositional rules to non-overlapping spans, retaining whole-sentence derivations labeled $ROOT.The parser may skip arbitrary words, and a sentence can yield multiple derivations or alternative h-sketches.Source: §6.2 · pp. 8–9

6.3 Learning feature weights

  • A discriminative log-linear model scores derivations using rule and span features, learning parameters from English descriptions paired with annotated sketches.Training maximizes the probability of generating the target sketch regardless of which derivation produces it, increasing weights for features in matching derivations.Source: §6.3 · p. 9
  • Beam search approximates the highest-scoring derivation by retaining only the top m derivations for each span instead of enumerating the exponentially large derivation set.Training normalizes likelihood over the retained beam rather than over all possible derivations.Source: §6.3 · p. 9

7 Implementation

Regel combines natural-language descriptions and labeled examples with time and output controls, then searches multiple sketch completions in parallel. Implementation heuristics reduce redundant membership queries and duplicate sketches.

7 Implementation

  • Regel accepts a description, positive and negative examples, a time budget, and a requested result count, returning up to k example-consistent regexes.Fewer than k results may be returned when the time budget expires.Source: §7 · p. 9
  • Regel uses SEMPRE for semantic parsing, Z3 for symbolic-integer inference, and Brics for regex membership checking.These components support parsing, constraint solving, and automaton-based matching respectively.Source: §7 · p. 9
  • The workflow generates up to 500 derivations, ranks them, runs 25 top sketches in parallel, and returns completed results within the user-specified budget.The system waits for up to k PBE instances to finish before returning their regexes.Source: §7 · p. 10
  • Subsumption heuristics eliminate redundant membership queries, while duplicate sketches are removed during beam search.The implementation exploits implications between operators such as StartsWith and Contains, and between RepeatAtLeast variants.Source: §7 · p. 10

8 Data Sets for Evaluation

Evaluation uses an adapted DeepRegex data set and a more challenging StackOverflow collection containing descriptions, examples, and ground-truth regexes. Training sketches and search settings differ by data-set difficulty, with stricter budgets and more displayed results for StackOverflow tasks.

8 Data Sets for Evaluation

  • The evaluation combines 200 adapted DeepRegex benchmarks with 122 harder StackOverflow regex tasks containing English descriptions and positive and negative examples.DeepRegex benchmarks average 4 positive and 5 negative examples, while StackOverflow ground truth comes from accepted answers translated into the DSL.Source: §8 · p. 10
  • Training requires English–h-sketch pairs because the original data sets lack hierarchical-sketch annotations.The selected sketch strategy balances parser usefulness against giving the PBE engine enough freedom to complete the target.Source: §8 · p. 10
  • DeepRegex training sketches replace each target regex’s root operator with a hole, whereas StackOverflow sketches are manually constructed from descriptions.Manual sketches preserve unambiguous structure and use holes for ambiguous or difficult-to-parse fragments.Source: §8 · p. 10
  • Regel uses a 10-second timeout and one displayed result for DeepRegex, versus 60 seconds and five results for StackOverflow.Tools are compared with the same t and k values, and a task counts as solved when the intended regex appears within the top k.Source: §8 · p. 10

9 Experimental Results

Across 322 regex tasks, Regel combines natural-language sketches with examples to outperform NLP-only and PBE-only baselines, while its pruning techniques improve synthesis speed and its user study shows higher success with the tool.

9.1 Benefits of multi-modal synthesis

  • Regel’s natural-language specification substantially speeds up the PBE engine, while DeepRegex has negligible running time because it performs no search.The iteration plots report solved benchmarks and average running time across DeepRegex and StackOverflow datasets.Source: §9.1 · p. 11
  • Regel solves 151 of 200 DeepRegex benchmarks initially and up to 185 with additional examples, while solving 74 of 122 StackOverflow benchmarks.The corresponding baseline results are 134 for DeepRegex and 66 for Regel-Pbe on DeepRegex, versus 3 and 18 on StackOverflow.Source: §9.1 · p. 11
  • 80% of 322 benchmarks are solved by Regel, compared with 43% for DeepRegex and 26% for the PBE baseline.This comparison evaluates multi-modal synthesis against natural-language-only and example-only approaches.Source: §9.1 · p. 11

9.2 Evaluation of PBE engine

  • For the first 1000 sketches solved by all variants, Regel is around 10× faster than AlphaRegex and 2.5× faster than Regel-Approx.Regel-Approx omits symbolic regexes, while the full system combines sketch-guided pruning with symbolic-regex reasoning.Source: §9.2 · pp. 11–12

9.3 User study

  • In the user study, correct solutions increased from 28.3% without Regel to 73.3% with it, with p < 0.0000001.The study involved 20 participants solving StackOverflow-derived tasks under both conditions.Source: §9.3 · p. 12
  • Failures arose when Regel timed out or when ambiguous StackOverflow posts supported multiple interpretations, while the study used mostly students and non-personal tasks.The authors characterize the user-study evidence as preliminary rather than a study of use in the wild.Source: §9.3 · p. 12

10 Related Work

Prior regex synthesis spans example-based learning, natural-language translation, and multimodal sketching, but existing approaches differ in their inputs, search strategies, and target domains.

Learning regexes from examples

  • Example-based regex learners can require far more queries than Regel-Pbe, with L∗ needing 679 queries versus 8 examples for [A-Za-z]+.Source: §10 · p. 12
  • AlphaRegex performs top-down search with approximations but is limited to binary alphabets and does not use natural language.Regel instead combines hierarchical-sketch guidance, symbolic regexes, and SMT-based reasoning for pruning.Source: §10 · p. 13

Learning regexes from language

  • Natural-language regex systems translate descriptions directly, whereas Regel first produces a hierarchical sketch and then synthesizes from examples.Source: §10 · p. 13

Multi-modal synthesis

  • Other multimodal systems use probabilistic version spaces, concept-specific examples, generic sketch completion, or MaxSMT constraints, often targeting broader string programs or data wrangling.Source: §10 · p. 13

PBE and sketching

  • Regel’s sketches differ from prior sketching methods because their holes represent arbitrary regexes and constraint solving rules out infeasible integer constants.Source: §10 · p. 13

11 Conclusions and Future Work

Regel synthesizes regexes by combining natural-language sketches with examples, achieving strong benchmark performance and faster PBE search than AlphaRegex. Future work targets interactive disambiguation, better parser feedback, and applications beyond regexes.

  • 80% of 322 benchmarks were solved within four user interaction steps, compared with 43% for NLP-only and 26% for example-only synthesis.Source: §11 · p. 13
  • Regel’s PBE engine was an order of magnitude faster than AlphaRegex, a state-of-the-art regex synthesis tool.Source: §11 · p. 13
  • Future work includes active learning that asks membership queries to distinguish multiple regexes consistent with the examples.Source: §11 · p. 13
  • The authors also plan improved semantic parsing for feedback when sketches are too coarse and applications beyond regular expressions.Source: §11 · p. 13

A Proofs

The appendix formalizes regex and h-sketch semantics, proves approximation and constant-inference correctness, and establishes that the synthesis procedures preserve feasible solutions while pruning the search.

A Proofs

  • Approximate constructs an over-approximation and under-approximation for h-sketches and partial regexes, with correctness proved by structural induction.Source: A Proofs · pp. 15–16
  • The approximation proof extends across negation, standard combinators, and symbolic repetition operators while preserving the required matching bounds.Source: A Proofs · pp. 15–16
  • InferConstants is complete for concrete regexes consistent with positive and negative examples, because its worklist exhausts feasible symbolic-integer assignments.Source: A Proofs · pp. 16–17
  • The proofs establish soundness and coverage of the symbolic search, including termination when the finite assignment space has been exhausted.Source: A Proofs · pp. 16–17
  • The Encode procedure is correct: any matching concrete instantiation yields a satisfying assignment for the generated length constraint.Source: A Proofs · p. 17

B Semantics for the Regex DSL

  • The regex DSL defines matching semantics for character classes, substring operators, negation, optionality, concatenation, Boolean combinations, and repetition.Source: B Semantics for the Regex DSL · p. 17

C DeepRegex Data Set Details and Benchmark Collection Procedure

The evaluation uses cleaned DeepRegex and StackOverflow benchmarks, trains the semantic parser separately for each source, and tests Regel through an interactive user study.

C DeepRegex Data Set Details and Benchmark Collection Procedure

  • The adapted DeepRegex collection contains 200 benchmarks with descriptions, target regexes, and 4–14 positive or negative examples after removing noise and inconsistencies.The original dataset had 10,000 generated benchmarks, including noisy paraphrases and approximately 1,400 empty-language regexes.Source: C DeepRegex Data Set Details and… · pp. 17–18

D StackOverflow Data Set Details and Benchmark Collection Procedure

  • The StackOverflow dataset contains 122 consistent benchmarks covering tasks such as number matching, phone-number matching, and password validation.Posts were cleaned by removing irrelevant attempted solutions, fixing typos, and handling visually formatted constraints.Source: D StackOverflow Data Set Details and… · p. 18
  • Ground-truth regexes were represented in the paper’s DSL to enable equivalence checking with the Automaton library.Source: D StackOverflow Data Set Details and… · p. 18

E Training for Each Data Set

  • DeepRegex sketch labels were generated from target regexes, whereas StackOverflow labels were manually written and trained with five-fold cross-validation.Source: E Training for Each Data Set · p. 18

F User Study Procedure

  • In the user study, participants solved three tasks with Regel and three without it, with task order randomized to reduce knowledge-transfer effects.Source: F User Study Procedure · p. 18
  • With Regel, users received three synthesized candidates and could add two examples repeatedly; without Regel, they could consult the cheat-sheet and other resources.Source: F User Study Procedure · pp. 18–19
Loading 1908.03316v3…