Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917496205869056 |
|---|---|
| author | Schmitt, Frederik Cosler, Matthias Metzger, Niklas Siber, Julian Krsmanovic, Vladimir Ghanem, Mohamed Finkbeiner, Bernd |
| author_facet | Schmitt, Frederik Cosler, Matthias Metzger, Niklas Siber, Julian Krsmanovic, Vladimir Ghanem, Mohamed Finkbeiner, Bernd |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15131 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models Schmitt, Frederik Cosler, Matthias Metzger, Niklas Siber, Julian Krsmanovic, Vladimir Ghanem, Mohamed Finkbeiner, Bernd Machine Learning 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. |
| title | Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models |
| topic | Machine Learning |
| url | https://arxiv.org/abs/2605.15131 |