This paper made me afraid of AI for the first time

Originally written: October 7th, 2020

I'd never really ever been afraid of AI and ML. Perhaps it's because I've worked in ML. Whenever people tell me that AI is going to replace our jobs and take over the world, I think of this meme:

A meme image that has a

Jokes aside, current machine learning techniques only allow models to learn very specific set of behaviors. They can be very good at their specific task, i.e. AlphaGo, but no artificial knowledge can currently emulate humans' "general intelligence".

That's not to say artificial intelligence hasn't caused disruptive impacts. Facial recognition is a practically solved problem, and privacy concerns are the only thing holding back potential mass surveillance. Neural machine translation has completely transformed the field of machine translation, unfortunately rendering decades of work by statistical machine translation researchers no longer releveant

So, I didn't really think much of when I saw the recent GPT-f paper. Recently Open AI released the natural language generating model GPT-3, and it led to some fun results like the model producing a graphing calculator or a HTML generator. It was incredibly powerful, but I didn't feel like it was a conceptually groundbreaking development. Naturally, I didn't expect much from the GPT-f paper, either. I noticed Ilya Sutskever -- the co-author of AlexNet, the model that sparked the deep learning revolution in 2012 -- listed as a co-author, but besides that, I didn't notice anything amiss.

But then I read the paper.

The paper describes the GPT-f model, a deep learning model based on GPT-3 set out to "prove theorems" using the Metamath proof assistant. In a conceptual simplification, it's GPT-3 fine-tuned to theorem and github data; on a high level, it doesn't devise a groundbreakingly new training strategy or an algorithm. It doesn't get everything right: it was only able to close 56.22% of proofs. Which is more than twice the previous state of the art (21.16%), but it isn't not something you're going to feed questions expecting the correct solution.

However, the amazing contribution of this model was that it was actually able to shorten 23 proofs in Metamath's library -- in ways humans had not done before! GPT-f delivered concise proofs in ways previously unknown. The deep learning system actually had an effective contribution to formal mathematics -- perhaps a field that seems to require the most "reasoning".

Now, we know that GPT-f doesn't really reason, but only generates from training data. However, the result is still astonishing -- much like AlphaGo, it doesn't matter that it can't reason, it can still give you the answer.

I used to think that machine learning would have limited success in things that had to be 100% correct: proofs, code generation, etc. However, I come to realize that actually, we humans are fallible as well. Andrew Wiles, the person who proved Fermat's Last Theorem, originally published an incorrect proof. It took him another year and almost giving up until he resolved the proof. Humans make mistakes. We'd like compilers and operating systems to be perfect, as so much depend on them, but we can't create programs without bugs.

So, even though maching learning, by its nature, can never reach 100% accuracy, that might not matter. 99% might be better than what we humans can do. And with enough training data and sophisticated models, we might be able to get there. This scares me.

Obviously, we are still so far away from I, Robot (how are we going to clean up all the data to train it?), but the GPT-f paper has made me realize that with enough data and sophisticated models, maybe machine learning can do everything. It doesn't matter that they can't "reason". They can still produce the right answers.

Perhaps we'll all have to be machine learning engineers. Perhaps one day AI code generation and program synthesis will be so good that it'll write code that has fewer bugs than what we can write. Currently, we're nowhere near there, and this has a host of other problems -- creating specification to program training data, or ways to fix certain parts of the model -- but we are, actually, getting there.