Luke Muehlhauser: From your perspective, what are some of the most interesting or important developments in higher-order verification in the past decade?

Suresh Jagannathan: I would classify the developments of the past decade into four broad categories:

1. The development of higher-order recursion schemes (or higher-order model checking). This approach is based on defining a language semantics in terms of a (recursive) tree grammar. We can now ask whether the tree generated by the grammar satisfies a particular safety property. Because recursion schemes are very general and expressive structures, they can be viewed as natural extensions of model checkers based on pushdown automata or finite-state systems. In the past decade, there have been substantial advances that have made higher-order model checking a practical endeavor, accompanied by realistic implementations.
2. Liquid Types combine facets of classic type inference techniques found in functional language with predicate abstraction techniques used in model checkers to automatically infer dependent type refinements with sufficient precision to prove useful safety properties about higher-order functional programs. Implementations of this approach found in OCaml, SML, and Haskell have demonstrated that it is indeed possible to verify non-trivial program properties without significant type annotation burden.
3. There have been substantial advances in the development of new languages built around rich dependent type systems that enable the expression and static verification of rich safety and security specifications and properties of higher-order programs. These include the languages that support mechanized proof assistants like Coq, Agda, or Epigram, languages like F* geared towards secure distributed programming, libraries like Ynot that encapsulate imperative (stateful) features and Hoare-logic pre/post-conditions within a higher-order dependent type framework, and features such as GADTs and type classes found in languages like GHC.
4. Polyvariant control-flow analyses like CFA2 or higher-order contracts are two techniques that facilitate verification and analysis of dynamic higher-order languages. CFA2 adopts pushdown models used in program analyses for first-order languages to a higher-order setting, enabling precise matching of call/return sequences. Higher-order contracts allow runtime verification and blame assignment of higher-order programs and are fully incorporated into Racket, a multi-paradigm dialect of Lisp/Scheme.

Read more »

Luke Muehlhauser: In Fuchs et al. (2013), you and your co-authors provide an introduction to quantum Bayesianism aka “QBism,” which you more or less co-invented with Carlton Caves and Christopher Fuchs. But before I ask about QBism, let me ask one of the questions asked of the interviewees in Elegance and Enigma: The Quantum Interviews (including Fuchs): “What first stimulated your interest in the foundations of quantum mechanics?”

Ruediger Schack: I can trace the beginning of my interest in quantum foundations to reading one paper: “Where do we stand on maximum entropy?” by Ed Jaynes, and one book: Du Microscopique au Macroscopique by Roger Balian. Jaynes’s paper introduced me to Bayesian probability theory, and Balian’s book taught me that one can think of quantum states as representing Bayesian probabilities.

Read more »

Luke Muehlhauser: One of your projects at IHMC is “The Role of Benevolence in Trust of Autonomous Systems“:

The exponential combinatorial complexity of the near-infinite number of states possible in autonomous systems voids the applicability of traditional verification and validation techniques for complex systems. New and robust methods for assessing the trustworthiness of autonomous systems are urgently required if we are to have justifiable confidence in such applications both pre-deployment and during operations…  The major goal of the proposed research is to operationalize the concept of benevolence as it applies to the trustworthiness of an autonomous system…

Some common approaches for ensuring desirable behavior from AI systems include testing, formal methods, hybrid control, and simplex architectures. Where does your investigation of “benevolence” in autonomous systems fit into this landscape of models and methods?

Read more »

Luke Muehlhauser: In 2004 you co-authored Introduction to Autonomous Mobile Robots, which offers tutorials on many of the basic tasks of autonomous mobile robots: locomotion, kinematics, perception, localization, navigation, and planning.

In your estimation, what are the most common approaches to “gluing” these functions together? E.g. are most autonomous mobile robots designed using an agent architecture, or some other kind of architecture?

Roland Siegwart: Mobile robots are very complex systems, that have to operate in real world environments and have to take decisions based on uncertain and only partially available information. In order to do so, the robot’s locomotion, perception and navigation system has to be best adapted to the environment and application setting. So robotics is before all a systems engineering task requiring a broad knowledge and creativity. A wrongly chosen sensor setup cannot be compensated by the control algorithms. In my view, the only proven concepts for autonomous decision making with mobile robots are Gaussian Processes and Bayes Filters. They allow to deal with uncertain and partial information in a consistent way and enable learning. Gaussian Processes and Bayes filter can model a large variety of estimation and decision processes and can be implemented in different forms, e.g. as the well-known Kalman Filter estimator.

Most mobile robots use some sort of agent architecture. However, this is not a key issue in mobile robots, but rather an implementation issue for systems that run multiple tasks in parallel. The main perception, navigation and control algorithms have to adapt to unknown situation in a somewhat predictably and consistent manner. Therefore the algorithms and navigation concepts should also allow the robotics engineer to learn from experiments. This is only possible, if navigation, control and decision making is not implemented in a black-box manner, but in a model based approach taking best advantage of prior knowledge and systems models.
Read more »

Luke Muehlhauser: In Verma & del Vecchio (2011), you and your co-author summarize some recent work in semiautonomous multivehicle safety from the perspective of hybrid systems control. These control systems will “warn the driver about incoming collisions, suggest safe actions, and ultimately take control of the vehicle to prevent an otherwise certain collision.”

I’d like to ask about the application of hybrid control to self-driving cars in particular. Presumably, self-driving cars will operate in two modes: “semi-autonomous” (human driver, with the vehicle providing warnings and preventing some actions) and “fully autonomous” (no human driver). Do you think hybrid control will be used for both purposes, in commercial self-driving cars released (e.g.) 10 years from now? Or do you think hybrid control will be competing with other approaches aimed at ensuring safe behavior in autonomous and semi-autonomous vehicles?

Read more »

Luke Muehlhauser: A couple years ago you wrote a review article on algorithmic self-assembly, and also created a video introduction to the subject. Your review article begins:

Self-assembly is the process by which small components automatically assemble themselves into large, complex structures. Examples in nature abound: lipids self-assemble a cell’s membrane, and bacteriophage virus proteins self-assemble a capsid that allows the virus to invade other bacteria. Even a phenomenon as simple as crystal formation is a process of self-assembly… Algorithmic self-assembly systems automate a series of simple growth tasks, in which the object being grown is simultaneously the machine controlling its own growth.

As an example, here’s a an electron microscope image of a Sierpinski triangle produced via algorithmic self-assembly of DNA molecules:

Read more »

Read more »