Skip to content

Latest commit

 

History

History
148 lines (131 loc) · 6.25 KB

README.md

File metadata and controls

148 lines (131 loc) · 6.25 KB

symexe4dnn

How to run

navigate to ./src directory, and run the following:

python se.py <input>

Currently, we have a couple hardcoded input under ./example.

Examples

  1. python se.py ../example/toy/4x3_1.py

    This is a toy DNN example that has 4 inputs, 3hidden layers, and 4 neurons at each layer (12 ReLU neurons). SE is able to scale on these kind of small networks.


    Running Symexe4DNN on this example 
    $ python se.py ../example/toy/4x3_1.py

=========SE started=========
layer: 0
        inputs: ['i0', 'i1']
layer: 1
        inputs: ['n00', 'n01', 'n02', 'n03']
layer: 2
        inputs: ['n10', 'n11', 'n12', 'n13']
layer: 3
        inputs: ['n20', 'n21', 'n22', 'n23']
============================
DONE:
2       inputs
4       layers
2       outputs
time used: 
0.007296120000319206 s
symbolic states obtained
And(n00 ==
    If(1*i0 + 1*i1 + 1/10 <= 0, 0, 1*i0 + 1*i1 + 1/10),
    n01 ==
    If(1/2*i0 + 1/2*i1 + 1/5 <= 0, 0, 1/2*i0 + 1/2*i1 + 1/5),
    n02 ==
    If(3/2*i0 + 0*i1 + 3/10 <= 0, 0, 3/2*i0 + 0*i1 + 3/10),
    n03 ==
    If(0*i0 + 3/2*i1 + 2/5 <= 0, 0, 0*i0 + 3/2*i1 + 2/5),
    n10 ==
    If(1/2*n00 + -1/2*n01 + 0*n02 + 1*n03 + 1 <= 0,
    0,
    1/2*n00 + -1/2*n01 + 0*n02 + 1*n03 + 1),
    n11 ==
    If(-1/2*n00 + 1/10*n01 + 2*n02 + -3*n03 + -2 <= 0,
    0,
    -1/2*n00 + 1/10*n01 + 2*n02 + -3*n03 + -2),
    n12 ==
    If(1/2*n00 + -1/5*n01 + 2/5*n02 + 1*n03 + 3 <= 0,
    0,
    1/2*n00 + -1/5*n01 + 2/5*n02 + 1*n03 + 3),
    n13 ==
    If(-1/2*n00 + 1/10*n01 + 6/5*n02 + -1/2*n03 + -4 <= 0,
    0,
    -1/2*n00 + 1/10*n01 + 6/5*n02 + -1/2*n03 + -4),
    n20 ==
    If(1/2*n10 + -1/5*n11 + 1/2*n12 + 1/2*n13 + -1 <= 0,
    0,
    1/2*n10 + -1/5*n11 + 1/2*n12 + 1/2*n13 + -1),
    n21 ==
    If(-1/2*n10 + 1/10*n11 + 11/10*n12 + -1*n13 + 1 <= 0,
    0,
    -1/2*n10 + 1/10*n11 + 11/10*n12 + -1*n13 + 1),
    n22 ==
    If(1/2*n10 + -1/5*n11 + -1/2*n12 + 1/5*n13 + 1 <= 0,
    0,
    1/2*n10 + -1/5*n11 + -1/2*n12 + 1/5*n13 + 1),
    n23 ==
    If(-1/2*n10 + 1/10*n11 + 11/10*n12 + 2*n13 + -1 <= 0,
    0,
    -1/2*n10 + 1/10*n11 + 11/10*n12 + 2*n13 + -1),
    o0 == 1/2*n20 + 1/2*n21 + -2/5*n22 + 1*n23 + 1,
    o1 == -1/5*n20 + -1/2*n21 + 11/10*n22 + 2*n23 + 1)

=========SE finished=========

  2. python se.py ../example/acasxu/acasxu_1.py

    This is a DNN taken from the ACASXU flight navigation benchmark. This network has 5 in/outputs and 6 hidden layers each with 50 ReLU neurons (300 ReLu neurons). We are able to generate the symbolic state of this network, but the symbolic state is too large for the solver(z3) to solve.

    Sample in/output 
    $ python se.py ../example/acasxu/acasxu_1.py
=========SE started=========
layer: 0
        inputs: ['i0', 'i1', 'i2', 'i3', 'i4']
layer: 1
        inputs: ['n00', 'n01', 'n02', 'n03', 'n04', 'n05', 'n06', 'n07', 'n08', 'n09', 'n010', 'n011', 'n012', 'n013', 'n014', 'n015', 'n016', 'n017', 'n018', 'n019', 'n020', 'n021', 'n022', 'n023', 'n024', 'n025', 'n026', 'n027', 'n028', 'n029', 'n030', 'n031', 'n032', 'n033', 'n034', 'n035', 'n036', 'n037', 'n038', 'n039', 'n040', 'n041', 'n042', 'n043', 'n044', 'n045', 'n046', 'n047', 'n048', 'n049']
layer: 2
        inputs: ['n10', 'n11', 'n12', 'n13', 'n14', 'n15', 'n16', 'n17', 'n18', 'n19', 'n110', 'n111', 'n112', 'n113', 'n114', 'n115', 'n116', 'n117', 'n118', 'n119', 'n120', 'n121', 'n122', 'n123', 'n124', 'n125', 'n126', 'n127', 'n128', 'n129', 'n130', 'n131', 'n132', 'n133', 'n134', 'n135', 'n136', 'n137', 'n138', 'n139', 'n140', 'n141', 'n142', 'n143', 'n144', 'n145', 'n146', 'n147', 'n148', 'n149']
layer: 3
        inputs: ['n20', 'n21', 'n22', 'n23', 'n24', 'n25', 'n26', 'n27', 'n28', 'n29', 'n210', 'n211', 'n212', 'n213', 'n214', 'n215', 'n216', 'n217', 'n218', 'n219', 'n220', 'n221', 'n222', 'n223', 'n224', 'n225', 'n226', 'n227', 'n228', 'n229', 'n230', 'n231', 'n232', 'n233', 'n234', 'n235', 'n236', 'n237', 'n238', 'n239', 'n240', 'n241', 'n242', 'n243', 'n244', 'n245', 'n246', 'n247', 'n248', 'n249']
layer: 4
        inputs: ['n30', 'n31', 'n32', 'n33', 'n34', 'n35', 'n36', 'n37', 'n38', 'n39', 'n310', 'n311', 'n312', 'n313', 'n314', 'n315', 'n316', 'n317', 'n318', 'n319', 'n320', 'n321', 'n322', 'n323', 'n324', 'n325', 'n326', 'n327', 'n328', 'n329', 'n330', 'n331', 'n332', 'n333', 'n334', 'n335', 'n336', 'n337', 'n338', 'n339', 'n340', 'n341', 'n342', 'n343', 'n344', 'n345', 'n346', 'n347', 'n348', 'n349']
layer: 5
        inputs: ['n40', 'n41', 'n42', 'n43', 'n44', 'n45', 'n46', 'n47', 'n48', 'n49', 'n410', 'n411', 'n412', 'n413', 'n414', 'n415', 'n416', 'n417', 'n418', 'n419', 'n420', 'n421', 'n422', 'n423', 'n424', 'n425', 'n426', 'n427', 'n428', 'n429', 'n430', 'n431', 'n432', 'n433', 'n434', 'n435', 'n436', 'n437', 'n438', 'n439', 'n440', 'n441', 'n442', 'n443', 'n444', 'n445', 'n446', 'n447', 'n448', 'n449']
layer: 6
        inputs: ['n50', 'n51', 'n52', 'n53', 'n54', 'n55', 'n56', 'n57', 'n58', 'n59', 'n510', 'n511', 'n512', 'n513', 'n514', 'n515', 'n516', 'n517', 'n518', 'n519', 'n520', 'n521', 'n522', 'n523', 'n524', 'n525', 'n526', 'n527', 'n528', 'n529', 'n530', 'n531', 'n532', 'n533', 'n534', 'n535', 'n536', 'n537', 'n538', 'n539', 'n540', 'n541', 'n542', 'n543', 'n544', 'n545', 'n546', 'n547', 'n548', 'n549']
============================
DONE:
5       inputs
7       layers
5       outputs
time used: 
0.7024715990010009 s
symbolic states obtained
(smt formula omitted)
...

=========SE finished=========
1. Generating random inputs and obtain outputs
failed to solve
2. Simulating concrete execution
failed to solve
=============     =============
=============DONE:============

dependencies

  • z3-solver

If you want to try the ACASXU example, you will need the following packages

  • onnx
  • onnx2pytorch
  • torch

A conda envs is provided: envs.yaml