Jonathan Laurent

Large Language Models have proven surprisingly effective at solving a wide range of tasks from just a handful of examples. However, their lack of reliability and modularity limits their capacity to tackle large problems that require many steps of reasoning. In response, researchers have proposed advanced pipelines that leverage domain-specific knowledge to chain smaller prompts, provide intermediate feedback and improve performance through search. However, the current complexity of writing, tuning, maintaining and improving such pipelines has limited their sophistication. We propose oracular programming, a foundational paradigm for building LLM-enabled applications that lets domain experts express high-level problem-solving strategies as programs with unresolved choice points. These choice points are resolved at runtime by LLMs, which generalize from user-provided examples of correct and incorrect decisions. An oracular program is composed of three orthogonal components: a strategy that consists in a nondeterministic program with choice points that can be reified into a search tree, a policy that specifies how to navigate this tree with the help of LLM oracles, and a set of demonstrations that describe successful and unsuccessful search tree navigation scenarios across diverse problem instances. Each component is expressed in a dedicated programming language and can be independently improved or substituted. We address the key programming language design challenges of modularly composing oracular programs and enforcing consistency between their components as they evolve.

Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic winning policies of hybrid games, where each deterministic specialization of the policy is a control solution. This paper synthesizes nondeterministic winning policies for hybrid games that are as permissive as possible. It introduces subvalue maps, a compositional representation of such policies that enables verification and synthesis along the structure of the game. An inductive logical characterization in differential game logic (dGL) checks whether a subvalue map induces a sound control envelope which always induces a winning play. A policy is said to win if it always achieves the desirable outcome when the player follows it, no matter what actions the opponent plays. The maximal subvalue map, which allows the most action options while still winning, is shown to exist and satisfy a logical characterization. A family of algorithms for nondeterministic policy synthesis can be obtained from the inductive subvalue map soundness characterization. An implementation of these findings is evaluated on examples that use the expressivity of dGL to model a range of diverse control challenges.

Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, before a problem can be solved it needs to be stated. This requires writing a formal physics model of the cyber-physical system, which is a complex task that traditionally requires human expertise and becomes a bottleneck.

This paper experimentally studies whether Large Language Models (LLMs) can automate the formalization process. A 20-problem benchmark suite is designed drawing from undergraduate-level physics kinematics problems. In each problem, the LLM is provided with a natural language description of the objects’ motion and must produce a model in differential game logic (dGL). The model is (1) syntax checked and iteratively refined based on parser feedback, and (2) semantically evaluated by checking whether symbolically executing the dGL formula recovers the solution to the original physics problem. A success rate of 70% (best over 5 samples) is achieved. We analyze failing cases, identifying directions for future improvement. This provides a first quantitative baseline for LLM-based autoformalization from natural language to a hybrid games logic with continuous dynamics.

A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate runtime knowledge acquisition. Model-checking and automated reasoning have been successfully used for shielding, i.e., to monitor untrusted controllers and override potentially unsafe decisions, but only at the cost of hard tradeoffs in terms of expressivity, safety, adaptivity, precision and runtime efficiency. We propose a programming-language framework that allows experts to statically specify adaptive shields for learning-enabled agents, which enforce a safe control envelope that gets more permissive as knowledge is gathered at runtime. A shield specification provides a safety model that is parametric in the current agent's knowledge. In addition, a nondeterministic inference strategy can be specified using a dedicated domain-specific language, enforcing that such knowledge parameters are inferred at runtime in a statistically-sound way. By leveraging language design and theorem proving, our proposed framework empowers experts to design adaptive shields with an unprecedented level of modeling flexibility, while providing rigorous, end-to-end probabilistic safety guarantees.

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.