# Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 25 of its 55 references that are in the map.
- First posted on arXiv 14 May 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 25 of 25)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [VeriGen: A Large Language Model for Verilog Code Generation](https://mlsanity.com/paper/2308.00708/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [Grounding Complex Natural Language Commands for Temporal Tasks in Unseen Environments](https://mlsanity.com/paper/2302.11649/) (2023)
- [QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation](https://mlsanity.com/paper/2505.24183/) (2025)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [From Spot 2.0 to Spot 2.10: What's New?](https://mlsanity.com/paper/2206.11366/) (2022)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [DeepGate4: Efficient and Effective Representation Learning for Circuit Design at Scale](https://mlsanity.com/paper/2502.01681/) (2025)
- [Retrieval-Guided Reinforcement Learning for Boolean Circuit Minimization](https://mlsanity.com/paper/2401.12205/) (2024)
- [Fuzzing Hardware Like Software](https://mlsanity.com/paper/2102.02308/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [VerifyThisBench: Generating Code, Specifications, and Proofs All at Once](https://mlsanity.com/paper/2505.19271/) (2025)
- [BoSy: An Experimentation Framework for Bounded Synthesis](https://mlsanity.com/paper/1803.09566/) (2018)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control](https://mlsanity.com/paper/2406.07400/) (2024)
- [Grammar-Forced Translation of Natural Language to Temporal Logic using LLMs](https://mlsanity.com/paper/2512.16814/) (2025)
- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Parameterized Synthesis](https://mlsanity.com/paper/1401.3588/) (2014)
- [The Temporal Logic Synthesis Format TLSF v1.2](https://mlsanity.com/paper/2303.03839/) (2023)

## Abstract (arXiv)

Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this paper, we tackle both sides of the problem. For the algorithmic side, we present a neuro-symbolic approach to reactive synthesis that couples large reasoning models with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmarks than the best dedicated tools in the annual synthesis competition and extends to constructing parameterized systems, a problem known to be undecidable. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language by introducing a hand-authored dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.