Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

Problem
This paper addresses the dual challenges in reactive synthesis: the algorithmic complexity of constructing hardware circuits from logical specifications and the difficulty of manually writing formal specifications. The authors propose a novel approach that integrates large reasoning models with model checkers to enhance the synthesis process. This work is presented as a preprint and has not yet undergone peer review.

Method
The authors introduce a neuro-symbolic framework that combines large language models (LLMs) with traditional model checking techniques. The architecture involves an iterative feedback loop where the LLM generates Verilog implementations based on natural language specifications, which are then refined using symbolic reasoning. The model checkers provide sound feedback to iteratively repair the generated circuits. Additionally, the authors propose an autoformalization step that translates natural language specifications into a format suitable for synthesis, utilizing a hand-authored dataset of natural-language specifications. The training compute details are not disclosed, but the approach leverages the capabilities of large reasoning models to enhance the synthesis process.

Results
The proposed method outperforms existing dedicated reactive synthesis tools in the annual synthesis competition, solving a greater number of benchmarks. Specifically, the authors report a significant improvement in the number of successfully synthesized circuits compared to state-of-the-art tools, although exact performance metrics (e.g., percentage improvement or specific benchmark names) are not provided in the abstract. The method also demonstrates the ability to handle parameterized systems, a problem typically considered undecidable, showcasing its robustness and versatility.

Limitations
The authors acknowledge that their approach may be limited by the quality and coverage of the hand-authored dataset used for natural language specifications. Additionally, the reliance on large reasoning models may introduce challenges related to model interpretability and the potential for generating incorrect or suboptimal Verilog implementations. The paper does not address the computational overhead associated with the iterative feedback process or the scalability of the approach to larger, more complex specifications.

Why it matters
This work has significant implications for the field of formal verification and hardware design automation. By demonstrating that large reasoning models can effectively bridge the gap between natural language and formal specifications, the authors pave the way for more accessible and efficient reactive synthesis workflows. This could lead to broader adoption of formal methods in industry, as it reduces the barrier to entry for engineers who may not be proficient in temporal logic. Furthermore, the ability to tackle undecidable problems in a practical manner opens new avenues for research in automated reasoning and synthesis.

Authors: Frederik Schmitt, Matthias Cosler, Niklas Metzger, Julian Siber, Vladimir Krsmanovic, Mohamed Ghanem, Bernd Finkbeiner
Source: arXiv:2605.15131
URL: https://arxiv.org/abs/2605.15131v1