20 Jun 2019
9 min read
#Symbolic AI for algorithm state-space exploration
Our world runs on algorithms — from autopilot systems inside Boeing jets to “dark pools” run by investment banks to autonomous vehicle controllers. So it’s fairly important we understand how they might behave (especially when they can behave in ways we don’t want).
When describing an algorithm or a complex system, we often need to enumerate its “edge cases” or distinct behaviors, and illustrate them with concrete examples. The problem is that modern “real world” algorithms (systems) are designed to process (virtually) infinite collections of possible inputs (think of a Boeing autopilot system and the possible scenarios it can be in). So how do we manage this “infinity”?
At Imandra we’ve developed a technique for automatically describing and reasoning about algorithm state-spaces. We call it Region Decomposition and it is a core feature of Imandra, our cloud-native automated reasoning engine. It creates a quantitative ‘map’ of how a system might behave with sample points. One exciting application of Region Decomposition is for software testing as it creates a quantitative and explainable coverage metric of a system under test. In this post we’ll introduce Region Decomposition and outlines its many applications.
The term Region Decomposition (RD) refers to a (geometrically inspired) “slicing” of an algorithm’s state-space into distinct regions where the behavior of the algorithm is invariant, i.e., where it behaves “the same.” Each “slice” or region of the state-space describes a family of inputs and the output of the algorithm upon them, both of which may be symbolic and represent many concrete instances. We’ll dive into examples below which will make everything clear, but for now remember this – each region of the state-space represents a “distinct” behavior of the system, and a decomposition is a collection of regions covering the entire space, including the so-called “edge-cases.”
RD is inspired by Cylindrical Algebraic Decomposition (CAD) but Imandra “lifts” these techniques to algorithms at large. There are many recent advances in formal verification, mathematics and computers science that are packed into Imandra to make this happen.
Describing algorithms’ behaviors this way has many exciting applications in automated software testing, reinforcement learning, autonomous systems and many other domains. In this and the subsequent posts we will go into more detail with examples and applications.
Let’s jump in and start to build the intuition!
Note: Imandra, our reasoning engine, supports OCaml and ReasonML at its lowest level (we’ll have Python interface out soon), so all of the examples presented here are in OCaml. Why OCaml (and ReasonML)? We’ve created a ‘mechanized formal semantics’ for the pure subset of OCaml which allows Imandra to automatically convert the code into axiomatic representation (i.e. mathematical logic) and reason about it similarly to how a mathematician would reason about a theorem. Since ReasonML is a syntactic extension to OCaml, we fully support it too.
Consider the following code fragment:
let g x = if x > 22 then 9 else 100 + x let f x = if x > 99 then 100 else if x < 70 && x > 23 then 89 + x else if x > 20 then g x + 20 else if x > -2 then 103 else 99 ;;
We have two functions g and f and the latter looks somewhat convoluted. (In OCaml, types are inferred from the code and since we’re using integer arithmetic operators and values, both x arguments in functions g and f are taken to be integers)
Function f takes x as input, which is an integer and there are quite a few integers, so how many distinct behaviors of f are there? Let’s ask Imandra!
When we run decompose command with the name of the function f, we get the following (we include a still screenshot below, but the full region decomposition can be interactively explored at try.imandra.ai):
Imandra decomposes the function
7 regions. We’ve created a Voronoi widget for Jupyter Notebooks to help us visualize them. The region selected in the image above is
R (the naming convention refers to how Imandra decides to differentiate regions internally, based upon their symbolic relationships). In this decomposition,
R represents subset of the state-space where input x satisfies
-2 < x <= 20 (e.g.
15) — in this region, the function will always return the value103. If you click on
R, the constraint is
20 < x <= 22 and invariant result is
x + 120. Notice that the invariant in
R is symbolic, so if
21 then the function will return
If you combine all of these regions together, you will get the full behavior of
f, a fact which Imandra mathematically proves behind the scenes.
An immediate question might be whether RD scales to “real-world” algorithms. The answer is “Yes.” In fact, it is already deployed in production at some of the world’s leading financial institutions. It took us a few years of R&D and industrial POCs to get it right.
A naive approach would be to simply follow ‘branching’ within code and identify those paths as ‘distinct’ behaviors, but this would quickly ‘explode’ with even remotely complex algorithms. Moreover, when recursive functions are involved (even typical operations over Lists are recursive!), things get really tricky — Imandra is packed with quite a few powerful techniques to manage this.
Here’s a small example to help illustrate how Region Decomposition works under the hood. Consider the function myfunc below:
let myfunc a = if a > 10 then true else if a > 5 then true else false
How many regions would you expect myfunc to have? The answer is
1 and if this wasn’t the case, then the approach we present here wouldn’t scale.
Imandra determined that myfunc may be described with a single region without any constraints on the input argument a and whose behavior is described by the invariant result of
a > 5! For all possible values of a, the output of
myfunc a is equal to
a > 5, which of course could either be
As described, Region Decomposition is one of the core features of Imandra and there are quite a few ways you can use it.
At the lowest level (we have other front-end languages for RD including Python which we’ll cover later) Imandra accepts OCaml (and ReasonML). For the pure subsets of OCaml/ReasonML, Imandra (automatically) converts code into an axiomatic representation, applying numerous magical tricks and generating a state-space decomposition with an accompanying completeness proof. Each region in the decomposition also includes a solver which can be used to automatically generate inputs satisfying the region constraints. This feature is very useful for test-suite generation, for example.
In this section we’ll briefly cover transforming/printing regions into other formats (e.g. English prose) and using side-conditions to focus on various subsets of the algorithm state-space you’re decomposing. As always, please see our documentation at https://docs.imandra.ai for full information.
What can we do with these results? Well, since Imandra reflects the results back into the OCaml/ReasonML runtime, quite a lot:
-Synthesize inputs and test-cases: Given a region, we can ask Imandra to synthesize concrete inputs (as valid OCaml values) satisfying the region constraints. These are inputs which “push” the system into the given region. This provides a powerful basis for test-case and documentation generation, for example.
We’ll look at an example of a printer for the longer example below.
A key feature of Region Decomposition is the ability to superimpose constraints on the inputs and/or result of the function you’re decomposing. This allows you to focus on a specific subset of the state-space of the algorithm.
To to illustrate this, let’s revisit our first example function
f. What if we wanted to restrict the input?
Since the side condition is just a boolean function, we can constrain the state space based on the result of running the function
Let’s now look at something a bit more complex and “real-world”. The complete example is in our documentation page (with a live Jupyter Notebook), so please check it out — we will just provide a high-level overview here.
Algorithms underpinning financial venues (exchanges and “dark pools”) are notoriously complex and are definitely “safety-critical”, so when they crash or ‘misbehave’, bad things happen. Naturally, they should be designed, tested and audited with formal methods. At Imandra, we’re making this a reality.
For this next example, we’re going to take a description of order book pricing logic from an actual exchange (SIX Swiss). This specific component determines the price of a transaction between a buy and a sell order, if the trade is possible. This logic would be just a fraction of the entire model of the exchange, but this is outside the scope of this exercise (interested readers should take a look at our white papers for complete discussion of how we model exchanges and other venues).
The main function of this code is as follows:
let match_price (ob : order_book) (ref_price : real) = (* Select the best buy and sell order of the order book (if they exist) *) let bb = best_buy ob in let bs = best_sell ob in match bb, bs with (* Now we'll match on values of `bb` and `bs`. We're using OCaml's option types - explicitly having a value of `None` when no `bb` or `bs` order exists. *) Some bb, Some bs -> begin match bb.order_type, bs.order_type with (* When we're matching Limit/Limit or Quote/Quote orders, then the outcome is simply limit price of the older order. *) | (Limit, Limit) | (Quote, Quote) -> Known (older_price bb bs) (* Logic gets more nuanced, however, when *) | (Market, Market) -> if bb.order_qty <> bs.order_qty then Unknown else (* need to look at other orders in the order book *) let bBid = match (next_buy ob) with Some bestBuy -> if bestBuy.order_type = Market then None else Some bestBuy.order_price | _ -> None in let bAsk = match (next_sell ob) with Some bestSell -> if bestSell.order_type = Market then None else Some bestSell.order_price | _ -> None in begin match bBid, bAsk with | (None, None) -> Known ref_price | (None, Some ask) -> if ask <. ref_price then Known ask else Known ref_price | (Some bid, None) -> if bid >. ref_price then Known bid else Known ref_price | (Some bid, Some ask) -> if bid >. ref_price then Known bid else if ask <. ref_price then Known ask else Known ref_price end | (Market, Limit) -> Known bs.order_price | (Limit, Market) -> Known bb.order_price | (Quote, Limit) -> if bb.order_time > bs.order_time then (* incoming quote *) begin if bb.order_qty < bs.order_qty then Known bs.order_price else if bb.order_qty = bs.order_qty then match (next_sell ob) with | None -> Known bb.order_price | Some ord -> Known ord.order_price else Unknown end else (* existing quote's price is used *) Known bb.order_price | (Quote, Market) -> if bb.order_time > bs.order_time then (* incoming quote *) begin let nextSellLimit = next_sell ob in if bb.order_qty < bs.order_qty then Known bs.order_price else if bb.order_qty = bs.order_qty then match nextSellLimit with | None -> Known bb.order_price | Some ord -> Known ord.order_price else Unknown end else (* The quote's price is used *) Known bb.order_price | (Limit, Quote) -> if bb.order_time > bs.order_time then begin (* incoming quote *) if bs.order_qty < bb.order_qty then Known bb.order_price else if bb.order_qty = bs.order_qty then match (next_buy ob) with | None -> Known bs.order_price | Some ord -> Known ord.order_price else Unknown end else (* existing quote's price is used *) Known bs.order_price | (Market, Quote) -> if bb.order_time > bs.order_time then begin (* incoming quote *) if bs.order_qty < bb.order_qty then Known bb.order_price else if bb.order_qty = bs.order_qty then (match (next_buy ob) with | None -> Known bs.order_price | Some ord -> Known ord.order_price ) else Unknown end else (* The quote's price is used *) Known bs.order_price end | _ -> Unknown
When we ask Imandra to decompose this function, we get this:
The constraints as they’re written by default are basically OCaml – you’ll notice some of the constraints contain List.hd ob.buys or List.hd ob.sells. Those are references to the first buy and sells orders using the standard OCaml list functions. To make this more readable we can make use of OCaml’s pattern matching and Imandra’s extensibility to create a custom printer (the notebook has full source code):
module Refiner = struct open PPrinter let walk (x : node) : node = match x with | Funcall ("List.hd", [FieldOf (_, "buys", _)]) -> Var "First buy order" | Funcall ("List.hd", [FieldOf (_, "sells", _)]) -> Var "First sell order" | Funcall ("List.hd", [Funcall ("List.tl", [FieldOf (_, "buys", _)])]) -> Var "Second buy order" | Funcall ("List.hd", [Funcall ("List.tl", [FieldOf (_, "sells", _)])]) -> Var "Second sell order" | Is (t, ty, FieldOf (_, "order_type", x)) -> Is (t, ty, x) | FieldOf (Assoc, (("order_id" | "order_qty" | "order_price" | "order_time") as field), x) -> FieldOf(Human, field, x) | x -> x let refine node = XF.walk_fix walk node |> CCList.return end
After we install this new printer and view the regions, we see the constraints printed in a much more ‘human-readable’ format (if you spend more time on the printer, you can do much more!).
It’s a pretty powerful technique — we’ve gone from a pure executable OCaml algorithm describing the business logic (a simulator) to automated generation of edge case descriptions in English-like prose!
The last step we’ll perform is generating sample points for the regions. A natural use case for these samples are test cases. Imagine you create a model of the system you would like to test and ask Imandra to describe its regions (or ‘edge cases’) and construct inputs for each one of them. This will give you test cases and also a quantitative coverage metric describing what it is that you’re actually testing!
In this post, we have introduced Region Decomposition — a powerful technique of describing algorithm state-spaces. The next posts in this series will cover more advanced features and applications. Here’s the current plan:
If you have any questions or requests, don’t hesitate to drop us a line (or two) in our Discord server.
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!