Loop Invariant Synthesis
withMachine Learning
Taro Sekiyama
National Institute of Informatics
Including joint work with
Unno Hiroshi, Naoki Kobayashi, Issei Sato,
Kohei Suenaga, Takeshi Tsukada, Minchao Wu

Software verification & Machine learning

Softwareverification

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

Machinelearning

2

Software verification & Machine learning

Softwareverification

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

Machinelearning

3

Accidents caused by software bugs
♦ Therac-25 radiation therapy◊ Involved six accidents of radiation overdoses♦ Ariane 5 rocket◊ Resulted in the launch failure anda loss > $370 million♦ Heartbleed (an OpenSSL vulnerability)◊ Major servers (Apache, nginx, etc.)
on the internet were vulnerable♦ Others: List of software bugs (Wikipedia)
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

4

Program verification
Methodology to assure correctness of programsby mathematical reasoning
int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1; }return y; }Program 𝑷 has been provento work as specified by 𝝍
Program 𝑷
OK

Specification 𝝍

Verification tool∀n ∈ ℕ. P n = σni=0 i
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

5

Program verification
Methodology to assure correctness of programsby mathematical reasoning
int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1; }return y; }A counterexample that witnesses
𝑷 doesn’t work as specified by 𝝍
Program 𝑷
NGSpecification 𝝍

Verification tool∀n ∈ ℕ. P n = σni=0 i
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

6

Difference from software testing
Program verification♦ Executable Specification♦ Logical Specification∀n ∈ ℕ. P n

Software testing= σni=0 i♦ Assuring correctness for any input
Input Correctness Assured

assert (P(1) == 1);
assert (P(2) == 3);
assert (P(5) == 15);

♦ Assuring correctness for given inputs
Input Correctness Assured

1

✓

1

✓

2

✓

2

✓

3

✓

3



Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

7

Verification of real-world software♦ SLAM: a research project to verify Windows device drivers♦ Infer: a verification tool for Java, C, and C++ code
◊ Used to verify Facebook’s Android / iOS apps

♦ CPAcheker: a verification tool for C◊ Used to verify control software of airplanes and a space station♦ Astree: a verification tool for C◊ Used to verify Linux device drivers
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)8

in Hoare Logic

Let’s try verification!

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

9

Example: sum from 1 to n
Goal

Specification

Proving “y = σn𝑖=0 𝑖“ holds after
exiting from the loops (★)∀n ∈ ℕ. P n = σni=0 i

ProgramQuestion

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
★ return y;}}?

What holds during the loops?

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

10

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

11

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

12

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

13

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

14

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

15

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}= σn𝑖=𝑥+1 𝑖xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

is a property that holds before / after every loop

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

16

Example: sum from 1 to nSpecification∀n ∈ ℕ. P n = σni=0 i

Programint P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
return y;}= σn𝑖=𝑥+1 𝑖xy

Before the loopn0After the 1st loopn-1nAfter the 2nd loopn-2

n + n-1

After the 3rd loopn-3

n + n-1 + n-2

…

…

0

n + n–1 + n-2 + … + 1

After the nth loop

σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

is a property that holds before / after every loop

Loop invariant

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

17

Example: sum from 1 to n
Goal

Specification

Proving “y = σn𝑖=0 𝑖“ holds after
exiting from the loops (★)∀n ∈ ℕ. P n = σni=0 i

ProgramAnswer

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
★ return y;}}✓

Loop invariant
𝜙 𝑥, 𝑦 ≡ σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

Proof of the goal
The final loop exits with x = 0, so
𝜙 0, 𝑦 ≡ σ0𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (0 ≥ 0)
holds

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)18

Example: sum from 1 to n
Goal

Specification

Proving “y = σn𝑖=0 𝑖“ holds after
exiting from the loops (★)∀n ∈ ℕ. P n = σni=0 i

ProgramAnswer

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
★ return y;}}✓

Loop invariant
𝜙 𝑥, 𝑦 ≡ σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

Proof of the goal
The final loop exits with x = 0, so
𝜙 0, 𝑦 ≡ σ𝟎𝒊=𝟎 𝒊 + 𝒚 = σ𝒏𝒊=𝟎 𝒊 ∧ (0 ≥ 0)
holds

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

19

Example: sum from 1 to n
Goal

Specification

Proving “y = σn𝑖=0 𝑖“ holds after
exiting from the loops (★)∀n ∈ ℕ. P n = σni=0 i

ProgramAnswer

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
★ return y;}}✓

Loop invariant
𝜙 𝑥, 𝑦 ≡ σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

Proof of the goal
The final loop exits with x = 0, so
𝜙 0, 𝑦 ≡ σ𝟎𝒊=𝟎 𝒊 + 𝒚 = σ𝒏𝒊=𝟎 𝒊 ∧ (0 ≥ 0)
holds

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)20

Example: sum from 1 to n
Goal

Specification

Proving “y = σn𝑖=0 𝑖“ holds after
exiting from the loops (★)∀n ∈ ℕ. P n = σni=0 i

ProgramAnswer

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1;}
★ return y;}}✓

Loop invariant
𝜙 𝑥, 𝑦 ≡ σx𝑖=0 𝑖 + 𝑦 = σ𝑛𝑖=0 𝑖 ∧ (𝑥 ≥ 0)

Proof of the goal ✓The final loop exits with x = 0, so
𝜙 0, 𝑦 ≡ σ𝟎𝒊=𝟎 𝒊 + 𝒚 = σ𝒏𝒊=𝟎 𝒊 ∧ (0 ≥ 0)
holds

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)21

Challenge in automating verification
Finding loop invariants♦ It is an undecidable problem in general♦ (Incomplete) approaches to invariant synthesis◊ Learning-based approaches◊ Template-based approaches◊ Fixing the shape of invariants and searching for parameters thatsatisfy constraints on invariants
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

22

Learning framework for invariant synthesis
Interleaving learning and checking of invariant candidates
Logical constraint 𝑪
on loop invariants
Invariant candidate 𝜙Teacher

LearnerCounterexample 𝒄 to 𝜙(𝜙(𝒄) doesn’t satisfy 𝑪)

No candidateNG

𝜙 is aninvariant

OK
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

23

Learning framework for invariant synthesis
Interleaving learning and checking of invariant candidates
Logical constraint 𝑪
on loop invariants

Machine Learning!

Implemented by
SAT/SMT solvers

Invariant candidate 𝜙Teacher

LearnerCounterexample 𝒄 to 𝜙(𝜙(𝒄) doesn’t satisfy 𝑪)

No candidateNG

𝜙 is aninvariant

OK
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)24

Invariant learning

Specification

Program∀n ∈ ℕ. P n = σni=0 i

int P(int n) {int x = n, y = 0;
while (x != 0) {y = y + x;
x = x - 1; }return y; }Goal: To find a loop invariant 𝜙Given:

A set 𝓔 of counterexamples to candidates, categorized into:♦ Positive examples: 𝒄 s.t. 𝜙(𝒄) must be true
In P, ∀𝑛 ≥ 0. 𝜙 𝑥 ≔ 𝑛, 𝑦 ≔ 0, 𝑛 must be true as invariants must hold before entering the loops♦ Negative examples: 𝒄 s.t. 𝜙(𝒄) must be false𝑛In P, 𝜙 𝑥 ≔ 0, 𝑦 ≔ 10, 𝑛 ≔ 2 must be false as y = Σ𝑖=0
𝑖 must hold after exiting the loops♦ Implication constraints: (𝒄, 𝒅) s.t. 𝜙(𝒄) ⟹ 𝜙(𝒅)Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)25

ML-based approaches to invariant learning♦ ML to lean invariants◊ Learning invariants as decision trees[Krishna, Puhrsch & Wies, arXiv’15; Garg, Neider, Madhusudan & Roth, POPL’16]◊ Learning by deep reinforcement learning[Si, Dai, Raghothaman, Naik & Song, NeurIPS’18]◊ Encoding constraints into neural networks[Ryan, Wong, Yao, Gu & Jana, ICLR’20 & PLDI’20]♦ ML to aid symbolic reasoning◊ Speeding up symbolic approaches withreinforcement learning[Tsukada, Unno, Sekiyama & Suenaga, arXiv’21]
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)26

ML-based approaches to invariant learning♦ ML to lean invariants◊ Learning invariants as decision trees[Krishna, Puhrsch & Wies, arXiv’15; Garg, Neider, Madhusudan & Roth, POPL’16]◊ Learning by deep reinforcement learning[Si, Dai, Raghothaman, Naik & Song, NeurIPS’18]◊ Encoding constraints into neural networks[Ryan, Wong, Yao, Gu & Jana, ICLR’20 & PLDI’20]♦ ML to aid symbolic reasoning◊ Speeding up symbolic approaches withreinforcement learning[Tsukada, Unno, Sekiyama & Suenaga, arXiv’21]
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)27

Learning invariants as decision trees

Decision tree
learning

Example set 𝓔

Converting tological formula

Decision tree

Invariant candidate

𝑝1

𝑝1 ⟹ ¬𝑝2 ∧ (¬𝑝1 ⟹ 𝑝3 )

𝑝2

𝑝3

− +

+ −

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)28

Nodes are predicates over program variables

Learning invariants as decision
trees
Challenge: poor scalability ofE.g., for integer-manipulating programs,
every node 𝒑𝒊 is an inequation 𝒂 ⋅ 𝒙 ≥ 𝒄♦ 𝒙 are program variables of integers♦ 𝒂, 𝒄 are parameters to be optimized
Optimizing 𝒂, 𝒄in each node

Example set 𝓔

decision tree learning in
the number of parameters 𝒂, 𝒄

Decision tree
learning

Converting tological formula

Decision tree

Invariant candidate

𝑝1

𝑝1 ⟹ ¬𝑝2 ∧ (¬𝑝1 ⟹ 𝑝3 )

𝑝2

𝑝3

− +

+ −

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)29

Solution to scalability♦ Pre-synthesizing predicates used as nodes
Decision tree
learning

Example set 𝓔

Selecting nodes fromgiven predicates

Converting tological formula

Decision tree

Invariant candidate

𝑝1

𝑝1 ⟹ ¬𝑝2 ∧ (¬𝑝1 ⟹ 𝑝3 )Set of predicates 𝒑𝒊
𝑝2

𝑝3

− +

+ −

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)30

Solution to scalability♦ Pre-synthesizing predicates used as nodes?

Decision tree
learning

Example set 𝓔

Selecting nodes fromgiven predicates

Converting tological formula

Decision tree

Invariant candidate

𝑝1

𝑝1 ⟹ ¬𝑝2 ∧ (¬𝑝1 ⟹ 𝑝3 )Set of predicates 𝒑𝒊
𝑝2

𝑝3

− +

+ −

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

31

Neural synthesis of predicates over integers[Kobayashi, Sekiyama, Sato & Unno, SAS’21]
Synthesis fromthe weights 𝑎𝑖
in the NN
4

3

-

5

3

+

6

3

-

…

…

…

Training

𝑎11

...

label

...

𝑥2

...

𝑥1

𝑎𝑛2

Example set 𝓔

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

𝑥1 + 𝑥2 + 9 > 0,
4𝑥1 − 𝑥2 > 0,…

Predicates usedin DT learning32

tree learning with
Predicate synthesis from NNs Decisionsynthesized predicates togenerate invariant candidates
Idea: Designing a NN that encodes invariants andrepresents predicate parameters 𝑎,
Ԧ 𝑐 as weights

Assumption: Formulas are logical combinations of 𝑎 ⋅ 𝑥 + 𝑐 > 0
𝑦𝑖 = 𝜎 𝑎𝑖 ⋅ 𝑥 + 𝑐𝑖 , so𝑦𝑖 ≃ 1 ⟺ 𝑎𝑖 ⋅ 𝑥 + 𝑐𝑖 > 0
𝑦𝑖 ≃ 0 ⟺ 𝑎𝑖 ⋅ 𝑥 + 𝑐𝑖 < 0
if |𝑎𝑖 ⋅ 𝑥 + 𝑐𝑖 | ≫ 0(e.g., (p1 ∨ 𝑝2 ) ∧ (𝑝3 ∨ 𝑝4 ))

𝑎11

𝑦1
𝑦2

𝑥1

Grouping the ratios
𝑎𝑖1 ∶ 𝑎𝑖2 ∶ 𝑐𝑖
𝑎𝑖2

𝑜𝑖

𝑐𝑖

2∶3∶9

4∶1∶0

𝑎82

Feedforward NN with 2 hidden layers

𝑎𝑖1

...

𝑦8

...

𝑥𝑛

...

...

0

2𝑥1 + 3𝑥2 + 9 > 0,
4𝑥1 + 1𝑥2 + 0 > 0𝑦1

𝜎 : sigmoid function
1

𝑦𝑖 ≈ 𝑝𝑖

Intended to recognize
logical combinations𝑦8
33

Experiments♦ Predicate synthesis works well on linear invariants
Positive
Negative♦ Quadratic invariants can be supported by preprocessing
inputs to the NN

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)34

ML-based approaches to invariant learning♦ ML to lean invariants◊ Learning invariants as decision trees[Krishna, Puhrsch & Wies, arXiv’15; Garg, Neider, Madhusudan & Roth, POPL’16]◊ Learning by deep reinforcement learning[Si, Dai, Raghothaman, Naik & Song, NeurIPS’18]◊ Encoding constraints into neural networks[Ryan, Wong, Yao, Gu & Jana, ICLR’20 & PLDI’20]♦ ML to aid symbolic reasoning◊ Speeding up symbolic approaches withreinforcement learning[Tsukada, Unno, Sekiyama & Suenaga, arXiv’21]
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)35

Template-based symbolic invariant synthesis
Invariant learnerConstraint 𝑪
Example set 𝑬
Invariant template 𝑻 (parameterized over

# of Boolean combinators, bounds of 𝑎,Ԧ 𝑐, etc.)¬∃𝝓
Extending 𝑻
by a heuristic

Synthesizing candidate 𝜙 byinstantiating parameters in 𝑻

Invariant candidate𝜙OK

TeacherCounterexample 𝒄to the candidate 𝜙Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)36

Template-based symbolic invariant synthesis
Invariant learnerConstraint 𝑪
Example set 𝑬
Invariant template 𝑻 (parameterized over

# of Boolean combinators, bounds of 𝑎,Ԧ 𝑐, etc.)¬∃𝝓
Extending 𝑻
by a heuristic

Synthesizing candidate 𝜙 byinstantiating parameters in 𝑻

Invariant candidate𝜙OK

TeacherCounterexample 𝒄to the candidate 𝜙♦Challenge: finding effective heuristics for template extension♦Approach: applying reinforcement learning to optimize
heuristic strategies
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)37

Reinforcement learning
Learning strategies of agent’s actions to maximize total
rewards obtained from environments
Agent

ActionEnvironmentState & Reward

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

38

Applying to heuristic learning
Goal: learning template extension strategies to minimize
the total time spent by invariant synthesis
Agent

ActionEnvironment
Invariant learner

Extendingtemplate 𝑻

Synthesizing
candidate 𝜙 from 𝑻

TeacherState & Reward

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

39

Applying to heuristic learning
Goal: learning template extension strategies to minimize
the total time spent by invariant synthesis
Decides which part of 𝑇 is enlarged
Agent

ActionEnvironment
Invariant learner

Extendingtemplate 𝑻

Synthesizing
candidate 𝜙 from 𝑻

TeacherState & Reward
Human-engineered features oftemplate 𝑻 and example set 𝑬

ー1 × (Time spent on verification)

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)40

Experiments♦ Implemented on a verifier PCSat [Unno+, AAAI’20&CAV’21]♦ Effective heuristics can be learned!
Tool# of solved test problems (total # = 171)

PCSat w/ Advantage Actor-Critic

154 (90.05%)

PCSat w/ Monte Carlo155 (90.06%)

LoopInvGen

92 (53.80%)

CVC4111 (64.91%)

Eldarica

131 (76.61%)

PCSat w/ the hand-tuned heuristic

144 (84.21%)

HoIce

149 (87.13%)

Spacer165 (96.49%)

Ours: PCSat withlearned heuristics

Baseline

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

41

Outline
1. Introduction to program verification
2. Learning-based invariant synthesis

3. Conclusion

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

42

Findings
Applying ML to verification is possible but hard
♦ Program verification is deductive,
while ML is inductive“Softer” program verification
is more suitable to use ML?

♦ Program verification addresses hard constraints,
while some of ML techs target only soft constraints♦ Needing a means to interpret / explain ML models logically◊ E.g., converting decision trees to logical formulas,extracting predicates from weights in a neural net♦ Available are only small datasets (of the sizes from 10 to 1000)
Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

43

Conclusion♦ A main bottleneck of automating verification isinvariant synthesis♦ Data-driven invariant synthesis is emerging!
♦ Collaboration b/w ML and verification is promisingand challenging
Softwareverification?

Machinelearning

Loop Invariant Synthesis with Machine Learning / Taro Sekiyama (NII)

44