Machine Assisted Proof [video]
youtube.com
youtube.com
Conclusions (from slides at 49:56)
Computers by themselves still seem unlikely to resolve major mathematical problems on their own.
However, they are increasingly being used to generate (sic) assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.
For instance, we have seen they can be useful at generating conjectures or uncovering intriguing mathematical phenomena.
Automated provers could also be used to explore the space of proofs itself, beyond the small set of "human-generatable" proofs that often require one to stay close to other sources of intuition, such as existing literature or connections to other ways of thinking.
While AI technology shows great potential, in the immediate term, I expect it to have the most impact on tasks peripheral to mathematical research rather than central to it, such as automatically summarizing large amounts of literator or suggesting related work.
Proof formalization continues to make steady improvements in speed and ease of use. The "de Brujin factor" (the ratio between the difficulty of writing a correct formal proof and a correct informal proof) is still well above one (I estimate ~ 20), but dropping. Once AI integration takes place, this factor could potentially drop below one, which would be transformative to our field.
can you fix this? even with the (sic) I have no idea what you are trying to say here.
However, they are increasingly being used to assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.My impression is that most of the people who were "upset" didn't think that the result was false, or even that the work that went into the Four Color Theorem didn't constitute a proof. It's more that we mathematicians tend to like a proof more when it helps us understand why a fact is true rather than just that a fact is true. So an argument that ends with "and then we checked thousands of cases on a computer and it turned out they all worked" feels unsatisfying, since it feels like it doesn't fully explain what's going on.
> in full: sic erat scriptum, "thus was it written"
This to me is one of the exciting core capabilities that AI unlocks: the ability to verify/enforce a set of standards across many inputs. It's one of the information age's core problems. One example used a lot in social sciences is inter-rater reliability (IRR) [1]. There's probably a lot of domains out there that can benefit from this pattern of machines verifying distributed human inputs, both in crunch the numbers like machine assisted proofs, as well as more subjective domains where subjectivity can be extremely carefully defined.
I'd love to see more AI tooling focused on these kinds of large scale multi-contributor problem solving methods, including the idea of knowing how to correctly state the overall problem (I believe this was an example in the video).
The ITPs will keep the LLMs in check, and stop them from bs-ing.
The ITPs unlock massive collaboration.
Edit: are they interactive theorem provers?
A few friends of mine (who are ML practitioners!) still don't trust LLMs or find them useful in their day-to-day work.
I've noticed a similar trend among folks who work on compilers, preferring to "stay in their lane" instead of embracing GPT-4. The opposite appears true among those who work on user-facing applications, adoption of LLMs is much higher in their day-to-day.
Research into ML-guided optimisation predates chatjippity.
I see a lot of people saying it's replaced some large fraction of their search usage, but they generally don't explain what type of queries they're making.
For instance, if I want to know about extreme ultraviolet lithography and I tell GPT-4 that I have a degree in engineering and that I studied advanced optics, the explanation is much richer in useful detail, going way beyond what any of the pages I could find on Google would reveal.
If you wander off of that knowledge sphere, and you are not sufficiently knowledgeable yourself about the topic, it can tell you some really stupid stuff.
Nonetheless, I do use it quite regularly in everyday life, as it is basically the best reverse dictionary (that works for any language) there is. For work (programming), I didn’t find a better use case than sometimes passing it a list of stuff, giving it an example on the first element on what I want, and using it to generate it for the rest of the elements.
But that is <1% of what I do each day.
I decided to give it another go and ask GPT-4 three questions which I needed to get answers to within the last few months.
Asking conceptually about DPO: https://chat.openai.com/share/6611454c-60de-4317-811b-2b7f31... - In this one it completely leaves out the actual trick which enables DPO, so I would say it has almost no information content. Someone who didn't know what DPO is and read this would incorrectly think that they had learned something. - To learn about this, the right place was to read the original DPO paper, and some follow-up work
Asking about FSDP compatibility with LoRA: https://chat.openai.com/share/5f8892ea-61e6-496f-abda-d5a8ad... - In this one it just says a bunch of generic vague things without answering the question. - The right place to learn the answer to this is diving through Github issue comments
Asking for details the MegaBlocks mixture-of-experts setup: https://chat.openai.com/share/c010e630-ba08-407e-afb3-03df99... - Again it's just saying generic stuff which is relevant to mixture-of-experts in general, but it leaves out everything that actually makes the MegaBlocks MoE different from a generic MoE idea - For this one I had to do a combination of reading the paper and the MegaBlocks repo
So 0/3 and pretty dramatically. I was actually expecting it to get at least one of those. As far as I can tell, it didn't really do anything different based on me specifying my background either. I'd love to see any links to productive conversations that people can share.
Now imagine they have zero problem with you interrupting them to ask the stupidest question or the most profound, difficult question, as long as you want, and if you don't like their answer you can tell them to try again. And they don't care how often you do either.
What kinds of questions might you ask that coworker in the course of your work? It's highly individual.
Then it would be able to logically reason, which it absolutely can’t do.
It’s a next generation search engine, which is very good at language-related tasks (and translating a python code it has in its training set to your language is a language task, that’s why it can be applicable to certain programming tasks).
- Copy pasted terms & conditions of a website into GPT-4 context and asked it to find the answer to a question I had.
- Copy pasted a law into GPT-4 context to check if some activity was not illegal. Hallucinations can be avoided by asking it to recite the relevant lines, then you can CTRL+F for it to double check.
- Research medical condition to point me in a vague direction
- Create shell script and desktop shortcut with custom png, to launch an application with certain parameters
- Ask perplexity.ai for the best github library for a thing I wanted to do
- Upload github library to https://app.getonboardai.com/chat and ask it questions.
- A handful of smaller things. Any error message or blocker goes straight into GPT-4.
Almost every criticism of generative chat AI that I've seen in forums is someone holding it wrong, the direct equivalent of troubleshooting by searching for the term "my PC crashed" instead of a specific error code or whatever.
Similarly, the people complaining about ChatGPT not being very good don't realise they're using the free-tier v3.5 instead of the paid GPT4 that's much smarter. The equivalent is people who use the default browser (IE) and use the default search engine (Bing) and complain that "the Internet is not useful".
Just recently I had to review a bunch of legacy C# code, and I've found GPT4 to be enormously useful. It can find bugs and security issues in seconds, will suggest fixes to them, explain why they're bad, etc...
Note that I don't have to trust it to write security-bug-free code! I'm asking it to find bugs that I will then fix myself.
The usefulness of LLMs for writing code is strongly correlated with how "Stack Overflowable" your work is.
I tried to teach GPT about an algorithm I come up with to run a sequence of min-heap operations in O(n) (instead of O(n log n)). But I could not make it understand. But that was also a brand new concept built on top of some pretty niche literature (Chazelle's Soft Heap); so GPT would have to actually 'think', instead of just regurgitate papers.
My prompt was: (and it gave me the right answer)
"I have to formulate an MIP. I have a list of items i \in I each belong to groups g \in G. They are related by a static parameter G_{ig} which says if i in g, then 1 else 0. I want each item i to be freely and independently assigned to slots c \in C. However I want to keep items i together with other items in the same group if possible -- it's a soft preference.
How do i write the mathematical MIP formulation?"
Since formal proof checkers provide a reward signal (correct/incorrect proof) the above process could scale to superhuman performance in generating proofs for conjectures. This is unlike ordinary language models, which only try to imitate the human-written training distribution.
Just wanted to remind people that we haven't sucked the human element out of math.
But can we do even better? Terence touches upon automated theorem proving, which to some degree formalizes the notion of searching proof space. Once formalized, this becomes its own area of mathematics, where now the goal is to find proofs of the fastest ways to search the subset of proofs relevant to fast proof-finding.
It’s always been a bit odd to me that we defaulted to considering probabilistic approaches to universal search rather than mathematical ones; these are all mathematical structures at the core of it after all, so I would think deduction would be much more effective than induction in this domain. But then again, who knows—GPT seems to be quickly getting better at providing novel intuitive ideas to explore. And I guess induction is actually kind of necessary when determining which potential path of deduction to explore.
Another question is whether there exist algorithms that are the most efficient at solving particular classes of problems but unprovably so within any reasonable formal system, in which case automated theorem proving wouldn’t help. I kind of doubt it though. And in that case, brute-force search certainly isn’t going to find those algorithms either, so they may as well not exist within our “lightcone” of reachable algorithms that could be used to accelerate universal search.
The only exception would be if these algorithms do exist and are actually dense in program space—in that case I suppose you would then have to optimize the balance of time spent between searching proof space and algorithm space. Again, I would intuitively think this possibility is highly unlikely, and so we should instead spend all of our time on improving machine assisted proof systems if we want to accelerate AI development via improvements to universal search.
Need to know how to handle building a C++ project or dependencies? No longer have to go through dozens of posts on Reddit or DO or pages upon pages of documentation. I can just ask, then focus on what I actually want to learn.
Confused about some bizarre syntax in Haskell that gives me nothing on Google? Just ask. Don't understand how a function is constructed? Don't need to figure out what the correct terms are in what combination to find out what I'm looking at. Want a step by step explanation? Easy.
Even though it's far from perfect and I have plenty to complain about, it's already a valuable part of my everyday life with its impact on how I learn new things and experiment.
I'm not trying to be nasty, but for loops, variables, the concept of program flow etc are very elementary concepts that many children and teens are fully capable of teaching themselves, even pre-internet.
I think ChatGPT could pass any intro programming course so I have a hunch that it's just going to lead to lots of cheating and poor programming skills.
Did you end up sticking it out? Grats if so and you're probably better off for not having had ChatGPT hold your hand. For me, the temptation to just have it pass my classes for me would have been way too tempting. It's too good at boilerplate programming which is every programming 101 project.
"Write me an employee tracking system in java." Change up the comments and boom done with the assignment.
It's the same with LLMs. Now I don't have to wait hours or days for someone on SO or Reddit to read and respond to my question. Or spend who knows how long Googling for a similar - but not the SAME - question and trying to bend their solution to my problem.
And for a well trodden basic technique like mathematical induction, GPT is probably 'smart' enough to be able to explain everything.
Basically, most questions a beginner might have are already covered in something like Stack Overflow, so GPT 'just' has to give you the right cached answer, instead of coming up with new thoughts of its own. (This is very hand-wave-y.)
Induction is just set membership. Every inductive proof looks like this:
1. There's a set, S.
2. There's a scalar value, e, in S.
3. e has property p.
4. There is a function, f, from S to S.
5. f preserves property p.
6. Every element of S can be reached from e by repeated application of f. (Often because S is defined to consist of e plus f(x) for any x in S.)
---------
7. Therefore, every element of S has property p.
Terrance Tao doesn't even trust its outputs either and can verify if it is outputting nonsense that may look 'correct' in your eyes.
Love that my name appears in the talk (in small print) :-D
Now I just have to somehow find funding for my project, Practal [1].
I've been wanting to build a tool to help find and work with combos for deck builders of card games -- specifically Magic: The Gathering, but it could also apply to other games.
There is a wonderful dataset of combos available for download from Commander Spellbook -- currently boasting over 26k combos in the database, and growing all the time.
One thought I've had is to train my own embedding model so that cards that are likely to combo with each other embed closely with one other. This way, even after new cards are printed, we can rapidly discover cards that are likely to combo with them. In practice, the first attempt that I had at fine-tuning my own embedding model proved lackluster, but I intend to refine my data and try again -- possibly after pre-training.
Second thought is to fine-tune an LLM on the text of existing combos -- give it the text of each card in the combo, and then train it to predict the rest of the interactions. This is cool and all, but I don't entirely know how to train it to (reliably) give "these cards don't combo" answers -- I fear that it would tend to hallucinate for cards that don't combo, and I don't know how to handle that.
Obviously any answers that come out of this system would need to be vetted by humans before adding to the database, but it feels like this could be an interesting way to explore the game space if nothing else.
In a related way, it feels like a mathematical proof begins with a set of starting conditions, a conjecture, and then works forward using established rules. In a similar way, a combo in Magic starts with a set of starting conditions, a conjecture ("this combo will result in infinite life" or "this combo will result in infinite damage"), and then works forward to detail the process of using established rules to accomplish the conjecture.
Anyways, it's an interesting use-case to me, and I'm excited to learn more about the parallels. I don't know if my embedding model or my LLM approach are worthwhile, and I would like to learn about other tactics I might employ!