“Misc. stuff” posts will appear periodically. They will contain, well, miscellaneous [1] stuff – mainly links to papers and discussions which might be interesting to readers of this blog.
For each, I’ll try to explain why it is relevant [2].
Hacker News and this blog
My spec bugs post made it to the first page of Hacker News, and during one glorious 24-hour period we got ~ 6000 new readers (welcome folks).
The Hacker News discussion of that post is here. It mainly discusses the plugger incident itself, not the general question of “can simulation-based methods help prevent such spec bugs”.
Machine learning and verification
What is it: Machine learning (and especially deep learning) has experienced a huge revival in recent years. To learn more about deep learning, take a look at the Wikipedia article, or see this excellent 45-minute video by Andrew Ng explaining it all.
Why relevant for this blog: Many complex systems (which SVF should be able to verify) now use machine learning. For instance, some of the image recognition logic attached to AV’s cameras uses deep neural networks (NNs).
Machine learning (and especially NNs) present two big problems for verification:
- They work well, but it is hard to understand how they work, in the sense of “what are the rules they operate by”. As somebody said, “they don’t have a spec, they just have a résumé”. Thus it is hard to reason about them and verify them, especially in the context of a bigger system which is not all-NNs.
- A second issue concerns on-the-fly machine learning: This can be quite useful (e.g. let your AV improve as it operates), but some regulatory bodies (and hence manufacturers) don’t like it because it makes verification harder: Essentially, the machine on the road is not the same machine that was verified in the factory.
Links:
- A new paper by some Google folks about the pitfalls of machine learning: Machine Learning: The High-Interest Credit Card of Technical Debt (pdf)
It refers specifically to various verification / testing issues (e.g. of multiple configurations). Some excerpts:
The goal of this paper is highlight several machine learning specific risk factors and design patterns to be avoided or refactored where possible.
Many engineers do a great job of thinking hard about abstractions and unit tests in production code, but may treat configuration (and extension of configuration) as an afterthought. Indeed, verification or testing of configurations may not even be seen as important. Configuration by its very nature tends to be the place where real-world messiness intrudes on beautiful algorithms.
- Somewhat relevant, and beautiful: Inceptionism: Going Deeper into Neural Networks
This paper (also by Google folks) tries to “understand” how NNs work, by sort of “reversing” their operations to see what they “see”. The results are interesting, beautiful, and weird. Excerpt:
One way to visualize what goes on is to turn the network upside down and ask it to enhance an input image in such a way as to elicit a particular interpretation. Say you want to know what sort of image would result in “Banana.” Start with an image full of random noise, then gradually tweak the image towards what the neural net considers a banana”.
- Completely off-topic, but interesting: The brain as a universal learning machine
I have talked about the verification challenge of FAI (Friendly Artificial Intelligence) here. This was not an official post (rather a by-the-way page) because FAI verification is somewhat outside the range of this blog (which is already wide enough).
Well, the recent success of deep learning seems to cause quite a few people to say “So maybe the brain does work this way”. And one of the FAI folks wrote this very interesting paper, which summaries this view. Excerpt:
In this article I am going to quickly introduce the abstract concept of a universal learning machine, present an overview of the brain’s architecture as a specific type of universal learning machine, and finally I will conclude with some speculations on the implications for the race to AGI and AI safety issues in particular.
iPython and Jupyter
What is it: iPython is a way to combine text, code and the results of that code into a single document – see for instance this iPython notebook by Peter Norvig for solving the traveling salesman problem. This can be viewed as the modern incarnation of Knuth’ idea of literate programming (they call it “literate computing”).
Jupyter is a more general framework, which lets you do it for multiple languages (not just Python).
Why relevant for this blog: One of the things one would like to do within a framework like SVF is to discuss bugs, failures, simulation results, configurations and so on.
This involves writing text like this:
One potential problem with the current proposal is
. However, if we then the above failures disappear. However, then in average fuel consumption could be much worse – see produced from .
One way to write this kind of text is as a Jupyter-style notebook, which can then be hyperlinked from other such documents.
Link: Project Jupyter: Computational Narratives as the Engine of Collaborative Data Science
This new paper (really a Jupyter manifesto, but written as a grant proposal) discusses the vision of the Jupyter team to do (for the scientific community) what I would like to do for big-system architects / verifiers. Excerpts:
While standalone software libraries exist in science (say the building of a library to solve differential equations), we target a more common scenario: the iterative exploration of a problem via computation and the interactive study of intermediate results. In this kind of computational work, scientists evolve their codes iteratively, executing small test programs or fragments and using the results of each iteration as insight that informs the next step. The computations inform their understanding of their scientific questions, and those questions shape the process of computing. The nature of this process means that, for scientists, an interactive computing system is of paramount importance: the ability to execute very small fragments of code (possibly a single line) and immediately see the results is at the heart of their workflow.
Furthermore, the purpose of computation in science is precisely to advance science itself. In the famous words of R. Hamming, “the purpose of computing is insight, not numbers.” For this reason, computation in science is ultimately in service of a result that needs to be woven into the bigger narrative of the questions under study: that result will be part of a paper, will support or contest a theory, will advance our understanding of a domain. And those insights are communicated in papers, books and lectures: narratives of various formats.
The problem the Jupyter project tackles is precisely this intersection: creating tools to support in the best possible ways the computational workflow of scientific inquiry, and providing the environment to create the proper narrative around that central act of computation. We refer to this as Literate Computing, in contrast to Knuth’s concept of Literate Programming, where the emphasis is on narrating algorithms and programs. In a Literate Computing environment, the author weaves human language with live code and the results of the code, and it is the combination of all that produces a computational narrative
Notes
[1] Erik Panu and myself once came up with a great startup slogan, guaranteed to convince would-be investors of our razor-sharp focus: “Miscellaneous – that’s all we do!”.
[2] You’ll notice that the range of things I consider “relevant” is quite large. I guess I am following the footsteps of Caspar Weinberger (ex US Secretary of Defense), of whom it was said that he “never met a weapons system he didn’t like”.