Machine Reasonable Design with Imandra
On July 19th the US Securities and Exchange Commission approved changes to the 20-year old Reg ATS, bringing greater transparency to US financial markets. These changes come at a time of unprecedented regulatory changes in European markets as well. MiFID II led to a creation of a whole new class of pre-trade transparent venues implementing ‘periodic auctions’. Their logics are typically much more complex than those of their predecessors, something that is already causing concern about their opaqueness from some investors and regulators.
In this post we discuss Machine Reasonable Design – a form of system design susceptible to automated reasoning (symbolic artificial intelligence). Such format allows for rigorous design analysis, testing and auditing of complex venues, alleviating many of the issues facing these markets today. We demonstrate how our automated reasoning system, Imandra, makes this possible.
The SEC approves changes to Reg ATS
A month ago the US Securities and Exchange Commission approved Reg ATS-N, an overhaul to the existing Reg ATS specifying, among other things, how ATS (aka “dark pool”) operators (e.g. investment banks) should publicly disclose details of their venue operations. The process of submitting this document is akin to your tax returns with the authorities – the SEC doesn’t check that it’s valid when you submit it, but rather acknowledge that they’ve received it, and may later investigate whether it’s actually what’s implemented inside. That is because the disclosure is an English prose, hence there’s no easy way to connect it to the actual production system and perform an audit. As it stands, this audit process takes years (because the SEC has to reconcile English with data), so when you read about fines imposed on venue operators it will say that the investigation took X years. Moreover, as we demonstrate later, the submitted form may be logically inconsistent in subtle yet important ways that only an artificial intelligence system may recognise (very difficult to ‘do it by hand’). We’ll show how this happens using our winning UBS competition entry.
The new form Reg ATS-N will be required of all ATS operators and is a much more thorough description of how these venues operate. Now ATS operators will need to make their forms publicly available, which was voluntary before. Although the changes do not go as far as our recommendations outlined in a public comment letter we’ve written in 2016, we believe this is a great outcome for the industry and is indicative of further scrutiny financial firms should expect worldwide when it comes to their trading systems.
MiFID II and periodic auctions
Introduction of MiFID II in Europe led to a proliferation of a new type of pre-trade transparent venues. They run multiple auctions throughout the day and publish prices that other firms may participate at. On the surface that sounds like a minimal amount of work. This could not be farther from the truth; auctions and transitions into/from them are shockingly complex. There are many examples where big financial firms failed to consider (let alone enumerate) the vast number of edge cases such designs entail and correctly implement them. Some of the more famous examples are the BATS IPO and Facebook IPO glitches.
Despite seemingly counterintuitive, designs of periodic auction venues may be actually more complex than that of their public exchange counterparts (e.g. like those examples above where they failed to perform IPO auctions). One of the reasons is that these venues operate more options that lead to highly non-trivial behaviour. One example is “broker preference” – feature that changes order priority ranking to favour orders from the same member above others (for a given price level, etc.). These features lead to a much more complex recursive structure of the auction algorithm and become both a design and a implementation risk.
Increasingly complex market structure with greater regulatory transparency requirements overlaid with margin compression is creating an unsustainable operating environment. Throughout this post we discuss venues because they are often public entities and their operational details are available, but our approach covers virtually all types of complex trading systems.
The current industry practice of creating trading software relies on ‘hope’ as an integral component of IT strategy. Project managers hope that requirements are correct and are logically consistent. Developers hope they understand the requirements. Compliance hopes that they understand the system behaviour. Senior management hopes the people doing the actual work are smart, diligent and are not going to change jobs within the current audit cycle. Regulators secretly hope that some of those hopes are misplaced.
Some banks fare much better than others. But there is an alternative approach. One that enforces a quantitative measure of governance eliminating reliance on hope in at least some places.
Machine Reasonable Design
Let’s think about the 3 broad categories of persons involved in creating and running a venue (again, we use venues are examples but this message carries across all typical financial systems):
- Business – sales and product managers tasked with designing features that would be attractive to clients (i.e. can be sold)
- Developers – project managers, actual developers writing the code and quality assurance personnel (QA)
- Regulators – compliance staff and the actual regulators
Currently these three groups communicate with each other over long Word documents and email chains. Such ambiguity leads to missed requirements, their inconsistency and poor code quality (when it’s actually delivered). Poor code quality results in more Word documents, emails and middle management/compliance headcount. This leads to internal politics and makes everyone depressed. Depressed people cannot be motivated, so the bank makes less money. And so it continues.
When you think about the unfathomable costs of software development in finance, this is the reason. Finance has enough smart people that know how to code, figuring out what they should code is the difficult part. Very few people realise this. This is analogous to how most people think they’re better drivers than the average. Telling developers, people that were the smartest in their High School class, that they need to think more about what they’re going to code before they start coding is a challenge. However the payoff is worth it.
One analogy that we often is use is that of a skyscraper construction process. It’s similar to finance in that it’s very complex and involves different types of stakeholders: from architects to civil engineers to construction workers. What’s different is that they communicate over something that’s precise – a blueprint that describes in necessary detail what should be built.
Finance needs something similar and it has to be incremental - it cannot require firms to wait years before any results start to bear fruit.
The Promised Land
Financial systems should have precise designs – especially in environments with so many moving parts and stakeholders. Understanding the full behaviour of a system – i.e. all the infinitely many ways it can behave – before you start building it sounds like a trivial requirement, but it is far from the norm. There are two culprits behind this: finance, until recently, was making too much money to care and the technology/science wasn’t there to facilitate this.
In other safety-critical industries Model-Based Engineering (MBE) is advocated as a way to ensure rigour of software development processes. There are numerous tools like MathWorks Simulink that allow one to construct and reason about data-flow models (e.g. for control algorithms in avionics). But these are very different from the typical systems in finance. Finance deals with FIX messages, derivative contracts, etc. Simulink and similar tools would be too difficult to adapt to financial markets.
The design of a financial system in this case is an executable model of the system business logic (together with messaging, etc) with which you can:
- Compile the model to binary or generate source code in a target language
- Verify properties about its behaviour
- Generate test cases
- Generate English-prose documentation
- Run an audit against the actual production trading data.
Why is it Machine Reasonable and why is this important?
A typical financial system is complex and more importantly, it may be in a virtually infinite number of states. Just as 80 or so years ago people started to use computers to reason about numbers (because the calculations became too intense for humans to perform ‘by hand’), so must we when it comes to reasoning about algorithms. After all, just as numbers, algorithms are mathematical objects. If you think it’s a good idea to use a computer to price an option or forecast price of a security, you should also try using it to analyse algorithms. You’ll be surprised.
By Machine Reasonable we mean that you can use a computer to automatically analyse behaviour of this code and ask typical questions which may cover infinitely many possibilities. We’ve already written about Machine Reasonable APIs for specifying how systems should communicate with each other. This post tackles a different problem. One example: “Can this venue product fills outside the NBBO?”. You simply cannot test (in a traditional way) for these properties. Once you are confident the design is correct (or still correct when you make amendments), then you leverage it to test all of the edge case (we call these state space regions) and use it to audit production data.
Automated Reasoning with Imandra
Historically, reasoning about code in the deep way we’ve been discussing was very labour-intensive (limited automation) and reserved to a few that had specialised training (e.g. teams of scientists at places like NASA). We created Aesthetic Integration to change this.
We’ve spent over 4 years of R&D to create an engine that allows you to write production quality code and also reason about its behaviour. Check out https://try.imandra.ai. We’re launching a commercial version this September that you’ll be able to download and use on your local files, seamlessly leveraging Imandra’s groundbreaking scalable symbolic AI in the cloud.
We’ve taken a pure subset of OCaml and given it mechanised formal semantics – meaning that everything you write in this language, Imandra automatically translates into mathematical logic. The beauty is that you can leverage the OCaml ecosystem (e.g. compiler, etc) to develop code and use Imandra’s Reasoning as a Service (TM) engine to verify its critical components.
Imandra has two core features:
- Code Verification – ensuring the code satisfies a certain property (and getting a mathematical proof when it does or a concrete counterexample when it doesn’t). Imandra’s code verification is built on major recent advances in the field of formal verification. We’ll see examples of this later when we look at the UBS Form ATS and transitivity of their order ranking logic.
- Code Analysis – understanding the different ways the code may behave. We already discussed that there are typically infinitely many possible states – this feature describes them symbolically through a finite number of edge cases (or state space regions).
Both of these are important when it comes to creating and using Machine Reasonable Design.
When one claims that a venue, for example, “Always generates fills within the BBO.”, you’re covering infinitely many scenarios. You’re not forced to come up with some sample inputs that would pass for ‘test cases’, you’re allowed to reason on a higher level, just like you do when you speak to someone describing how this venue works.
It’s important to note that the process of creating such a design is an iterative one and that’s a good thing. It forces the stakeholders involved to think through all of the subtle issues prior to anyone starting to code in C++, get regulators to sign off or sales start to send out marketing materials. Even if the system is already implemented, one can use the model to generate test cases or even audit the log data to look for inconsistencies with the verified design.
Now let’s look at a concrete example.
UBS Future of Finance Challenge 2015
About 3 years ago, when our company was just getting started, we were looking for public ways we could demonstrate how Imandra could fundamentally change how the financial software is created and regulated. We came across UBS Future of Finance Challenge – a competition run by the bank with over 620 participants from 52 countries. It ran over multiple months (2 rounds) and we ultimately got 1st place.
With the launch of https://try.imandra.ai, we can finally publicly demonstrate the work that we did for the competition. We’ll do a high-level summary below, but here are more resources:
- The full notebook (you can try it live)
- Our white paper
- Bloomberg article “Intel’s Pentium Bug Fix is Proposed as a Solution to Dark Pools”
In early 2015, UBS was fined around $15 million for violations of the way its “dark pool” operated. The settlement was made public by the SEC and detailed the 2 main violations – undisclosed crossing restrictions (conditions preventing two orders from trading with each other) and sub-penny pricing (allowing orders with limit prices violating minim tick requirements). The second one is important because if you’re allowed to send in an order to buy a stock at 5.0000001, then technically you will automatically receive price priority over someone that is buying it at 5.00 even though the difference is economically negligible.
Luckily, UBS made their Form ATS (see the very first paragraph) available as well, so we began to encode the model as we interpreted it from the form and the 2 violations described in the SEC settlement. In the process, we discovered something much more interesting and subtle.
Here’s a snippet of code that contains the logic (again, based on the English description from the Form ATS) of how the priority between two orders is determined. Typically, priority is determined by ‘price/time’, meaning that an order whose price is more aggressive (higher for buys and lower for sells) is selected, and if there’s a tie, then the older order is selected. In dark pools this criteria may get more complicated and this is one such example:
When we began to attempt to reason about the full model with this logic, Imandra kicked it back to us because it discovered a fundamental flaw: this ranking criteria was not transitive. Transitivity means that if A is greater than B and B is greater than C, then A must be greater than C. If the criteria is not transitive, then using it to sort a list of items makes no sense (especially if you’re regulated by the SEC). Sounds obvious? Well, it can get really tricky if you’re sorting orders.
Here is how we could state it explicitly in Imandra (as you can see, we’re simply writing a boolean function that Imandra will then reason about):
The English version of this is “For all sides and market conditions, if Order 1 is higher ranked than Order 2 and Order 2 is higher ranked than Order 3, then Order 1 must be higher ranked than Order 3”. We’d expect this to hold true, but Imandra gives us the following counterexample:
I’m going to jump ahead and present this using a custom printer (again, all the code is in the notebook) so it’s more pleasant to see what’s going on:
Because the counterexamples are reflected back into the runtime, we can use them to check whether these counterexamples are valid by computing the actual values:
You can figure out the error for yourself on the live Jupyter notebook site!
Computing with counterexamples is important because most often, when you have a model and a property you wish to verify, you will have edge cases you haven’t thought about. This is where Imandra shines – you discover them at this stage and figure out what is wrong before systems are developed, let alone put into production.
We’ve covered verification – to see how you generate test cases from this model, print out its behaviour in English prose, etc. check out our notebooks at try.imandra.ai.
Conclusion
It’s inevitable that humans use machines to reason about code – we’re simply not designed to analyse millions upon millions of edge cases that are typical of modern trading systems. We’re already working with several investment banks on leveraging Imandra to bring unprecedented rigour and governance to their software development processes. We’ll launch a commercial version of Imandra you’ll be able to download and use locally this September, so stay tuned!
To stay in touch, email us at contact@imandra.ai.
