arXiv subjects

Frederik Schmitt

Publications and source records attributed to Frederik Schmitt.

11 recordsLinked to original sources

arXiv2026

Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models

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.

cs.LG↗

arXiv2024

Learning Better Representations From Less Data For Propositional Satisfiability

Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifiers to ensure output correctness. In this paper, we present NeuRes, a neuro-symbolic approach to address both challenges for propositional satisfiability, being the quintessential NP-complete problem. By combining certificate-driven training and expert iteration, our model learns better representations than models trained for classification only, with a much higher data efficiency -- requiring orders of magnitude less training data. NeuRes employs propositional resolution as a proof system to generate proofs of unsatisfiability and to accelerate the process of finding satisfying truth assignments, exploring both possibilities in parallel. To realize this, we propose an attention-based architecture that autoregressively selects pairs of clauses from a dynamic formula embedding to derive new clauses. Furthermore, we employ expert iteration whereby model-generated proofs progressively replace longer teacher proofs as the new ground truth. This enables our model to reduce a dataset of proofs generated by an advanced solver by ~32% after training on it with no extra guidance. This shows that NeuRes is not limited by the optimality of the teacher algorithm owing to its self-improving workflow. We show that our model achieves far better performance than NeuroSAT in terms of both correctly classified and proven instances.

cs.LG↗

arXiv2024

Precise Control of Process Parameters for >23% Efficiency Perovskite Solar Cells in Ambient Air Using an Automated Device Acceleration Platform

Achieving high-performance perovskite photovoltaics, especially in ambient air relies heavily on optimizing process parameters. However, traditional manual methods often struggle to effectively control the key variables. This inherent challenge requires a paradigm shift toward automated platforms capable of precise and reproducible experiments. Herein, we use a fully automated device acceleration platform (DAP) to optimize the process parameters for preparing full perovskite devices using a two-step method in ambient air. Eight process parameters that have the potential to significantly influence device performance are systematically optimized. Specifically, we delve into the impact of the dispense speed of organic ammonium halide, a parameter that is difficult to control manually, on both perovskite film and device performance. Through the targeted design of experiments, we reveal that the dispense speed significantly affects device performance primarily by adjusting the residual PbI2 content in the films. We find that moderate dispense speeds, e.g., 50 μl/s, contribute to top-performance devices. Conversely, too fast or too slow speeds result in devices with relatively poorer performance and lower reproducibility. The optimized parameter set enables us to establish a Standard Operation Procedure (SOP) for additive-free perovskite processing under ambient conditions, which yield devices with efficiencies surpassing 23%, satisfactory reproducibility, and state-of-the-art photo-thermal stability. This research underscores the importance of understanding the causality of process parameters in enhancing perovskite photovoltaic performance. Furthermore, our study highlights the pivotal role of automated platforms in discovering innovative workflows and accelerating the development of high-performing perovskite photovoltaic technologies.

physics.app-ph↗

arXiv2024

NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis

We introduce NeuroSynt, a neuro-symbolic portfolio solver framework for reactive synthesis. At the core of the solver lies a seamless integration of neural and symbolic approaches to solving the reactive synthesis problem. To ensure soundness, the neural engine is coupled with model checkers verifying the predictions of the underlying neural models. The open-source implementation of NeuroSynt provides an integration framework for reactive synthesis in which new neural and state-of-the-art symbolic approaches can be seamlessly integrated. Extensive experiments demonstrate its efficacy in handling challenging specifications, enhancing the state-of-the-art reactive synthesis solvers, with NeuroSynt contributing novel solves in the current SYNTCOMP benchmarks.

cs.LO↗

arXiv2023

Autonomous Optimization of an Organic Solar Cell in a 4-dimensional Parameter Space

Optimizing solution-processed organic solar cells is a complex task due to the vast parameter space in organic photovoltaics (OPV). Classical Edisonian or one-variable-at-a-time (OVAT) optimization approaches are laborious, time-consuming, and may not find the optimal parameter set in multidimensional design spaces. To tackle this problem, we demonstrate here for the first time artificial intelligence (AI) guided closed-loop autonomous optimization for fully functional organic solar cells. We empower our LineOne, an automated materials and device acceleration platform with a Bayesian Optimizer (BO) to enable autonomous operation for solving complex optimization problems without human interference. The system is able to fabricate and characterize complete OPV devices and navigate efficiently through the design space spanned by composition and processing parameters. In addition, a Gaussian Progress Regression (GPR) based early prediction model is employed to predict the efficiency of the cells from cheap proxy measurements, in our case, thin film absorption spectra, which are analyzed using a spectral model based on physical properties to generate microstructure features as input for the GPR. We demonstrate our generic and complete autonomous approach by optimizing composition and processing conditions of a ternary OPV system (PM6:Y12:PC70BM) in a four-dimensional parameter space. We identify the best parameter set for our system and obtain a precise objective function over the whole parameter space with a minimal number of samples. We demonstrate autonomous optimization of a complex opto-electronic device within 40 samples only, whereas an Edisonian approach would have required about 1000 samples. This raises an important discussion on the necessity of autonomous platforms to accelerate Material science.

cond-mat.mtrl-sci↗

arXiv2023

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present nl2spec, a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend.

cs.LO↗

arXiv2023

Iterative Circuit Repair Against Formal Specifications

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.

cs.LG↗

arXiv2022

Formal Specifications from Natural Language

We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language to generalize, e.g., to new variable names or operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the-art for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.

cs.SE↗

arXiv2022

Attention Flows for General Transformers

In this paper, we study the computation of how much an input token in a Transformer model influences its prediction. We formalize a method to construct a flow network out of the attention values of encoder-only Transformer models and extend it to general Transformer architectures including an auto-regressive decoder. We show that running a maxflow algorithm on the flow network construction yields Shapley values, which determine the impact of a player in cooperative game theory. By interpreting the input tokens in the flow network as players, we can compute their influence on the total attention flow leading to the decoder's decision. Additionally, we provide a library that computes and visualizes the attention flow of arbitrary Transformer models. We show the usefulness of our implementation on various models trained on natural language processing and reasoning tasks.

cs.LG↗

arXiv2021

Neural Circuit Synthesis from Specification Patterns

We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic (LTL). The LTL synthesis problem is a well-known algorithmic challenge with a long history and an annual competition is organized to track the improvement of algorithms and tooling over time. 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. In this paper, we consider a method to generate large amounts of additional training data, i.e., pairs of specifications and circuits implementing them. We ensure that this synthetic data is sufficiently close to human-written specifications by mining common patterns from the specifications used in the synthesis competitions. We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions, and even out-of-distribution examples from a recent case study.

cs.LG↗

arXiv2021

Teaching Temporal Logics to Neural Networks

We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.

cs.LO↗