Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
101
Of particular interest for the synthesis of Lyapunov functions, is the ability of
Z3 to solve polynomial constraints. Z3 stores and exactly manipulates algebraic
real numbers that are roots of rational univariate polynomials: this is done for
an algebraic real α, by storing a polynomial p(x) for which p(α) = 0 and two
rationals l, u such that p(x) = 0 for x ∈ (l, u) if and only if x = α. In this work,
Z3 has been used through its Python APIs, named Z3Py. An example of a simple
assertion verification follows.
Example 2 (Assertion in Z3). Consider the (valid) formula x ≥ 0 ⇒ 3x + 1 > 0.
The code using Z3Py results in:
x = Real('x')
s = Solver()
s.add(Implies(x >= 0, 3 * x + 1 > 0))
print(s.check())
which evaluates (as expected) to SAT.
2.3 Inductive Synthesis - CEGIS
An approach to solve second-order logic problems, such as those characterising
the synthesis of Lyapunov functions, is inductive synthesis (IS). IS infers general
rules (or functions) from specific examples (observations), entailing the process of
generalisation. Within the IS procedure, a synthesiser attempts the construction
from a (usually small) subset of the original specifications. It then generalises to
the complete specification by identifying patterns in the input data.
An exemplar of IS is the CEGIS framework. Fig. 1 depicts the relation between its two main components. It sets off with a given specification ψ over a
set I for the synthesis. The synthesis engine (a component that will be also denoted as learner ) provides a candidate solution for ι, a subset of I, the space of
possible inputs. This candidate solution is passed to a second component, called
verifier, that acts as an oracle: either it approves the solution over the entire I,
so that the process terminates, or it finds an instance ¯
x (a counterexample in
I) where the candidate solution does not comply with the specifications. The
learner takes ¯
x and adds it to ι, computing a new (more general) candidate solution for the problem. This cycle is repeated. Note that this algorithm might not
terminate, depending on the structure of I, or might take many cycles to find
a proper solution: in those instances, tailored candidate solutions and insightful
counterexamples are necessary. In this work, the IS is implemented using SMTsolvers. The verifier finds counterexamples ¯
x by seeking a witness of the negated
formula ¬ψ, namely trying to prove that a violation of the formula exists. The
learner might employ SMT solvers to solve the system of constraints generated
by the counterexamples, i.e. to find a valid instance of such constraints, however
in general it does not need to be sound, as it is the verifier that guarantees
the soundness of the proposed solution. Section 3.1 illustrates the two CEGIS
components, the learner L and the verifier Z in relation to Lyapunov function
synthesis.
101
Of particular interest for the synthesis of Lyapunov functions, is the ability of
Z3 to solve polynomial constraints. Z3 stores and exactly manipulates algebraic
real numbers that are roots of rational univariate polynomials: this is done for
an algebraic real α, by storing a polynomial p(x) for which p(α) = 0 and two
rationals l, u such that p(x) = 0 for x ∈ (l, u) if and only if x = α. In this work,
Z3 has been used through its Python APIs, named Z3Py. An example of a simple
assertion verification follows.
Example 2 (Assertion in Z3). Consider the (valid) formula x ≥ 0 ⇒ 3x + 1 > 0.
The code using Z3Py results in:
x = Real('x')
s = Solver()
s.add(Implies(x >= 0, 3 * x + 1 > 0))
print(s.check())
which evaluates (as expected) to SAT.
2.3 Inductive Synthesis - CEGIS
An approach to solve second-order logic problems, such as those characterising
the synthesis of Lyapunov functions, is inductive synthesis (IS). IS infers general
rules (or functions) from specific examples (observations), entailing the process of
generalisation. Within the IS procedure, a synthesiser attempts the construction
from a (usually small) subset of the original specifications. It then generalises to
the complete specification by identifying patterns in the input data.
An exemplar of IS is the CEGIS framework. Fig. 1 depicts the relation between its two main components. It sets off with a given specification ψ over a
set I for the synthesis. The synthesis engine (a component that will be also denoted as learner ) provides a candidate solution for ι, a subset of I, the space of
possible inputs. This candidate solution is passed to a second component, called
verifier, that acts as an oracle: either it approves the solution over the entire I,
so that the process terminates, or it finds an instance ¯
x (a counterexample in
I) where the candidate solution does not comply with the specifications. The
learner takes ¯
x and adds it to ι, computing a new (more general) candidate solution for the problem. This cycle is repeated. Note that this algorithm might not
terminate, depending on the structure of I, or might take many cycles to find
a proper solution: in those instances, tailored candidate solutions and insightful
counterexamples are necessary. In this work, the IS is implemented using SMTsolvers. The verifier finds counterexamples ¯
x by seeking a witness of the negated
formula ¬ψ, namely trying to prove that a violation of the formula exists. The
learner might employ SMT solvers to solve the system of constraints generated
by the counterexamples, i.e. to find a valid instance of such constraints, however
in general it does not need to be sound, as it is the verifier that guarantees
the soundness of the proposed solution. Section 3.1 illustrates the two CEGIS
components, the learner L and the verifier Z in relation to Lyapunov function
synthesis.