9 ms·

Machine Assisted Proof [video]

223 points by stefanpie 3y ago

hansonpeter 3y ago
[dead]
the_panopticon 3y ago
In the same spirit of this talk, good HN post https://news.ycombinator.com/item?id=38035672 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-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
bagels 3y ago
One hour talk, mostly going over the history of machine proofs, and machine assisted proofs. 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.
- 38 3y ago
  > 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.
  - tehnub 3y ago
    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.
  - bagels 3y ago
    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"
    - Animats 3y ago
      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.
      - senfiaj 3y ago
        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.
        nicf 3y ago
        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.
Sakos 3y ago
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.
- SOLAR_FIELDS 3y ago
  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.
  - Sakos 3y ago
    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.
    - empath-nirvana 3y ago
      It's been _incredibly_ useful for bringing new Rust devs up to speed here.
  - bongodongobob 3y ago
    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.
rq1 3y ago
Terence Tao is a machine to me. :)
jumploops 3y ago
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.
- SOLAR_FIELDS 3y ago
  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?
  - kweingar 3y ago
    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.
  - PhilipRoman 3y ago
    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.
- moonchild 3y ago
  > 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.
pfdietz 3y ago
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.
paulpauper 3y ago
Interesting, I wonder how this could be applied to solving any of the millennium problems.
munchler 3y ago
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!
- zaik 3y ago
  Using the Curry-Howard isomorphism my program shows there is a mapping from HTTP requests to HTTP responses!
  - renonce 3y ago
    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
zero-sharp 3y ago
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.
npunt 3y ago
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 https://en.wikipedia.org/wiki/Inter-rater_reliability
- pests 3y ago
  How is that something only AI unlocks?
  - npunt 3y ago
    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.
    - pests 3y ago
      May I ask how you are using it or what you are getting it to rate?
      - npunt 3y ago
wenc 3y ago
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!
- eru 3y ago
  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.
  - wenc 3y ago
    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?"
    - eru 3y ago
      Nice, thanks!
Croline79 3y ago
[flagged]
Williams77 3y ago
[dead]
Linda231 3y ago
[dead]
HanClinto 3y ago
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!
spaduf 3y ago
Terrence talks a lot about his experiences with Lean and the field more generally on his Mastodon over at @tao@mathstodon.xyz
Xcelerate 3y ago
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.
- visarga 3y ago
  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).
practal 3y ago
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 https://practal.com
cubefox 3y ago
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 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.

223 points by stefanpie 3y ago

[dead]

In the same spirit of this talk, good HN post https://news.ycombinator.com/item?id=38035672 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-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...

bagels 3y ago

One hour talk, mostly going over the history of machine proofs, and machine assisted proofs. 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.

38 3y ago
> 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.
- tehnub 3y ago
  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.
- bagels 3y ago
  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"
  - Animats 3y ago
    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.
    - senfiaj 3y ago
      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.
      - nicf 3y ago
        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.

Sakos 3y ago

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.

SOLAR_FIELDS 3y ago
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.
- Sakos 3y ago
  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.
  - empath-nirvana 3y ago
    It's been _incredibly_ useful for bringing new Rust devs up to speed here.
- bongodongobob 3y ago
  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.

rq1 3y ago

Terence Tao is a machine to me. :)

jumploops 3y ago

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.

SOLAR_FIELDS 3y ago
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?
- kweingar 3y ago
  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.
- PhilipRoman 3y ago
  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.
moonchild 3y ago
> 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.

pfdietz 3y ago

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.

paulpauper 3y ago

Interesting, I wonder how this could be applied to solving any of the millennium problems.

munchler 3y ago

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!

zaik 3y ago
Using the Curry-Howard isomorphism my program shows there is a mapping from HTTP requests to HTTP responses!
- renonce 3y ago
  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

zero-sharp 3y ago

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.

npunt 3y ago

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 https://en.wikipedia.org/wiki/Inter-rater_reliability

pests 3y ago
How is that something only AI unlocks?
- npunt 3y ago
  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.
  - pests 3y ago
    May I ask how you are using it or what you are getting it to rate?
    - npunt 3y ago

wenc 3y ago

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!

eru 3y ago
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.
- wenc 3y ago
  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?"
  - eru 3y ago
    Nice, thanks!

Croline79 3y ago

[flagged]

Williams77 3y ago

[dead]

Linda231 3y ago

[dead]

HanClinto 3y ago

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!

spaduf 3y ago

Terrence talks a lot about his experiences with Lean and the field more generally on his Mastodon over at @tao@mathstodon.xyz

Xcelerate 3y ago

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.

visarga 3y ago
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).

practal 3y ago

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 https://practal.com

cubefox 3y ago

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 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.