Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

• URL: http://arxiv.org/abs/2605.15131v1
• Date: Thu, 14 May 2026 17:39:58 GMT
• Title: Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
• Abstract summary: Reactive synthesis is the problem of automatically constructing a hardware circuit from a logical specification.<n>We present a neuro-symbolic approach to reactive synthesis that couples large reasoning models with model checkers.<n>On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language.
• Score: 7.768952514701895
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• MathAgent: Adversarial Evolution of Constraint Graphs for Mathematical Reasoning Data Synthesis [26.328617109421327]
  This paper proposes a hierarchical framework that formulates data synthesis as an unsupervised optimization problem.<n>We introduce a Legislator-Executor paradigm: The Legislator adversarially evolves structured generation blueprints encoding the constraints of the problem, while the Executor instantiates these specifications into diverse natural language scenarios.<n> Experiments conducted on a total of 10 models across the Qwen, Llama, Mistral, and Gemma series demonstrate that our method achieves notable results.
  arXiv  Detail & Related papers  (2026-04-13T08:48:12Z)
• CircuitSynth: Reliable Synthetic Data Generation [44.80087038178069]
  Large Language Models (LLMs) frequently suffer from hallucinations, logical inconsistencies, and mode collapse when tasked with structured generation.<n>Existing approaches, such as prompting or retrieval-augmented generation, lack the mechanisms to balance linguistic expressivity with formal guarantees regarding validity and coverage.<n>We propose Circuit Synth, a novel neuro-symbolic framework that decouples semantic reasoning from surface realization.
  arXiv  Detail & Related papers  (2026-04-11T09:18:52Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Controlled Agentic Planning & Reasoning for Mechanism Synthesis [18.8323743697237]
  This work presents a dual-agent acllm-based reasoning framework for automated planar mechanism synthesis.<n>From a natural-language task description, the system composes symbolic constraints and equations, generates and parametrises simulation code, and iteratively refines designs via critic-driven feedback.
  arXiv  Detail & Related papers  (2025-05-23T08:16:32Z)
• RV-Syn: Rational and Verifiable Mathematical Reasoning Data Synthesis based on Structured Function Library [58.404895570822184]
  RV-Syn is a novel mathematical Synthesis approach.<n>It generates graphs as solutions by combining Python-formatted functions from this library.<n>Based on the constructed graph, we achieve solution-guided logic-aware problem generation.
  arXiv  Detail & Related papers  (2025-04-29T04:42:02Z)
• The Role of Foundation Models in Neuro-Symbolic Learning and Reasoning [54.56905063752427]
  Neuro-Symbolic AI (NeSy) holds promise to ensure the safe deployment of AI systems. Existing pipelines that train the neural and symbolic components sequentially require extensive labelling. New architecture, NeSyGPT, fine-tunes a vision-language foundation model to extract symbolic features from raw data.
  arXiv  Detail & Related papers  (2024-02-02T20:33:14Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• Neural Circuit Synthesis from Specification Patterns [5.7923858184309385]
  We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications. New approaches using machine learning might open a lot of possibilities in this area, but suffer from the lack of sufficient amounts of training data. We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions.
  arXiv  Detail & Related papers  (2021-07-25T18:17:33Z)
• CounterExample Guided Neural Synthesis [12.742347465894586]
  Program synthesis is difficult and methods that provide formal guarantees suffer from scalability issues. We combine neural networks with formal reasoning to convert a logical specification into a sequence of examples that guides the neural network towards a correct solution. Our results show that the formal reasoning based guidance improves the performance of the neural network substantially.
  arXiv  Detail & Related papers  (2020-01-25T01:11:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.