Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

Frederik Schmitt, Matthias Cosler, Niklas Metzger, Julian Siber, Vladimir Krsmanovic, Mohamed Ghanem and Bernd Finkbeiner

Reactive synthesis is a challenging problem for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this extended abstract, we report on current advances in tackling both sides of the problem with Large Reasoning Models (LRMs). On the algorithmic side, we present a neuro-symbolic approach that couples LRMs with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmark instances than last year’s SYNTCOMP winner and extends to constructing parameterized systems. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language and introduce a 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.

15th Workshop on Synthesis July 2026
Contact Data Privacy Policy Imprint
Home People Publications
More