Jonathan Laurent

This paper presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system's sketch specifying the desired shape of the control envelope, the possible control actions, and the system's differential equations. In order to maximize the flexibility of the control envelope, the synthesized conditions saying which control action can be chosen when should be as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. An implicit, optimal solution to this synthesis problem is characterized using hybrid systems game theory, from which explicit solutions can be derived via symbolic execution and sound, systematic game refinements. Optimality can be recovered in the face of approximation via a dual game characterization. The resulting algorithm, Control Envelope Synthesis via Angelic Refinements (CESAR), is demonstrated in a range of safe control envelope synthesis examples with different control challenges.

We propose a new approach to automated theorem proving where an AlphaZero- style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.

In this paper, we introduce a unified approach for querying simulation traces of rule-based models about the statistical behavior of individual agents. In our approach, a query consists in a trace pattern along with an expression that depends on the variables captured by this pattern. On a given trace, it evaluates to the multiset of all values of the expression for every possible matching of the pattern. We illustrate our proposed query language on a simple example, and then discuss its semantics and implementation for the Kappa language. Finally, we provide a detailed use case where we analyze the dynamics of beta-catenin degradation in Wnt signaling from an agent-centric perspective.

Models based on rules that express local and heterogeneous mechanisms of stochastic interactions between structured agents are an important tool for investigating the dynamical behavior of complex systems, especially in molecular biology. Given a simulated trace of events, the challenge is to construct a causal diagram that explains how a phenomenon of interest occurred. Counterfactual analysis can provide distinctive insights, but its standard definition is not applicable in rule-based models because they are not readily expressible in terms of structural equations. We provide a semantics of counterfactual statements that addresses this challenge by sampling counterfactual trajectories that are probabilistically as close to the factual trace as a given intervention permits them to be. We then show how counterfactual dependencies give rise to explanations in terms of relations of enablement and prevention between events.

Ultra-critical systems are growing more complex, and future systems are likely to be autonomous and cannot be assured by traditional means. Runtime Verification (RV) can act as the last line of defense to protect the public safety, but only if the RV system itself is trusted. In this paper, we describe a model-checking framework for runtime monitors. This tool is integrated into the Copilot language and framework aimed at RV of ultra-critical hard real-time systems. In addition to describing its implementation, we illustrate its application on a number of examples ranging from very simple to the Boyer-Moore majority vote algorithm.

We discuss the design of Looprl, an experimental interactive theorem prover for loop invariant synthesis that has been optimized from the ground-up for a clean integration of theorem proving with reinforcement learning and neural guidance.

Rule-based modeling languages such as Kappa can be used to write mechanistic models of complex biochemical systems. Some techniques have been proposed to analyze the causal structure of such models, ideally providing a way to uncover signalling pathways from networks of low level protein-protein interactions. These methods take advantage of rule structure to (i) slice simulation traces into minimal subsets of events that are sufficient to replicate a phenomenon of interest and (ii) highlight direct causal influences between non-concurrent events. We propose a different but complementary approach to causal analysis that is based on counterfactual reasoning. We argue that our approach can provide better causal narratives by (i) being more sensitive to kinetics and (ii) providing a proper account of inhibition between molecular events.

Interactive theorem provers have been successfully used to formally verify safety- critical software. However, doing so requires a significant level of resources and expertise. A promising approach to scaling-up theorem proving and formal verification is to augment tactic-based interactive theorem provers with machine- learning for automation. The dominant approach in this area is to train a neural network to imitate human experts. However, this approach is limited by the acute scarcity of representative proofs.

An alternative approach inspired by the success of AlphaZero is to use reinforce- ment learning instead and train an agent to interact with a theorem prover via trial and error. Unfortunately, existing tactic-based interfaces offer unbounded action spaces that are hardly amenable to random exploration. Such interfaces are optimized for formalizing human insights in a concise way but often fail to define a tractable search space for deriving those insights in the first place. Moreover, although reinforcement learning alleviates the need for human proofs, the problem remains of providing theorem proving tasks of suitable relevance, diversity and difficulty for the learner.

In this thesis, we propose a novel framework for theorem proving where a teacher agent is trained to generate interesting and relevant tasks while a solver agent is co- trained to solve them. Both agents can leverage domain-specific expert strategies in the form of nondeterministic programs. Choice points in those programs are resolved by neural network oracles that are trained via reinforcement learning in a self-supervised fashion. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is entirely unavailable and hard to synthesize.

This work aims to establish conceptual and engineering foundations for such a framework. We introduce novel curriculum learning algorithms and build a new theorem prover based on neural-guided nondeterministic programming. We introduce standard abstractions and design principles for writing teacher and solver strategies. Finally, we plan to evaluate our theorem prover on a collection of tasks such as loop invariant synthesis, deductive program synthesis, arithmetic inequality proving and safe robot planning.

Rule-based modeling languages such as Kappa can be used to write mechanistic models of complex reaction systems. Such models consist in collections of stochastic graph-rewrite rules that are equipped with different firing rates.