5 ms·

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will h

by golol 2y ago

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn basic theory building like creating auxilliary definitions and Lemmas. I really think this is the holy grail of proof-assistance and will allow us to formalize most mathematics that we create very naturally. Humans will work podt-rigorously and let the machine asisst with filling in the details.

visarga 2y ago
> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.
- Eridrus 2y ago
  Search is great, search works, but there was not a tonne to learn from the AlphaGeometry paper unless you were specifically interested in solving geometry problems.
- kypro 2y ago
  My old AI professor used to say that every problem is a search problem. The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.
  - visarga 2y ago
    For some problems validation is expensive. Like the particle collider or space telescope, or testing the COVID vaccine. It's actually validation that is the bottleneck in search not ideation.
  - pishpash 2y ago
    There's no problem with search. The goal is to search most efficiently.
    - deely3 2y ago
      You mean that by improving search we can solve any problem? What if solution field is infinite, even if we make search algo 10x100 more performant, solution field will still be infinite, no?
      - pishpash 2y ago
        Gradient descent is a search. Where does it say the search space has to be small?
  - shkkmo 2y ago
    I would argue that no actually searchable solution space is really infinite (if only because infinite turing machines can't exist). Finite solution spaces can get more than large enough to be intractable.
    - smokel 2y ago
      What about ℕ? Seems pretty infinite to me, unless with "actually" you mean finite in time and space, which would make your argument a tautology. Or am I missing something?
      - shkkmo 2y ago
        Searches happen in finite time an space and, more importantly, systems performing those searches have practical finite limits on parameters that determine size of the space within which that search can take place (such as available memory). Even within fairly modest finite limits, you can produce a solution space that cannot be significantly searched with the available finite matter and time available in the observable universe. Thus, the problem with using search isn't that solution spaces can be infinite, but that finite solution spaces can be unimaginably large.
      - lupire 2y ago
        Almost every "number" "in" N doesn't actually exist. In the search for numbers that exist, we will most likely only ever find a finite set of numbers before the Universe or humanity dies. ("Scare quotes")
- Davidzheng 2y ago
  Yes and there's a lot of search here too. That's a key to the approach
- thomasahle 2y ago
  Also AlphaProof had to search for 60 hours for one of the IMO problems it solved.
  - renonce 2y ago
    It’s going to be significantly faster very soon, we have seen how AlphaGo evolved into KataGo which is many magnitudes more compute efficient
    - thomasahle 2y ago
      The main difficulty to scaling Alpha Proof is finding theorems to train it with. AlphaGo didn't have that problem because it could generate it's own data.
  - randcraw 2y ago
    And I understand the upper time limit for each question was 4.5 hours. So it solved one question almost immediately, two well over the allotted time (60 hrs), and two not at all. No medal for you, Grasshopper.
    - snewman 2y ago
      Contestants get 4.5 hours for each of the two days of competition. They have to solve three problems in that time, so on average you can spend 1.5 hours per problem (if you're aiming to finish all three). That said, the gap from "can't do it at all" to "can do it in 60 hours" is probably quite a bit larger than the gap from 60 hours to 1.5 hours.
      - moffkalast 2y ago
        Timing something that can be ran faster by throwing better hardware at it honestly feels conceptually irrelevant, as long as the complexity is actually tractable.
- gowld 2y ago
  What makes solving IMO problems hard is usually the limits of human memory, pattern-matching, and search, not creativity. After all, these are problems that are already solved, and it is expected that many people can solve the problems in about 1 hour's time. That makes it, in principle, similar or even easier than a champsionship-level chess move, which often take more than 1 hour for a professional human (with more training than an IMO high school student) to solve. Another interesting concern is that when posing a problem to humans, it's fine to pose an "easy" brute-forceable problem, but humans, being slow brute-searchers, need to find more clever solutions. But if you give such a problem to a computer, it can trivialize it. So to test a computer, you need to pose non- easily-brute-forceable problems, which are harder for the computer than the others, but equally difficult for the humans as the other problems are.
  - sebzim4500 2y ago
    Ok but if you read the actual solutions they aren't a bizarre mess of brute force. They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).
    - lupire 2y ago
      The solutions aren't a bizarre mess of brute force. The search for the solutions is.
    - knotthebest 2y ago
      They are, though. I spoke to an author just yesterday. They did mostly use brute-force.
  - snewman 2y ago
    Why do you say these are problems that are already solved? Sure, they're often variations on existing themes, but the same is true for chess positions and, honestly, almost everything else in any field of human endeavor. Agreed that the absolute upper tier of chess players have trained longer and harder than most or all IMO contestants. Though I do wonder which (top-tier chess or the IMO) draws on a larger talent pool. To my understanding, a significant fraction of all high school students on Earth take some form of qualifying exam which can channel them into an IMO training program. And as far as the being amenable to brute force (relative difficulty for humans vs. computers): it seems that chess was comparatively easier for computers, IMO problems are comparatively easier for humans, and the game of Go is somewhere in between.
fmap 2y ago
Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. By contrast, this kind of open ended formalization is something where progress used to be extremely slow and incremental. I worked in an adjacent field 5 years ago and I cannot stress enough that these results are simply out of reach for traditional automated reasoning techniques. Real automatic theorem proving is also useful for a lot more than pure mathematics. For example, it's simple to write out an axiomatic semantics for a small programming language in lean and pose a question of the form "show that there exists a program which satisfies this specification". If this approach scales it'll be far more important than any other ML application that has come out in the last few years.
- cubefox 2y ago
  > Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. The blog post indicates the opposite. The geometry problem in the IMO problem set was solved by AlphaGeometry 2, which is an LLM based on Google's Gemini. LLMs are considered relatively general systems. But the other three solved problems were proved by AlphaProof, which is a narrow RL system that is literally based on AlphaZero, the Go and Chess AI. Only its initial (bootstrapping) human training data (proofs) were formalized and augmented by an LLM (Gemini).
  - lacker 2y ago
    AlphaGeometry is not an LLM
    - cubefox 2y ago
      It is an LLM combined with a symbolic deduction engine.
  - dash2 2y ago
    AlphaZero is more general than a Go and Chess AI, right? Isn't it a general self-play algorithm?
EugeneOZ 2y ago
No. It's like you are allowed to use search engines to find a solution, nothing more than that.
- humansareok1 2y ago
  Through a search space often large enough to be completely intractable with a galaxy wide computer.
geysersam 2y ago
I imagine a system like this to be vastly more useful outside the realm of mathematics research. You don't need to be able to prove very hard problems to do useful work. Proving just simple things is often enough. If I ask a language model to complete a task, organize some entries in a certain way, or schedule this or that, write a code that accomplishes X, the result is typically not trustworthy directly. But if the system is able to translate parts of the problem to logic and find a solution, that might make the system much more reliable.
- creata 2y ago
  But for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.
  - lanstin 2y ago
    And most applied maths doesn't seem to worry about proofs much. They have techniques that either work pretty well or blow up.
    - optimalsolver 2y ago
      Bridge collapses are a form of proof validation.
  - geysersam 2y ago
    My intuition is that a regular LLM is better att coming up with a correct task description from a fuzzy description than it is at actually solving tasks.
  - humansareok1 2y ago
    There's a lot of automated proof checkers out there. Presumably you would just run any solution from an AI through those.
benreesman 2y ago
As resident strident AI skeptic, yeah, this is real. But MCTS was always promising when married to large NNs and DeepMind/Brain were always in front on it. I don’t know who fucked up on Gemini and it’s concerning for Alphabet shareholders that no one’s head is on a spike. In this context “too big to fail” is probably Pichai. But only very foolish people think that Google is lying down on this. It’s Dean and Hassabis. People should have some respect.
sideeffffect 2y ago
People are already working on this https://leandojo.org/ https://leandojo.org/ https://machine-learning-for-theorem-proving.github.io/ https://machine-learning-for-theorem-proving.github.io/ https://www.youtube.com/watch?v=P5ew0BrRm_I https://www.youtube.com/watch?v=P5ew0BrRm_I https://paperswithcode.com/task/automated-theorem-proving https://paperswithcode.com/task/automated-theorem-proving https://old.reddit.com/r/math/comments/11mb9lx/future_of_automated_theorem_proving/ https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut... https://github.com/RiccardoBiosas/LeanGPT https://github.com/RiccardoBiosas/LeanGPT

by golol 2y ago

visarga 2y ago

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

Eridrus 2y ago
Search is great, search works, but there was not a tonne to learn from the AlphaGeometry paper unless you were specifically interested in solving geometry problems.
kypro 2y ago
My old AI professor used to say that every problem is a search problem. The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.
- visarga 2y ago
  For some problems validation is expensive. Like the particle collider or space telescope, or testing the COVID vaccine. It's actually validation that is the bottleneck in search not ideation.
- pishpash 2y ago
  There's no problem with search. The goal is to search most efficiently.
  - deely3 2y ago
    You mean that by improving search we can solve any problem? What if solution field is infinite, even if we make search algo 10x100 more performant, solution field will still be infinite, no?
    - pishpash 2y ago
      Gradient descent is a search. Where does it say the search space has to be small?
- shkkmo 2y ago
  I would argue that no actually searchable solution space is really infinite (if only because infinite turing machines can't exist). Finite solution spaces can get more than large enough to be intractable.
  - smokel 2y ago
    What about ℕ? Seems pretty infinite to me, unless with "actually" you mean finite in time and space, which would make your argument a tautology. Or am I missing something?
    - shkkmo 2y ago
      Searches happen in finite time an space and, more importantly, systems performing those searches have practical finite limits on parameters that determine size of the space within which that search can take place (such as available memory). Even within fairly modest finite limits, you can produce a solution space that cannot be significantly searched with the available finite matter and time available in the observable universe. Thus, the problem with using search isn't that solution spaces can be infinite, but that finite solution spaces can be unimaginably large.
    - lupire 2y ago
      Almost every "number" "in" N doesn't actually exist. In the search for numbers that exist, we will most likely only ever find a finite set of numbers before the Universe or humanity dies. ("Scare quotes")
Davidzheng 2y ago
Yes and there's a lot of search here too. That's a key to the approach
thomasahle 2y ago
Also AlphaProof had to search for 60 hours for one of the IMO problems it solved.
- renonce 2y ago
  It’s going to be significantly faster very soon, we have seen how AlphaGo evolved into KataGo which is many magnitudes more compute efficient
  - thomasahle 2y ago
    The main difficulty to scaling Alpha Proof is finding theorems to train it with. AlphaGo didn't have that problem because it could generate it's own data.
- randcraw 2y ago
  And I understand the upper time limit for each question was 4.5 hours. So it solved one question almost immediately, two well over the allotted time (60 hrs), and two not at all. No medal for you, Grasshopper.
  - snewman 2y ago
    Contestants get 4.5 hours for each of the two days of competition. They have to solve three problems in that time, so on average you can spend 1.5 hours per problem (if you're aiming to finish all three). That said, the gap from "can't do it at all" to "can do it in 60 hours" is probably quite a bit larger than the gap from 60 hours to 1.5 hours.
    - moffkalast 2y ago
      Timing something that can be ran faster by throwing better hardware at it honestly feels conceptually irrelevant, as long as the complexity is actually tractable.
gowld 2y ago
What makes solving IMO problems hard is usually the limits of human memory, pattern-matching, and search, not creativity. After all, these are problems that are already solved, and it is expected that many people can solve the problems in about 1 hour's time. That makes it, in principle, similar or even easier than a champsionship-level chess move, which often take more than 1 hour for a professional human (with more training than an IMO high school student) to solve. Another interesting concern is that when posing a problem to humans, it's fine to pose an "easy" brute-forceable problem, but humans, being slow brute-searchers, need to find more clever solutions. But if you give such a problem to a computer, it can trivialize it. So to test a computer, you need to pose non- easily-brute-forceable problems, which are harder for the computer than the others, but equally difficult for the humans as the other problems are.
- sebzim4500 2y ago
  Ok but if you read the actual solutions they aren't a bizarre mess of brute force. They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).
  - lupire 2y ago
    The solutions aren't a bizarre mess of brute force. The search for the solutions is.
  - knotthebest 2y ago
    They are, though. I spoke to an author just yesterday. They did mostly use brute-force.
- snewman 2y ago
  Why do you say these are problems that are already solved? Sure, they're often variations on existing themes, but the same is true for chess positions and, honestly, almost everything else in any field of human endeavor. Agreed that the absolute upper tier of chess players have trained longer and harder than most or all IMO contestants. Though I do wonder which (top-tier chess or the IMO) draws on a larger talent pool. To my understanding, a significant fraction of all high school students on Earth take some form of qualifying exam which can channel them into an IMO training program. And as far as the being amenable to brute force (relative difficulty for humans vs. computers): it seems that chess was comparatively easier for computers, IMO problems are comparatively easier for humans, and the game of Go is somewhere in between.

fmap 2y ago

Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. By contrast, this kind of open ended formalization is something where progress used to be extremely slow and incremental. I worked in an adjacent field 5 years ago and I cannot stress enough that these results are simply out of reach for traditional automated reasoning techniques. Real automatic theorem proving is also useful for a lot more than pure mathematics. For example, it's simple to write out an axiomatic semantics for a small programming language in lean and pose a question of the form "show that there exists a program which satisfies this specification". If this approach scales it'll be far more important than any other ML application that has come out in the last few years.

cubefox 2y ago
> Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. The blog post indicates the opposite. The geometry problem in the IMO problem set was solved by AlphaGeometry 2, which is an LLM based on Google's Gemini. LLMs are considered relatively general systems. But the other three solved problems were proved by AlphaProof, which is a narrow RL system that is literally based on AlphaZero, the Go and Chess AI. Only its initial (bootstrapping) human training data (proofs) were formalized and augmented by an LLM (Gemini).
- lacker 2y ago
  AlphaGeometry is not an LLM
  - cubefox 2y ago
    It is an LLM combined with a symbolic deduction engine.
- dash2 2y ago
  AlphaZero is more general than a Go and Chess AI, right? Isn't it a general self-play algorithm?

EugeneOZ 2y ago

No. It's like you are allowed to use search engines to find a solution, nothing more than that.

humansareok1 2y ago
Through a search space often large enough to be completely intractable with a galaxy wide computer.

geysersam 2y ago

I imagine a system like this to be vastly more useful outside the realm of mathematics research. You don't need to be able to prove very hard problems to do useful work. Proving just simple things is often enough. If I ask a language model to complete a task, organize some entries in a certain way, or schedule this or that, write a code that accomplishes X, the result is typically not trustworthy directly. But if the system is able to translate parts of the problem to logic and find a solution, that might make the system much more reliable.

creata 2y ago
But for it to be 100% trustworthy, you'd have to express correctness criteria for those simple tasks as formal statements.
- lanstin 2y ago
  And most applied maths doesn't seem to worry about proofs much. They have techniques that either work pretty well or blow up.
  - optimalsolver 2y ago
    Bridge collapses are a form of proof validation.
- geysersam 2y ago
  My intuition is that a regular LLM is better att coming up with a correct task description from a fuzzy description than it is at actually solving tasks.
- humansareok1 2y ago
  There's a lot of automated proof checkers out there. Presumably you would just run any solution from an AI through those.

benreesman 2y ago

As resident strident AI skeptic, yeah, this is real. But MCTS was always promising when married to large NNs and DeepMind/Brain were always in front on it. I don’t know who fucked up on Gemini and it’s concerning for Alphabet shareholders that no one’s head is on a spike. In this context “too big to fail” is probably Pichai. But only very foolish people think that Google is lying down on this. It’s Dean and Hassabis. People should have some respect.

sideeffffect 2y ago

People are already working on this https://leandojo.org/ https://leandojo.org/ https://machine-learning-for-theorem-proving.github.io/ https://machine-learning-for-theorem-proving.github.io/ https://www.youtube.com/watch?v=P5ew0BrRm_I https://www.youtube.com/watch?v=P5ew0BrRm_I https://paperswithcode.com/task/automated-theorem-proving https://paperswithcode.com/task/automated-theorem-proving https://old.reddit.com/r/math/comments/11mb9lx/future_of_automated_theorem_proving/ https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut... https://github.com/RiccardoBiosas/LeanGPT https://github.com/RiccardoBiosas/LeanGPT