Machine Assisted Proof [video](youtube.com)
youtube.com
Machine Assisted Proof [video]
https://www.youtube.com/watch?v=AayZuuDDKP0
20 comments
> 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.
can you fix this? even with the (sic) I have no idea what you are trying to say here.
can you fix this? even with the (sic) I have no idea what you are trying to say here.
I think it's just that the word "generate" isn't supposed to be there:
However, they are increasingly being used to assist human mathematicians in a variety of creative ways, beyond just brute-force case checking or computation.That's literally what the slide says. Your guess is as good as mine, and my guess is that there's an extra word, "generate"
Probably. The talk covers many computer-assisted proofs where the big problem was a huge case analysis. The cases have to be generated and machine checked. The proof of the four-color theorem (1,482 cases) was the first major proof like that. It upset many mathematicians.
Why did it upset? Machines are just tools. Is using something beyond a pen and a paper considered a cheating. There are some problems where the easiest way is to just to use brute force. The God's number (the maximum moves to solve the Rubik's cube from any state) was calculated with brute force. If you can formally verify an algorithm I see no problem.
I'm a mathematician, although I'm too young to have been around for this. I feel like I might be able to add a little cultural perspective, though.
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.
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.
https://en.wikipedia.org/wiki/Sic
> in full: sic erat scriptum, "thus was it written"
> in full: sic erat scriptum, "thus was it written"
The coolest thing about Machine Assisted Proofs is the idea of expanding collaborators on a single large problem by orders of magnitude by breaking up work into small machine-verifiable pieces.
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).
[1] https://en.wikipedia.org/wiki/Inter-rater_reliability
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).
[1] https://en.wikipedia.org/wiki/Inter-rater_reliability
How is that something only AI unlocks?
verifying/enforcing standards on inputs is not something that only AI unlocks, but LLMs are an example of huge step forward in this kind of work and I was expressing my general enthusiasm for the new tools we now have for these sorts of problems. We can turn relatively subjective content into much more computable semi-objective ratings through simple prompting (e.g. rate X on a scale of 0.0 to 1.0), which is valuable for all sorts of use cases. I'm using it right now for my work.
Tao explicitly mentions that it is ITPs that unlock this.
The ITPs will keep the LLMs in check, and stop them from bs-ing.
The ITPs unlock massive collaboration.
The ITPs will keep the LLMs in check, and stop them from bs-ing.
The ITPs unlock massive collaboration.
Um yes ITPs are the unlock for specifically math collaboration. I was referring to other more subjective fields that can also benefit from tech that allows collaboration to scale. LLMs have value for those. For math, LLMs suck.
May I ask how you are using it or what you are getting it to rate?
Rating content in a dataset to determine if we need to review it as I'm standardizing a large dataset right now to improve user experience. It's a relatively mundane activity but I think this is tentatively a good method. I've been exploring ways to use it for a bunch of ideas, like distance between ideas and reflecting back to users on how their messages might land with others. I think this idea of accelerating self reflection is a big use case for AI.
This sounds interesting. Are there other examples of this out in the wild? Any plans to blog/write about it? I'm curious to learn more.
I haven't seen any tho I haven't really been looking. Mostly it's messing with prompts and looking at data. I hope to write about it eventually, tho probably in the context of the self reflection use case. I don't think a lot of people are barking up this tree yet and it's important.
It's refreshing to see someone like Terence Tao embrace GPT-4 as an assistant.
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.
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.
An observation I've made is that people that were early adopters and effective users of web search such as AltaVista or these days Google are also good at using LLMs.
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.
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.
DonHopkins(1)
Could you tell me some typical uses beyond just asking for code snippets? I'm an NLP researcher, and currently I still find myself using Google for other types of information seeking. I'm working on NLG decoding algorithms currently.
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.
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.
I’ll often ask GPT to explain a concept to me, but giving it a hint as to my existing level of knowledge in the subject area. With Google, you’re likely to get the most popular page on a topic; not the page that is appropriate for people with your expertise.
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.
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.
Hmm, I tried some questions which would have been relevant to me in the recent past, and it flubbed pretty hard on all of them. Even worse, instead of just saying it doesn't know it generates semi-plausible babbling or adjacent but not actually helpful knowledge.
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.
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.
That’s an area where they genuinely suck, unless there is an exact wikipedia article on the topic, readily within its training data set.
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.
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.
Reverse dictionary is a great one yeah. I think I've used it for resolving a tip-of-my tongue thing several times. For language learning I'm a bit more wary. A few times I've asked it for help with Chinese, and when I ask one of my native speaker friends they'll tell me it wasn't quite right.
Imagine you had a coworker who was like Leonardo Da Vinci and Einstein and someone with the power to access the hive mind of Reddit wrapped up in one but had dementia and sometimes spoke believably while completely hallucinating and lying, so you still needed to verify their work or take their answer and double check it.
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.
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.
> Leonardo Da Vinci and Einstein
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).
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).
It can say "let's think this through step by step", which is good enough for most cases.
I posted a few example questions (which are definitely way below Einstein level) in another comment. It's not doing too well! Do you have any links to conversations where it was particularly helpful? I do wonder if my GPT usage is bad in the same way my parents' Google usage is.
Maybe try asking your questions on phind.com. It does RAG on top of GPT4 so it might be able to base its answers on the paper or github issue you mentioned.
Well, Einstein and Da Vinci were fallible as well.
Asking for code snippets has replaced most of my Stack Overflow usage. I'd say 90% of the cases, it answers something usable. Maybe it's not relevant for an NLP researchers, but for a regular SWE like me, it's handy several times per day.
Completely agreed on this one, although it's maybe more like 70% for me. I did leave an exception for that specifically in my original comment.
Miscellaneous stuff from yesterday:
- 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.
- 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.
Just today, I took a picture of some medication my wife got because I wanted to know more about it, I also used it to lookup what Tesla probably did wrong with their CyberTruck that was causing the rusting (they likely didn't use passivated stainless), I also looked up the recommended age to give popcorn to kids since my toddlers received a small sealed bag of it for valentines. I pretty much use it all the time as a faster google. Whenever I wonder about something and want to know more, bam ChatGPT.
try asking it, reword it a few times.
> I've noticed a similar trend among folks who work on compilers, preferring to "stay in their lane" instead of embracing GPT-4
Research into ML-guided optimisation predates chatjippity.
Research into ML-guided optimisation predates chatjippity.
http://chatjippity.com/ is taken, btw
chatjippity what?
It is rather annoying because anyone who spends 15 minutes with the tool given the right context can easily learn its limitations and conclude that it’s a useful albeit imperfect tool. At this point not using an LLM in your day to day is like not using Google. Sure you can do it, but are you going to be outputting work as efficiently as possible? Wouldn’t you feel like doing your job without Google is hamstringing you a bit?
I definitely leave a lot on the table in terms of outputting work as efficiently as possible. In the past I’ve used personal wikis, time tracking software, personal project management software, etc. and it was a boon for my productivity. These days I don’t bother. I’m sure some people view chatbots the same way.
TBH my views on Google (and search engines) in general have also changed over time. The information available on the internet is surprisingly shallow. Anything related to proprietary tech, hardware, geographically local info, reverse engineering or just anything that relatively few people are working on is very hard to find.
It's not about not trusting it or "staying in your lane", LLM results for domain specific work are terrible, and additionally useless if you're writing fairly novel code (which most ML practitioners/Compiler programmers are doing if they're doing interesting work).
The usefulness of LLMs for writing code is strongly correlated with how "Stack Overflowable" your work is.
The usefulness of LLMs for writing code is strongly correlated with how "Stack Overflowable" your work is.
Theorem provers like Lean are awesome. As a software guy who admires mathematics from a safe distance, the Curry-Howard isomorphism is one of the most beautiful and surprising things I've ever seen. Programs are proofs!
Using the Curry-Howard isomorphism my program shows there is a mapping from HTTP requests to HTTP responses!
That’s far off, your program also branches to standard libraries and kernel syscalls and networking with other servers and maybe loops that aren’t guaranteed to terminate, that there are 10000s of cases where HTTP requests map to an error (bottom) instead of a response
I would like to see computational assistance for formalizing existing mathematical results. The goal would be a system that could take a paper and output its proofs in formalized form. Ultimately, this would enable us to vet all published mathematical results and deliver them as formal proofs, which could then be used as training inputs for future proof systems.
I’m not proving anything but I’m using ChatGPT to come up with MIP optimization mathematical formulations. It’s ingested all the techniques from journal papers so it actually comes up with some really solid formulations based on what I tell it. Super useful!
Fascinating! Could you give some examples?
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.
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.
Sure. Just ask ChatGPT 4 (not the free 3.5) to help you formulate some simple MIP constraints.
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?"
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?"
Nice, thanks!
It is interesting to note, apparently combining formal proof checkers with machine learning could be used to create synthetic training data for automatic self-training of proof generators. It could work something like this: https://news.ycombinator.com/item?id=38036986
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.
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.
In the same spirit of this talk, good HN post https://news.ycombinator.com/item?id=38035672 on Terry Tao's use of proof assistants and LLMs to find a paper bug https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
Part of mathematics is formalization. There's no doubt that computers will help us with proofs more and more, but there's also the "discovering" of what statements we should be taking for granted. That involves things like intuition, insight, and intention. People didn't have a "least upper bound property" hundreds of years ago, even though they were studying the real numbers.
Just wanted to remind people that we haven't sucked the human element out of math.
Just wanted to remind people that we haven't sucked the human element out of math.
Terrence talks a lot about his experiences with Lean and the field more generally on his Mastodon over at @[email protected]
Terence mentions how AI can potentially assist with finding mathematical proofs in the last few slides, but I wonder what his thoughts are on going the opposite direction, i.e., using mathematics to accelerate the development of AI. If we consider Levin search to be the “brute-force” approach to universal search, then Hutter search improves upon this by interleaving the search of algorithm/program space with a search of the space of formal mathematical proofs to find proofs of algorithmic equivalence, whereby we substitute the slower running algorithm with its faster equivalent.
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.
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.
Most interesting problems can't be solved by pure deduction. You need to construct things, and that is a leap of intuition (or LLM in case of AlphaGeometry).
On that note, I've been using ChatGPT to (re-)teach myself mathematical induction and working with proofs. It's like having my own tutor. There is huge potential here just for helping people learn new topics and skills.
I really wish I had ChatGPT when I was teaching myself programming. I wouldn’t have failed university programming courses and would have been in the workforce years faster.
Absolutely. I've been teaching myself Haskell and C++ too. For the first time in my life, learning is fun and not a dire struggle every step of the way (particularly as somebody with ADHD).
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.
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.
It's been _incredibly_ useful for bringing new Rust devs up to speed here.
With all due respect, if you couldn't get a passing grade in intro programming courses I'm not sure how much GPT would have helped. Additionally, if college was the first time getting your feet wet in programming, you were likely already years behind the curve.
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.
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.
When I was learning programming I was grateful for Stackoverflow and other internet resources. I couldn't imagine learning as quickly as I did without those resources.
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.
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.
[deleted]
I wouldn't be so reliant on AI black-boxes like ChatGPT to learn anything from medicine, law or even mathematics and you don't even trust if its outputs are even correct.
Terrance Tao doesn't even trust its outputs either and can verify if it is outputting nonsense that may look 'correct' in your eyes.
Terrance Tao doesn't even trust its outputs either and can verify if it is outputting nonsense that may look 'correct' in your eyes.
Ah, but the nice thing about constructing formal proofs is you can immediately tell if the output is correct.
Yes, but you also need to make sure the input is correct! For example, your idea of automatically formalising a paper needs to somehow make sure that the result means the same as the paper.
I don't blindly believe everything it says. I've caught it making mistakes plenty of times. But there's simply no going back anymore. There's no replacing what it can do and the kind of workflow it offers.
> to (re-)teach myself mathematical induction
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.
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.
How is this better than a mathematics book with exercises (and solutions to them at the end or in a second book)?
How do you ask a textbook a question? Exercises are great until the student is stuck at some "core concept" they could simply ask or explain their confusion and get a direct answer.
Isn't it obvious? I can't have a conversation with an exercise and the solution. ChatGPT has helped me uncover gaps in my mathematical knowledge because I can ask it questions about what something means, how something was arrived at, or how it works. Sometimes proofs involve logical "jumps" that aren't immediately or intuitively obvious, or require some mathematical maturity that I otherwise wouldn't be aware of. Something I would've otherwise needed a tutor for to determine.
GPT very naturally encourages you to write out questions. That by itself can be useful for learning. You can even get answers for your questions.
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.)
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.)
It's great that top mathematicians are now interested in machine assisted proof.
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].
[1] https://practal.com
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].
[1] https://practal.com
I've been tinkering with a hobby project lately, and I wonder how related it is to this.
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!
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!
Interesting, I wonder how this could be applied to solving any of the millennium problems.
Terence Tao is a machine to me. :)
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.