Abstract: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.
| Subjects: | Machine Learning (cs.LG) |
| Cite as: | arXiv:2605.15131 [cs.LG] |
| (or arXiv:2605.15131v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2605.15131 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Frederik Schmitt [view email]
[v1]
Thu, 14 May 2026 17:39:58 UTC (33 KB)