Hila Peleg

Verification, in @mvechev's context, is proving there is no attack possible on the NN. But everything (inputs, networks) are too big, so we need abstraction. AI2: AI (abstract interpretation) for AI (artificial intelligence), S&P'18. #POPL

Many of the papers about abstracting neurons for analysis are in AI conference like NeurIPS and ICLR, @mvechev asks where are the PL folks? This is a pure static analysis problem. #POPL

We're still far away from verifying realistic properties, @mvechev says. There's a lot of work to be done. But what about making models less susceptible to attacks from the get go? Let's talk about training and adversarial training. #POPL

What if we add background knowledge so if you misclassify a car, you'll at least misclassify it as a truck, not a dog? @mvechev shows how this is an optimization problem (all the math). #POPL

Why are better abstractions not producing more provable networks? @mvechev hypothesizes more complex abstractions make the optimization problem more difficult, because the training process changes a lot under abstraction. And accuracy is also worse... #POPL