Notes from attending FLoC 2022 as a student volunteer at Haifa, Israel. There is no notes after the third day due to a combination of jet lag, exhaustion, and mild sickness.

Neural Network Verification

Shared Certificates for Neural Network Verification

  • Even two input spaces (perturbation on a single input) can be very different, at later hidden layer the transformed output spaces may still contain each other.

    • Classification output partition is very coarse comparing with input space.

  • Check subset relation between transformed output spaces at any hidden layer

  • Template is a set in a hidden layer that potentially is a super set of some input spaces after transformation. and the output space of template satisfies the robustness spec.

    • Heuristic to choose templates.

  • Improve efficiency for nn verification

Example Guided Synthesis of Linear Approximations for Neural Network Verification

  • Compute linear overapproximations for different nonlinear neuron activation functions (e.g., sigmoid)

  • Accumulate overapproximations becomes overly conservative

  • Minimize volume between linear overapproximation and true function

  • Offline synthesis (need to understand details)

  • upshift to address violation to address unsound linear approximations

    • violation is a point of true function larger/above than the line defining approximations.
    • find upper bound on the violation using nonlinear optimization encoding the true function.

Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning

  • partition the continuous state space to finite abstract states and train neural network on abstract states as input

    • Seems to be a straightforward partition (grid based)

  • Convert system with NN to Kripke structure

    • Construct an explicit state transition system
    • Get action from nn using an abstract state as input and calculate next abstract state by evaluating concrete state evolution
    • Property directed reduction/simplification on abstract transition systems
    • Need more detail?

  • Verify against ACTL (temporal logic) using existing tools

  • Refinement process?

    • This might be the most interesting part?

  • Small examples with nn controllers

Affine Loop Invariant Generation via Matrix Algebra

  • Infer loop invariants for piecewise affine transition functions as the loop body

  • Encode proof of inductive step into checking Farka’s lemma holds

    • (exists linear combination of guard and inv on prestate x) /\ loop body => the guard and inv on poststate x’
    • “exists linear combination of guard and inv on prestate x” is a nonlinear constraints

  • Two methods to synthesize invariants based on eigenvalue and matrix inverse

    • Looks simple enough to understand
    • Applications in finding our AAPs?

Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes

  • discover attributes (feature variables) instead of enumerate all

    • Use convex shapes as “separator”
    • Learn disjunction of convex constraints
    • “Join-max” separator

  • What is the maximal guarantee for the synthesized invariants?

Logic Lounge: Autonomous systems

  • Driving Policy

  • Assume
  • “Safety-net”
    • Proper response within unsafe states (safe but close to bad states)
  • Guarantee
    • If all agents apply proper response, collision avoidance is still guaranteed under unsafe states
  • Duty of care - legal obligation
    • Safety-usefulness tradeoff

Aug. 8, Monday

  • Koopman operator linearization
    • https://github.com/EthanJamesLew/AutoKoopman
  • STLmc
    • Model checking for Signal Temporal Logic over what?
    • Robustness check
      • Is it able to model stability, ISS, ultimately bounded property
    • Barrier certificates
  • UCLID5
    • SyGus with Oracle? Synthesize contract for perception/state estimation functions.

    • add assumption over input output pairs

      • f(x) = y, positive sample
      • f(x) != y, negative sample
      • I(x) ==> I(x’), inductive example
    • Satisfiability algorithm
    • Synthesis algorithm?

CAV award 2022

  • Determinism
  • Time and function are (reasonably) independent

Real time with stream input

  • Software level “Virtually Synchronous”
    • Timed Triggered Architecture~(TTA) - single rate [HK et al 90]
      • Proven correct in PVS
    • Physically asynchronous Logically synchronous~(PALS) [JM et al 09]
    • Lingua Franca~(LF) reactor model [EL et al 2019]

Problem in synchronous When deadline/delay is larger than the period (cycle time). IF we change the function to address delay, the function and time are now dependent.

Kahn Process Networks~(KPN)!!!

  • Read until all inputs are ready in FIFO queue.

  • Asynchronous Write

  • KPN is deterministic under arbitrary interleaving/fair scheduling
  • independent of computation/communication delays!!!

With well typed KPN, FIFO queue for read can be bounded. Timed KPN – KPN with timed constraints Still deterministic functions rom timed input to timed output streams.

node type -> a step function with input and output typed with segments of stream connector type -> constraints on matching segment length from producer node to consumer node.

type checking -> bounded memory and deadlock free