Jonathan Laurent

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.

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.

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.