|
<< PUBLICATIONS (in reverse chronological order) Click here to hide/show abstracts
. . Compositional Taylor Model Based Validated Integration {Abstract} We present a compositional validated integration method based on Taylor models. Our method combines solutions for lower dimensional subsystems into solutions for a higher dimensional composite system, rather than attempting to solve the higher dimensional system directly. We have implemented the method in an extension of the Flow* tool. Our preliminary results are promising, suggesting significant gains for some biological systems with nontrivial compositional structure.
. . Formal Verification of Financial Algorithms {Abstract} Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we have pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools and FIX connectivity between trading systems), we describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We sketch many open problems and future directions along the way.
. . Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL {Abstract} We present a proof procedure for univariate real polynomial problems in Isabelle/HOL. The core mathematics of our procedure is based on univariate cylindrical algebraic decomposition. We follow the approach of untrusted certificates, separating solving from verifying: efficient external tools perform expensive real algebraic computations, producing evidence that is formally checked within Isabelle's logic. This allows us to exploit highly-tuned computer algebra systems like Mathematica to guide our procedure without impacting the correctness of its results. We present experiments demonstrating the efficacy of this approach, in many cases yielding orders of magnitude improvements over previous methods.
. . Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers {Abstract} We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., ``x^n in Q'' and ``x^n in Z.'' Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.
. . Case Study: 2015 SEC Fine Against UBS ATS {Abstract} This year's $14 million settlement between the US Securities and Exchange Commission (SEC) and UBS over allegations of misconduct in design, marketing and implementation of their ATS (dark pool) highlights the financial services industry's ongoing struggles with the staggering (and growing) complexity of trading algorithms. We demonstrate how UBS can leverage AI's groundbreaking formal verification technology to help prevent further regulatory fines related to the design and implementation of UBS dark pools. Powered by recent breakthroughs, our product Imandra is able to automatically prove properties of fairness and best execution of venue designs and test production implementations with unprecedented rigour. We demonstrate how Imandra can automatically detect and test for key recent issues raised by the SEC. Furthermore, based on UBS's publicly available Form ATS filing, we apply Imandra to highlight additional potential issues with UBS's current dark pool design. Finally, we discuss applications of Imandra to a wide range of financial algorithms, including routing systems and smart contracts.
. . Transparent Order Priority and Pricing {Abstract} Transparency of trading algorithms is a pressing issue in today's financial markets. For example, though a dark pool may have access to client-specific information, can it ever use that information to affect order priority or pricing in a manner not reflected in regulatory filings and marketing materials? Many such questions are difficult (if not impossible) to answer by looking at post-trade data alone. Fortunately, recent scientific breakthroughs allow us to systematically analyse algorithms for compliance and conformance with regulatory directives and marketing materials. Our product, Imandra, leverages latest research breakthroughs to deliver an automated formal verification solution for designing, implementing and regulating financial algorithms. Imandra reasons about precise statements concerning the behaviour of trading algorithms, giving the industry and regulators unprecedented insight into what trading algorithms can and cannot do. In this report, we illustrate Imandra's application to the transparency of order priority and pricing within venues.
. . Creating Safe and Fair Markets {Abstract} Many deep issues plaguing today's financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. When it comes to exhaustively reasoning about the behaviour of complex algorithms, the only viable solution is formal verification, the use of deep advances in mathematical logic to automatically reason about algorithms and prove properties of programs. Aesthetic Integration is bringing formal verification to financial markets for the first time. In this white paper intended for the wider financial industry, we present our vision for the design and regulation of electronic financial markets empowered by formal verification.
. . A Note on Real Quantifier Elimination by Virtual Term Substitution of Unbounded Degree {Abstract} We describe work in progress on constructing a complete implementation of Weispfenning's virtual term substitution method for real closed field formulas of unbounded degree. We build upon a recent high-performance library for computing over non-Archimedean real closed fields using Thom's Lemma.
. .
Collaborative Verification-Driven Engineering of Hybrid Systems {Abstract} Hybrid systems with both discrete and continuous dynamics are an important model for real-world physical systems. The key challenge is how to ensure their correct functioning with respect to safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven engineering. Despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is thus not uncommon for verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) graphical (UML) and textual modeling of hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification efforts.
. .
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals {Abstract} Recent applications of decision procedures for nonlinear real arithmetic (the theory of real closed fields, or RCF) have presented a need for reasoning not only with polynomials but also with transcendental constants and infinitesimals. In full generality, the algebraic setting for this reasoning consists of real closed transcendental and infinitesimal extensions of the rational numbers. We present a library for computing over these extensions. This library contains many contributions, including a novel combination of Thom's Lemma and interval arithmetic for representing roots, and provides all core machinery required for building RCF decision procedures. We describe the abstract algebraic setting for computing with such field extensions, present our concrete algorithms and optimizations, and illustrate the library on a collection of examples.
. .
Geometric Relevance Filtering for Real-Closed Field Arithmetic {Abstract} Nonlinear real arithmetic (the theory of real closed fields, or RCF) is crucial to the formal verification of cyber-physical systems (CPS). Though RCF is decidable, it is fundamentally infeasible (hyperexponential in the number of variables). This infeasibility is a serious practical concern, as modern CPS verification tools such as KeYmaera and MetiTarski make heavy use of nonlinear real arithmetic decision procedures, generating hundreds or thousands of many-variable RCF subproblems during their proof search. As these verification tools progress upon a proof, they accumulate a large database of RCF facts which pertain to the system being analyzed. As subsequent RCF subproblems are generated, they are tested for validity modulo this database of background facts. In this work, we exploit the fact that, in practice, often only a small subset of the background RCF facts are needed to decide the generated subproblems. The difficulty is in how the most relevant facts should be selected. We present an RCF decision method which combines sampling techniques and cell decomposition methods adapted from cylindrical algebraic decomposition to use geometric information to select relevant background facts. We illustrate its performance upon real-world benchmark problems drawn from KeYmaera and MetiTarski verification efforts.
. .
A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems {Abstract} Hybrid systems with both discrete and continuous dynamics are an important model for real-world physical systems. The key challenge is how to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner and formal verification to prove their correctness, forming the vision of verification-driven engineering. Despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires significant human guidance, since hybrid systems verification tools work over an undecidable theory. It is thus not uncommon for verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) modeling hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification tasks.
. .
The Strategy Challenge in SMT Solving {Abstract} High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems (e.g., SMT-LIB benchmarks), they may easily perform very badly on new classes of problems not anticipated by solver developers. This issue is becoming increasingly pressing as SMT solvers begin to gain the attention of practitioners in diverse areas of science and engineering. In many cases, changes to the prover heuristics can make a tremendous difference in the success of SMT solving within new problem domains. Classically, however, much of the control of these heuristics has been outside the reach of solver end-users. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence, through research undertaken with the tools RAHD and Z3, that the adaptation of ideas of strategy prevalent within both Argonne-style theorem provers and the LCF-influenced interactive theorem proving community can go a long way towards realizing this goal. In the process, we solidify some foundations for strategy in the context of SMT and pose a number of challenge problems.
. .
Real Algebraic Strategies for MetiTarski Proofs
{Abstract} MetiTarski is an automatic theorem prover that can prove inequalities involving sin, cos, exp, ln, etc. During its proof search, it generates a series of subproblems in nonlinear polynomial real arithmetic which are reduced to true or false using a decision procedure for the theory of real closed fields (RCF). These calls are often a bottleneck: RCF is fundamentally infeasible. However, by studying these subproblems, we can design specialised variants of RCF decision procedures that run faster and improve MetiTarski's performance.
. .
Abstract Partial Cylindrical Algebraic Decomposition I: The
Lifting Phase {Abstract} Though decidable, the theory of real closed fields (RCF) is fundamentally infeasible. This is unfortunate, as automatic proof methods for nonlinear real arithmetic are crucially needed in both formalised mathematics and the verification of real-world cyber-physical systems. Consequently, many researchers have proposed fast, sound but incomplete RCF proof procedures which are useful in various practical applications. We show how such practically useful, sound but incomplete RCF proof methods may be systematically utilised in the context of a complete RCF proof method without sacrificing its completeness. In particular, we present an extension of the RCF quantifier elimination method Partial CAD (P-CAD) which uses incomplete $\exists$ RCF proof procedures to ``short-circuit'' expensive computations during the lifting phase of P-CAD. We present the theoretical framework and preliminary experiments arising from an implementation in our RCF proof tool RAHD.
. . Impugning Randomness, Convincingly {Abstract} John organized a state lottery, and his wife won the main prize. You may feel that the event of her winning wasn't particularly random, but how would you argue that in a fair court of law? Traditional probability theory does not even have the notion of random events. Information complexity theory does, but it is not applicable to real-world scenarios like the lottery one. We attempt to rectify that.
. . Combined Decision Procedures for Nonlinear Arithmetics,
Real and Complex
{Abstract}
We describe contributions to algorithmic proof techniques for deciding the satisfiability of boolean combinations of many-variable nonlinear polynomial equations and inequalities over the real and complex numbers. In the first half, we present an abstract theory of Groebner basis construction algorithms for algebraically closed fields of characteristic zero and use it to introduce and prove correct Groebner basis methods specialised to the needs of modern satisfiability modulo theories (SMT) solvers. In the process, we use the technique of proof orders to derive a generalisation of S-polynomial superfluousness in terms of transfinite induction along an ordinal parameterised by a monomial order. We use this generalisation to prove the abstract (``strategy-independent'') admissibility of a number of superfluous S-polynomial criteria important for efficient basis construction. Finally, we consider local notions of proof minimality for weak Nullstellensatz proofs and give ideal-theoretic methods for computing complex ``unsatisfiable cores'' which contribute to efficient SMT solving in the context of nonlinear complex arithmetic. In the second half, we consider the problem of effectively combining a heterogeneous collection of decision techniques for fragments of the existential theory of real closed fields. We propose and investigate a number of novel combined decision methods and implement them in our proof tool RAHD (Real Algebra in High Dimensions). We build a hierarchy of increasingly powerful combined decision methods, culminating in a generalisation of partial cylindrical algebraic decomposition (CAD) which we call Abstract Partial CAD. This generalisation incorporates the use of arbitrary sound but incomplete (semi-)decision procedures for the existential theory of real closed fields as functional parameters for ``short-circuiting'' the lifting phase of CAD. Identifying the decision procedure parameters used during lifting formally with RAHD proof strategies, we implement the method in RAHD for the case of full-dimensional cell decompositions and investigate its efficacy with respect to a collection of proof strategy parameters and the Brown-McCallum projection operator. We end with some wishes for the future.
. . Groebner Basis Construction Algorithms Based on Theorem Proving Saturation Loops
{Abstract} We present novel Groebner basis algorithms based on saturation loops used by modern superposition theorem provers. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver.
. . Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations
{Abstract} RAHD is a tool that takes advantage of a heterogeneous collection of proof procedures to decide the satisfiability of formulas in the existential fragment of the theory of real closed fields. But system analysts can rarely restrict themselves only to arithmetic-based problems: they might want to use RAHD as part of a more diverse formal toolbox. In this paper, we present ongoing work on an architecture that enables the skeptical integration of RAHD into general-purpose proof assistants. We will present a system-level view of how this integration can be performed, and examine efficiency concerns for this implementation.
. . Superfluous S-polynomials in Strategy-Independent Groebner Bases
{Abstract} Using the machinery of proof orders originally introduced by Bachmair and Dershowitz in the context of canonical equational proofs, we give an abstract, strategy-independent presentation of Groebner basis procedures and prove the correctness of two classical criteria for recognising superfluous S-polynomials, Buchberger's criteria 1 and 2, w.r.t. arbitrary fair and correct basis construction strategies. To do so, we develop a general method for proving the strategy-independent correctness of superfluous S-polynomial criteria which seems to be quite powerful. We also derive a new superfluous S-polynomial criterion which is a generalisation of Buchberger-1 and is proved to be correct strategy-independently.
. . On Locally Minimal Nullstellensatz Proofs {Abstract} Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Groebner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction.
. . Universality of Polynomial Positivity and a Variant of
Hilbert's 17th Problem {Abstract} We observe that the decision problem for the existential theory of real closed fields (RCF) is simply reducible to the decision problem for RCF over a connective-free universal language in which the only relation symbol is a strict inequality. In particular, every existential RCF sentence phi can be settled by deciding a proposition of the form ``polynomial p (which is a sum of squares) takes on strictly positive values over the reals,'' with p simply derived from phi. Motivated by this observation, we pose the goal of isolating a syntactic criterion characterising the positive definite (i.e., strictly positive) real polynomials. Such a criterion would be a strictly positive analogue to the fact that every positive semidefinite (i.e., non-negative) real polynomial is a sum of squares of rational functions, as established by Artin's positive solution to Hilbert's 17th Problem. We then prove that every positive definite real polynomial is a ratio of a Real Nullstellensatz witness and a positive definite real polynomial. Finally, we conjecture that every positive definite real polynomial is a product of ratios of Real Nullstellensatz witnesses and examine an interesting ramification of this conjecture.
. . Note: This paper contains an obselete description of the RAHD system. Combined Decision Techniques for the Existential Theory
of the Reals {Abstract} Methods for deciding quantifier-free non-linear arithmetical conjectures over \mathbb{R} are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over \mathbb{R} is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have ``sweet spots'' -- e.g., types of problems for which they perform much better than they do in general. Such ``sweet spots'' can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation. RAHD (``Real Algebra in High Dimensions'') is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective ``sweet-spots.'' We discuss high-level mathematical and design aspects of RAHD and illustrate its use on a number of examples.
. . Proving SPARK Verification Conditions with SMT
Solvers {Abstract} We have constructed a tool for using SMT (SAT Modulo Theories) solvers to discharge verification conditions (VCs) from programs written in the SPARK language. The tool can drive any solver supporting the SMT-LIB standard input language and has API interfaces for some solvers. SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. Formal verification of SPARK programs is supported by tools produced by the UK company Praxis High Integrity Systems. We report in this paper on our experience in proving SPARK VCs using the popular SMT solvers CVC3, Yices, Z3 and Simplify. We find that the SMT solvers can prove virtually all the VCs that are discharged by Praxis's prover, and sometimes more. Average run-times of the fastest SMT solvers are observed to be roughly 1-2x that of the Praxis prover. Significant work is sometimes needed in translating VCs into a form suitable for input to the SMT solvers. A major part of the paper is devoted to a detailed presentation of the translations we implement.
. . Does SAT Exhibit Fractal Behavior? {Abstract} In this paper we study the structure of the set SAT of all satisfiable propositional logical formulas. In particular we raise the question whether the distribution of SAT within the set A of all propositional formulas exhibits fractal behavior. This answer is of course relative to a metric on A. We show that for one such metric there is strong evidence that the distribution does indeed behave wildly. Next we look at an alternative metric.
. . Diophantine Sets and Their Decision Problems
{Abstract} We shall examine the genesis and proof of the Davis-Putnam-Robinson-Matiyasevich negative solution to Hilbert's Tenth Problem, and then proceed to prove a handful of elementary new results on definability and decidability in <\mathbb{N}, *>. |