Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
For researchers and practitioners in formal verification, this work provides a practical method that outperforms existing tools on standard benchmarks and simplifies specification writing by using natural language.
The paper introduces a neuro-symbolic approach to reactive synthesis that uses large reasoning models and model checkers to iteratively repair Verilog implementations, solving more benchmarks than the best dedicated tools and extending to parameterized systems. It also introduces an autoformalization step that allows specifications in natural language, achieving performance comparable to formal specifications.
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.