Kleene 1 · 9M · B16 · T128 (kleene1-9m-b16-t128)

Kleene is a graph-to-sequence model that generates a simple regular expression (regex) for a deterministic finite automaton (DFA).

Converting an automaton into a regex is a classic problem. The standard method, state elimination, always gives a correct result, but the regex it produces can grow exponentially with the number of states and become very hard to read. Kleene was built to address this in RegexSolver, an open-source engine for set operations on regular languages. RegexSolver checks the model's regex against the automaton, then keeps either the model's regex or the one from state elimination, whichever is simpler.

The model is named after Stephen Kleene (1909–1994), the mathematician who invented regular expressions and showed that they describe exactly the languages recognized by finite automata.

This card describes release v1.3; the changelog lists the changes between releases.

Example

This DFA from the test set accepts the strings over a–e, g and h that end with hb or hbh (accepting states have a double circle; the rejecting sink state is not drawn):

State elimination converts it into this regex:

[a-eg]*h(b(hb)*(h{2}|([a-eg]|h[ac-eg])[a-eg]*h)|([ac-eg][a-eg]*)?h)*b(hb)*h?

With greedy decoding, which picks the most likely token at each step, the model generates this one:

[a-egh]*hbh?

The first regex has a cognitive complexity of 44.0 and the second 5.0. Cognitive complexity is the readability measure that RegexSolver and the model rely on; it is defined below. The example was chosen to illustrate the model, and the results show how often it succeeds.

How to use

The model runs in Rust with candle, through RegexSolver's neural-synthesis feature. The neural-synthesis-hub feature also lets RegexSolver download it from the Hugging Face Hub:

use regexsolver::neural_synthesis::{Device, NeuralSynthesizer};

// From the Hub, pinned to a release (`from_hub` loads the latest one)...
let synthesizer = NeuralSynthesizer::from_hub_revision("alexvbrdn/kleene1-9m-b16-t128", "v1.3", Device::best_available())?;
// ...or from this repository's files.
let synthesizer = NeuralSynthesizer::from_files("config.json", "model.safetensors", Device::Cpu)?;

let regex = automaton.to_regex_with(&synthesizer)?;

RegexSolver determinizes and minimizes the automaton before giving it to the model. By default, it then decodes 8 candidates (greedy decoding plus 7 samples) and keeps the simplest correct one, which this card calls best of 8. With with_candidates(1), it uses greedy decoding only.

When the model finds no correct regex, or when the DFA exceeds the model's limits, RegexSolver splits the DFA into smaller pieces and runs the model on each of them. This decomposition can take a few seconds on the CPU for automata with dozens of states, and with_decomposition(false) turns it off. GPU and faster CPU backends are available as neural-synthesis-* features.

Model

In the name, kleene1 is the generation (input encoding, vocabulary and file format), 9m the number of parameters, b16 the maximum number of bases, and t128 the maximum number of decoder positions (126 regex tokens, plus a start and an end token).

As in RegexSolver, the transitions of a DFA are labelled with bases: disjoint character ranges, of which each transition covers one or more (why this representation). The model works on bases rather than on individual characters.

The input is the minimal DFA in canonical form, as a graph with one node per state and one edge per transition and base. The output is a regex in prefix-order tokens, where each character class is a set of bases. The inputs section of config.json documents the encoding.

Training

The training code and dataset are not published.

Data. The dataset contains 2,032,778 synthetic minimal DFAs with up to 16 states and 16 bases: 1,992,807 for training, 20,039 for validation and 19,932 for testing. They were generated from random regexes (49%), random automata (25%) and set operations (26%), then deduplicated and balanced over the number of states, bases and accepting states. Each DFA's target is the simplest regex found for it within 126 tokens, by cognitive complexity. The 413,058 DFAs for which no such regex was found, which are larger on average, form a separate seed pool.

Supervised training. The model is trained with cross-entropy on the target tokens, using AdamW (Loshchilov and Hutter, 2019) with a batch size of 256, and a peak learning rate of 4e-4 when training from scratch and of 1e-4 to 2e-4 when fine-tuning. Training proceeds in rounds. Between rounds, the model's own correct regexes replace targets when they are simpler (mining) and give targets to seed-pool DFAs (seeding), a form of expert iteration, in which a model is retrained on its own outputs that pass a check (Polu et al., 2022). Every new target is checked against its DFA.

Reinforcement learning. The model is then fine-tuned with group relative policy optimization (GRPO, Shao et al., 2024), with rewards computed by checking each regex rather than by a learned reward model. For each training DFA, it samples 8 regexes; a wrong regex gets a reward of 0, and a correct one 1 plus its relative complexity gain over the target. The model learns to favour the regexes that score above their group's average, with a KL penalty keeping it close to its starting point.

Compute. About 33 hours on a single NVIDIA RTX PRO 4000 Blackwell GPU for training, mining and evaluation, and about 18 hours on a laptop with an Intel Core Ultra 7 258V CPU to prepare the data.

Results

The results below are for release v1.3, on the 19,932 test DFAs, which were never seen in training.

Correctness is the share of DFAs for which the model's regex describes exactly the DFA's language: 81.8% with greedy decoding and 88.8% with best of 8. It decreases as DFAs get larger:

The 1- and 2-state rows are nearly empty because almost all such DFAs are in the training set.

Simplicity is measured by cognitive complexity, as defined by RegexSolver (implementation). It does not depend on which characters a regex uses, and is computed as follows:

• a character class costs 1, and a concatenation the sum of its parts;
• an alternation costs the sum of its branches, read one level deeper, plus 1 + depth for each branch after the first;
• a quantifier costs its operand plus a weight times 1 + depth: 0.5 for ?, * and +, 1 for {n}, 1.5 for {n,} and 2 for {m,n}. A quantified group is read one level deeper, and a quantifier containing another one costs an extra 1 + depth.

On the DFAs it solves with greedy decoding, the model's median complexity is 14.5, against 29.0 for state elimination; the larger state elimination's regex, the larger the gap.

In RegexSolver, which keeps either the model's regex or the one from state elimination, whichever is simpler, the output is simpler than state elimination's for 66% of the test DFAs with greedy decoding and for 73% with best of 8. Its mean complexity drops from 72.6 to 46.2 and 41.2 respectively. These figures only count the model's regex for the whole DFA; decomposition, which is enabled by default, can make the output simpler still.

Limitations

• About 1 DFA in 9 gets no correct regex from the model, even with best of 8.
• DFAs with many bases are harder: with 13 to 16 bases, 41% are solved with greedy decoding and 51% with best of 8, because few of them have a known regex short enough to train on. For the same reason, DFAs with no known regex within 126 tokens, about 1 in 6 of those generated, are not in the test set, and the model's accuracy on them is unknown.
• The model was trained on synthetic DFAs; automata from real workloads may differ.

Changelog

Correctness is measured on the same test DFAs for every release, and given as greedy decoding / best of 8. Simplicity is compared with the previous release, on the DFAs that both releases solve with greedy decoding.

• v1.3: adds a reinforcement learning stage (GRPO). Correctness 81.8% / 88.8%. About as simple as v1.2 (simpler for 6.4% of the DFAs, more complex for 4.5%).
• v1.2: canonical order for alternations, simplified targets, mining and seeding with beam search. Correctness 76.0% / 85.5%. Simpler than v1.1 for 12.1% of the DFAs, more complex for 1.9%.
• v1.1: targets recomputed with RegexSolver 1.1.0's state elimination. Correctness 72.9% / 83.2%. Simpler than v1.0 for 3.4% of the DFAs, more complex for 1.1%.
• v1.0: first release. Correctness 72.7% / 83.1%.

Citation

@misc{vanbeurden2026kleene1,
  author       = {van Beurden, Alexandre},
  title        = {Kleene 1: a graph-to-sequence model for simple regular expressions from DFAs},
  year         = {2026},
  howpublished = {\url{https://huggingface.co/alexvbrdn/kleene1-9m-b16-t128}}
}