arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Daniel Neider

92 papers · 2010–2026

2010: 12011: 02012: 22013: 42014: 12015: 22016: 32017: 32018: 52019: 52020: 112021: 72022: 92023: 92024: 72025: 152026: 8
2010peak 15 in 20252026

Frequent co-authors

Papers

showing 1–25 of 92 RSS

Learning invariants using decision trees and implication counterexamples

Pranav Garg, Daniel Neider, P. Madhusudan +1 more

Artificial Intelligence · · cited 165× · DOI ↗ · more like this ·

Inductive invariants can be robustly synthesized using a learning model where the teacher is a program verifier who instructs the learner through concrete program configurations, classified as positive, negative, and implications. We propose the first learning algorithms in this model with implication counter-examples that are based on machine learning techniques. In particular, we extend classical decision-tree learning algorithms in machine learning to handle implication samples, building new scalable ways to construct small decision trees using statistical measures. We also develop a decision-tree learning algorithm in this model that is guaranteed to converge to the right concept (invariant) if one exists. We implement the learners and an appropriate teacher, and show that the resulting invariant synthesis is efficient and convergent for a large suite of programs.

Learning Linear Temporal Properties

Daniel Neider, Ivan Gavran

cs.LO · · cited 135× · arXiv ↗ · more like this ·

We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiability problems in propositional Boolean logic and produces a smallest LTL formula (in terms of the number of subformulas) that is consistent with the given data. Our second learning algorithm, on the other hand, combines the SAT-based learning algorithm with classical algorithms for learning decision trees. The result is a learning algorithm that scales to real-world scenarios with hundreds of examples, but can no longer guarantee to produce minimal consistent LTL formulas. We compare both learning algorithms and demonstrate their performance on a wide range of synthetic benchmarks. Additionally, we illustrate their usefulness on the task of understanding executions of a leader election protocol.

Joint Inference of Reward Machines and Policies for Reinforcement Learning

Zhe Xu, Ivan Gavran, Yousef Ahmad +4 more

cs.AI · · cited 113× · arXiv ↗ · more like this ·

Incorporating high-level knowledge is an effective way to expedite reinforcement learning (RL), especially for complex tasks with sparse rewards. We investigate an RL problem where the high-level knowledge is in the form of reward machines, i.e., a type of Mealy machine that encodes the reward functions. We focus on a setting in which this knowledge is a priori not available to the learning agent. We develop an iterative algorithm that performs joint inference of reward machines and policies for RL (more specifically, q-learning). In each iteration, the algorithm maintains a hypothesis reward machine and a sample of RL episodes. It derives q-functions from the current hypothesis reward machine, and performs RL to update the q-functions. While performing RL, the algorithm updates the sample by adding RL episodes along which the obtained rewards are inconsistent with the rewards based on…

Horn-ICE Learning for Synthesizing Invariants and Contracts

Deepak D'Souza, P. Ezudheen, Pranav Garg +2 more

cs.LO · · cited 75× · arXiv ↗ · more like this ·

We design learning algorithms for synthesizing invariants using Horn implication counterexamples (Horn-ICE), extending the ICE-learning model. In particular, we describe a decision-tree learning algorithm that learns from Horn-ICE samples, works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples. Since most verification proofs can be modeled using Horn clauses, Horn-ICE learning is a more robust technique to learn inductive annotations that prove programs correct. Our experiments show that an implementation of our algorithm is able to learn adequate inductive invariants and contracts efficiently for a variety of sequential and concurrent programs.

Learning to Break Deep Perceptual Hashing: The Use Case NeuralHash

Lukas Struppek, Dominik Hintersdorf, Daniel Neider +1 more

cs.LG · · cited 74× · arXiv ↗ · more like this ·

Apple recently revealed its deep perceptual hashing system NeuralHash to detect child sexual abuse material (CSAM) on user devices before files are uploaded to its iCloud service. Public criticism quickly arose regarding the protection of user privacy and the system's reliability. In this paper, we present the first comprehensive empirical analysis of deep perceptual hashing based on NeuralHash. Specifically, we show that current deep perceptual hashing may not be robust. An adversary can manipulate the hash values by applying slight changes in images, either induced by gradient-based approaches or simply by performing standard image transformations, forcing or preventing hash collisions. Such attacks permit malicious actors easily to exploit the detection system: from hiding abusive material to framing innocent users, everything is possible. Moreover, using the hash values, inferences…

Learning Universally Quantified Invariants of Linear Data Structures

Pranav Garg, Christof Loding, P. Madhusudan +1 more

cs.PL · · cited 42× · arXiv ↗ · more like this ·

We propose a new automaton model, called quantified data automata over words, that can model quantified invariants over linear data structures, and build poly-time active learning algorithms for them, where the learner is allowed to query the teacher with membership and equivalence queries. In order to express invariants in decidable logics, we invent a decidable subclass of QDAs, called elastic QDAs, and prove that every QDA has a unique minimally-over-approximating elastic QDA. We then give an application of these theoretically sound and efficient active learning algorithms in a passive learning framework and show that we can efficiently learn quantified linear data structure invariants from samples obtained from dynamic runs for a large class of programs.

Reinforcement Learning with Stochastic Reward Machines

Jan Corazza, Ivan Gavran, Daniel Neider

cs.LG · · cited 40× · arXiv ↗ · more like this ·

Reward machines are an established tool for dealing with reinforcement learning problems in which rewards are sparse and depend on complex sequences of actions. However, existing algorithms for learning reward machines assume an overly idealized setting where rewards have to be free of noise. To overcome this practical limitation, we introduce a novel type of reward machines, called stochastic reward machines, and an algorithm for learning them. Our algorithm, based on constraint solving, learns minimal stochastic reward machines from the explorations of a reinforcement learning agent. This algorithm can easily be paired with existing reinforcement learning algorithms for reward machines and guarantees to converge to an optimal policy in the limit. We demonstrate the effectiveness of our algorithm in two case studies and show that it outperforms both existing methods and a naive…

Neuro-Symbolic Verification of Deep Neural Networks

Xuan Xie, Kristian Kersting, Daniel Neider

cs.AI · · cited 28× · arXiv ↗ · more like this ·

Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g., "an autonomous vehicle has to stop in front of a stop sign") remain outside the scope of existing verification technology. To mitigate this severe practical restriction, we introduce a novel framework for verifying neural networks, named neuro-symbolic verification. The key idea is to use neural networks as part of the otherwise logical specification, enabling the verification of a wide variety of complex, real-world properties, including the one above. Moreover, we demonstrate how neuro-symbolic…

Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow +1 more

cs.AI · · cited 28× · arXiv ↗ · more like this ·

Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.

Deep Anomaly Detection on Tennessee Eastman Process Data

Fabian Hartung, Billy Joe Franks, Tobias Michels +15 more

cs.LG · · cited 27× · arXiv ↗ · more like this ·

This paper provides the first comprehensive evaluation and analysis of modern (deep-learning) unsupervised anomaly detection methods for chemical process data. We focus on the Tennessee Eastman process dataset, which has been a standard litmus test to benchmark anomaly detection methods for nearly three decades. Our extensive study will facilitate choosing appropriate anomaly detection methods in industrial applications.

Advice-Guided Reinforcement Learning in a non-Markovian Environment

Daniel Neider, Jean-Raphaël Gaglione, Ivan Gavran +3 more

Artificial Intelligence · Proceedings of the AAAI Conference on Artificial Intelligence · · cited 25× · DOI ↗ · more like this ·

We study a class of reinforcement learning tasks in which the agent receives its reward for complex, temporally-extended behaviors sparsely. For such tasks, the problem is how to augment the state-space so as to make the reward function Markovian in an efficient way. While some existing solutions assume that the reward function is explicitly provided to the learning algorithm (e.g., in the form of a reward machine), the others learn the reward function from the interactions with the environment, assuming no prior knowledge provided by the user. In this paper, we generalize both approaches and enable the user to give advice to the agent, representing the user’s best knowledge about the reward function, potentially fragmented, partial, or even incorrect. We formalize advice as a set of DFAs and present a reinforcement learning algorithm that takes advantage of such advice, with optimal…

Learning Interpretable Temporal Properties from Positive Examples Only

Rajarshi Roy, Jean-Raphaël Gaglione, Nasim Baharisangari +3 more

cs.LO · · cited 23× · arXiv ↗ · more like this ·

We consider the problem of explaining the temporal behavior of black-box systems using human-interpretable models. To this end, based on recent research trends, we rely on the fundamental yet interpretable models of deterministic finite automata (DFAs) and linear temporal logic (LTL) formulas. In contrast to most existing works for learning DFAs and LTL formulas, we rely on only positive examples. Our motivation is that negative examples are generally difficult to observe, in particular, from black-box systems. To learn meaningful models from positive examples only, we design algorithms that rely on conciseness and language minimality of models as regularizers. To this end, our algorithms adopt two approaches: a symbolic and a counterexample-guided one. While the symbolic approach exploits an efficient encoding of language minimality as a constraint satisfaction problem, the…

Being correct is not enough: efficient verification using robust linear temporal logic

Tzanis Anevlavis, Matthew Philippe, Daniel Neider +1 more

cs.LO · · cited 23× · arXiv ↗ · more like this ·

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper we present and study the logic rLTL which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula $φ$, of size at most $\mathcal{O} \left( 3^{ |φ|} \right)$, where $|φ|$ is the length of $φ$. This result improves upon the previously known bound of $\mathcal{O}\left(5^{|φ|} \right)$ for rLTL verification and is closer to the LTL bound of $\mathcal{O}\left( 2^{|φ|} \right)$. The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of…

Synthesis of safety controllers robust to unmodeled intermittent disturbances

Eric Dallal, Daniel Neider, Paulo Tabuada

Computational Theory and Mathematics · · cited 23× · DOI ↗ · more like this ·

The synthesis of controllers enforcing safety properties is a well understood problem for which we have practical algorithms as well as a deep theoretical understanding. This problem is typically formulated as game between the controller seeking to enforce the safety property and the environment seeking to violate it. The solution of these games is given by a winning set: inside the winning set the controller can enforce the desired property as long as it chooses one of the many inputs that forces the system to remain inside the winning set; outside the winning set the environment can violate the winning property independently of the controller's actions. In this paper we answer the following two questions: (1) Among the several inputs available to the controller inside the winning set, are there inputs that are “better” than others? (2) What should the controller do when the state is…

From LTL to rLTL monitoring

Corto Mascle, Daniel Neider, Maximilian Schwenger +3 more

Computational Theory and Mathematics · elib (German Aerospace Center) · · cited 13× · DOI ↗ · more like this ·

Runtime monitoring is commonly used to detect the violation of desired properties in safety critical cyber-physical systems by observing its executions. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can still be satisfied and violated by appropriate extensions. However, a wide range of formulas are not monitorable under this approach, meaning that they have a prefix for which satisfaction and violation will always remain undetermined no matter how it is extended. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, a robust semantics for LTL was introduced to capture different degrees by which a property…

Applications of automata learning in verification and synthesis

Daniel Neider, Wolfgang Thomas, Christof Löding +1 more

Artificial Intelligence · RWTH Publications (RWTH Aachen) · · cited 13× · OpenAlex ↗ · more like this ·

The objective of this thesis is to explore automata learning, which is an umbrella term for techniques that derive finite automata from external information sources, in the areas of verification and synthesis. We consider four application scenarios that turn out to be particularly well-suited: Regular Model Checking, quantified invariants of linear data structures, automatic reachability games, and labeled safety games. The former two scenarios stem from the area of verification whereas the latter two stem from the area of synthesis (more precisely, from the area of infinite-duration two-player games over graphs, as popularized by McNaughton). Regular Model Checking is a special kind of Model Checking in which the program to verify is modeled in terms of finite automata. We develop various (semi-)algorithms for computing invariants in Regular Model Checking: a white-box algorithm, which…

Evrostos

Tzanis Anevlavis, Daniel Neider, Matthew Phillipe +1 more

Computational Theory and Mathematics · · cited 9× · DOI ↗ · more like this ·

Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic (LTL) specifications. Technically, robustness was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In general, model checking an rLTL formula relies on constructing a generalized Büchi automaton of size 5 | φ | where | φ | denotes the length of an rLTL formula φ. It was recently shown that the size of this automaton can be reduced to 3 | φ | (and even smaller) when the formulas to be model checked come from a fragment of rLTL. In this paper, we introduce Evrostos, the first tool for model checking formulas in this fragment. We also present several empirical studies, based on models and LTL formulas reported in the literature, confirming that rLTL model checking for the…

Verifying rLTL formulas: now faster than ever before!

Tzanis Anevlavis, Matthew Philippe, Daniel Neider +1 more

Computational Theory and Mathematics · MPG.PuRe (Max Planck Society) · · cited 9× · DOI ↗ · more like this ·

Robust Linear Temporal Logic (rLTL) was crafted to incorporate the notion of robustness into Linear-time Temporal Logic specifications. Robustness is ubiquitous in control systems and translates the intuitive notion that “small” violations of environment assumptions should only lead to “small” violations of system guarantees. This notion was formalized in the logic rLTL via 5 different truth values and it led to an increase in the time complexity of the associated model checking problem. In this paper we identify and analyze a fragment of rLTL for which the model checking problem can be solved using generalized Biichi automata with at most 3 <sup xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">|φ|</sup> states where |φ| denotes the length of an rLTL formula φ. This is a substantial improvement over the previously known bound of 5 <sup…

Active Finite Reward Automaton Inference and Reinforcement Learning Using Queries and Counterexamples

Zhe Xu, Bo Wu, Aditya Ojha +2 more

cs.LG · · cited 8× · arXiv ↗ · more like this ·

Despite the fact that deep reinforcement learning (RL) has surpassed human-level performances in various tasks, it still has several fundamental challenges. First, most RL methods require intensive data from the exploration of the environment to achieve satisfactory performance. Second, the use of neural networks in RL renders it hard to interpret the internals of the system in a way that humans can understand. To address these two challenges, we propose a framework that enables an RL agent to reason over its exploration process and distill high-level knowledge for effectively guiding its future explorations. Specifically, we propose a novel RL algorithm that learns high-level knowledge in the form of a finite reward automaton by using the L* learning algorithm. We prove that in episodic RL, a finite reward automaton can express any non-Markovian bounded reward functions with finitely…

Analysis of recurrent neural networks via property-directed verification of surrogate models

Igor Khmelnitsky, Daniel Neider, Rajarshi Roy +7 more

Artificial Intelligence · International Journal on Software Tools for Technology Transfer · · cited 7× · DOI ↗ · more like this ·

Abstract This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as a verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping toward faulty flows hinting at the underlying error in the RNN. We also show that our method can be efficiently used for adversarial robustness certification of RNNs.

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free

Daniel Neider, Alexander Weinert, Martin Zimmermann

cs.LO · · cited 7× · arXiv ↗ · more like this ·

Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than one shortcoming. To this end, we combine the logics Linear Dynamic Logic, Prompt-LTL, and robust LTL, each addressing one aspect, to new logics. For all combinations of two aspects, the resulting logic has the same desirable algorithmic properties as plain LTL. In particular, the highly efficient…

ICE: A Robust Learning Framework for Synthesizing Invariants

Pranav Garg, Christof Löding, P. Madhusudan +1 more

Information Systems · · cited 7× · OpenAlex ↗ · more like this ·

Invariant generation lies at the heart of automated program verification, and the learning paradigm for synthesizing invariants is a new promising approach to solve this important problem. Unlike white-box techniques that try to generate an invariant by analyzing the program, learning approaches try to synthesize the invariant given concrete configurations that the invariant must include and exclude, and are algorithmically based on learning theory and scalable machine learning algorithms. In this paper we argue that traditional learning paradigms that use concrete examples and counterexamples are inherently non-robust for synthesizing invariants. We introduce a more general learning paradigm, called ICE-learning, that learns using examples, counter-examples, and implications, and show that this paradigm allows building honest teachers and convergent mechanisms for invariant synthesis.…

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

Daniel Neider, P. Madhusudan, Shambwaditya Saha +2 more

Computational Theory and Mathematics · Journal of Automated Reasoning · · cited 6× · DOI ↗ · more like this ·

Abstract We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that…

Learning Visibly One-Counter Automata in Polynomial Time

Daniel Neider

Artificial Intelligence · · cited 6× · OpenAlex ↗ · more like this ·

Visibly one-counter automata are a restricted kind of one-counter automata: The input symbols are typed such that the type determines the instruction that is executed on the counter when the input symbol is read. We present an Angluin-like algorithm for actively learning visibly one-counter automata that runs in polynomial time in characteristic parameters of the target language and in the size of the information provided by the teacher.

Property-Directed Verification of Recurrent Neural Networks

Igor Khmelnitsky, Daniel Neider, Rajarshi Roy +6 more

cs.LG · · cited 5× · arXiv ↗ · more like this ·

This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping towards faulty flows hinting at the underlying error in the RNN.