The deep feedforward neural networks (DNNs) are increasingly deployed in socioeconomic critical decision support software systems. DNNs exceptionally good at finding min-imal, sufficient statistical patterns within their training data. Consequently, may learn to encode decisions-amplifying existing biases or introducing new ones-that disadvantage protected individuals/groups and stand violate legal protections. While the search based testing approaches have been effective discovering...

A novel reinforcement learning scheme to synthesize policies for continuous-space Markov decision processes (MDPs) is proposed. This enables one apply model-free, off-the- shelf algorithms finite MDPs compute optimal strategies the corresponding without explicitly constructing finite-state abstraction. The proposed approach based on abstracting system with a MDP (without it explicitly) unknown transition probabilities, synthesizing over abstract MDP, and then mapping results back concrete...

A barrier certificate, defined over the states of a dynamical system, is real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable from unsafe ones. When combined with powerful decision procedures—such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT)—barrier certificates enable automated deductive verification approach to safety. The certificate has been extended refute LTL and ω -regular...

The programming of cardiac implantable electronic devices, such as pacemakers and defibrillators, represents a promising domain for the application automated learning systems. These systems, leveraging type artificial intelligence called reinforcement learning, have potential to personalize medical treatment by adapting device settings based on an individual’s physiological responses. At core these self-learning algorithms is principle balancing exploration exploitation. Exploitation refers...

Notions of transition invariants and closure certificates have seen recent use in the formal verification controlled dynamical systems against \omega-regular properties. Unfortunately, existing approaches face limitations two directions. First, they require a closed-form mathematical expression representing model system. Such an may be difficult to find, too complex any use, or unavailable due security privacy constraints. Second, finding such typically rely on optimization techniques as...

Data-driven software is increasingly being used as a critical component of automated decision-support systems. Since this class learns its logic from historical data, it can encode or amplify discriminatory practices. Previous research on algorithmic fairness has focused improving average-case fairness. On the other hand, at extreme ends spectrum, which often signifies lasting and impactful shifts in societal attitudes, received significantly less emphasis. Leveraging statistics value theory...

The theory of regular transformations finite strings is quite mature with appealing properties. This class can be equivalently defined using both logic (Monadic second-order logic) and finite-state machines (two-way transducers, more recently, streaming string transducers); closed under operations such as sequential composition choice; problems functional equivalence type checking, are decidable for this class. In paper, we initiate a study infinite strings. MSO-based definition generalizes...

Given a propositional formula F(x, y), Skolem function for x is ψ (y), such that substituting (y) in F gives semantically equivalent to ∃x F. Automatically generating functions of significant interest several applications including certified QBF solving, finding strategies players games, synthesising circuits and bitvector programs from specifications, disjunctive decomposition sequential etc. In many applications, given as conjunction factors, each which depends on small subset variables....

This study investigates various approaches to using Large Language Models (LLMs) for Text-to-SQL program synthesis, focusing on the outcomes and insights derived. Employing popular dataset, spider, goal was input a natural language question along with database schema output correct SQL SELECT query. The initial approach fine-tune local open-source model generate After QLoRa fine-tuning WizardLM's WizardCoder-15B spider execution accuracy generated queries rose high of 61%. With second...

Programming errors that degrade the performance of systems are widespread, yet there is very little tool support for finding and diagnosing these bugs. We present a method based on differential analysis---we find inputs which varies widely, despite having same size. To ensure differences in robust (i.e. hold also large inputs), we compare not only single inputs, but classes where each class has similar parameterized by their Thus, represented function from input size to performance....

This paper presents a data-driven debugging framework to improve the trustworthiness of US tax preparation software systems. Given legal implications bugs in such on its users, ensuring compliance and is paramount importance. The key barriers developing aids for systems are unavailability explicit specifications difficulty obtaining oracles. We posit that, since law adheres doctrine precedent, about outcome an individual taxpayer must be viewed comparison with individuals that deemed...

Constant-rate multi-mode systems are hybrid that can switch freely among a finite set of modes, and whose dynamics is specified by number real-valued variables with mode-dependent constant rates. The schedulability problem for such to design mode-switching policy maintains the state within safety set. main result paper be decided in polynomial time. We also generalize our optimal problems average cost reachability objectives. Polynomial-time scheduling algorithms make this class an appealing...

We study the problem of analyzing falsifying traces cyber-physical systems. Specifically, given a system model and an input which is counterexample to property interest, we wish understand parts inputs are "responsible" for as whole. Whereas this well known be hard solve precisely, provide approach based on learning from repeated simulations under test.

Bounded-rate multi-mode systems (BMS) are hybrid that can switch freely among a finite set of modes, and whose dynamics is specified by number real-valued variables with mode-dependent rates vary within given bounded sets. The schedulability problem for BMS defined as an infinite-round game between two players---the scheduler the environment---where in each round proposes time mode while environment chooses allowable rate mode, state system changes linearly direction vector. goal to keep...