Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

TL;DR

This paper introduces a neuro-symbolic approach using large reasoning models to improve reactive synthesis, outperforming existing tools and enabling natural language specifications for hardware design.

Contribution

It presents a novel neuro-symbolic method combining large models with model checkers and introduces autoformalization from natural language to formal specifications.

Findings

Outperforms the best dedicated tools in benchmark tests

Extends to constructing parameterized systems, despite undecidability

Achieves performance comparable to formal specifications from natural language

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.