Thoughts on “An Abstraction-Refinement Approach to Verification of Artificial Neural Networks”

Neural networks (NNs) have become a ubiquitous machine learning technique in a wide range of domains. In 2003, some researchers surveyed the literature on verification of NNs and concluded that they “represent a class of systems that do not fit into the current paradigms of software development and certification”. Wondering if that was still the case after the NN renaissance that’s taken place over the last ten years or so, I began looking for recent work on verifying interesting properties of neural networks. The first relevant paper I found in the software verification literature was “An Abstraction-Refinement Approach to Verification of Artificial Neural Networks”, by Luca Pulina and Armando Tacchella, which appeared in CAV 2010. Here are some thoughts on that paper.

Thoughts on “Adversarial examples in the physical world”

In machine learning, computers “learn” by being shown lots of examples; for instance, we might use millions of pictures to train a model that can identify pictures of cats. The idea is that if we do a good job training the model, then it should be able to correctly identify new cat pictures (that is, ones it never saw during training) most of the time.

But it’s possible to take a picture that the model classifies correctly as being of a cat, and then tweak that picture very slightly in a way that would be undetectable to a human, but that fools the same model into classifying it with high confidence as, say, a philodendron. These subtly tweaked images are called adversarial examples, and there are known techniques for generating lots of them. Such techniques rely on making tiny, precise perturbations to the original correctly-classified example.

The saga of Accumulo bug 4379

Not too long ago, I was setting up an installation of the Accumulo distributed database. At some point in the process, I ran Accumulo’s bin/ script, which printed out the following:

HADOOP_PREFIX not set cannot automatically configure LD_LIBRARY_PATH
Please remember to compile the native libraries using the bin/ script and to set the LD_LIBRARY_PATH variable in the /home/zk/accumulo/conf/ script if needed.

Publicity chair tip: use ruby-gmail to send bulk emails via Gmail

I’m currently serving a three-year term as the publicity chair for ICFP. Like many conferences, we use a Gmail account for sending publicity emails. If you’ve seen any messages on mailing lists from, those came from me (or David Van Horn before me, or Wouter Swierstra before him, or Matthew Fluet before him).

Getting into a Ph.D. program without previous research experience

Several weeks ago, I got this email from a reader of my blog:

I’ve read your blog a lot.

I have one question though. How did you get into a PhD program without previous undergrad research experience?

I’m in Nigeria studying CS and my school has virtually zero undergrad research opportunities, at least not in my area of interest – Compilers and Programming Languages.

I want to become a researcher in Programming Languages. I’m in my second year (undergrad) and I’m working through SICP and writing a compiler for JavaScript in Python.

I need your advice desperately about what I should be doing now to would help my chances of landing an admission into grad school.

Thank you.

I don’t necessarily feel obligated to respond to every cold email I get, but this one grabbed me. I’ve been obsessing for weeks about how to answer this question effectively. This post is what I’ve come up with so far. I recognize that my advice on this topic may not be helpful to everyone, and I’m interested in hearing other researchers’ answers to the question.