# Iterative Circuit Repair Against Formal Specifications

arXiv: https://arxiv.org/abs/2303.01158 · HTML: https://mlsanity.com/paper/2303.01158/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Placed in Circuits and mechanistic analysis, one of 13 directions in Mechanistic interpretability.
- Builds on 11 of its 41 references that are in the map.
- First posted on arXiv 2 Mar 2023.

## Placed in

- Mechanistic interpretability / [Circuits and mechanistic analysis](https://mlsanity.com/mechinterp/circuits-and-mechanistic-analysis/)

## Builds on (most cited first, 11 of 11)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [BoSy: An Experimentation Framework for Bounded Synthesis](https://mlsanity.com/paper/1803.09566/) (2018)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)
- [Visual Analysis of Hyperproperties for Understanding Model Checking Results](https://mlsanity.com/paper/2108.03698/) (2021)
- [OCTAL: Graph Representation Learning for LTL Model Checking](https://mlsanity.com/paper/2207.11649/) (2022)
- [Explainable Reactive Synthesis](https://mlsanity.com/paper/2012.14582/) (2020)

## Built on by (most cited first, 9 of 9)

- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software](https://mlsanity.com/paper/2411.13269/) (2024)
- [Learning Better Representations From Less Data For Propositional Satisfiability](https://mlsanity.com/paper/2402.08365/) (2024)
- [Learning Representations Through Contrastive Neural Model Checking](https://mlsanity.com/paper/2510.01853/) (2025)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)
- [Translating Natural Language to Strategic Temporal Specifications via LLMs](https://mlsanity.com/paper/2606.30441/) (2026)

## Abstract (arXiv)

We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by 6.8 percentage points on held-out instances and 11.8 percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.