Though this particular model doesn't sound generalizable, the neuro-symbolic approach seems very promising to me:
- linking the (increasingly powerful) "system 1" tools that are most of current ML with more structured "system 2" tools, like logical proof generation, which can plan and and check the veracity / value of output.
- System 2 chugs along 'till it gets stuck, then system 1 jumps in to provide an intuitive guess on what part of state space to check next.
- Here they leveraged the ability to generate proofs by computer to create a data set of 100m proofs, enabling scalable self-supervised learning. Seem to me the symbolic domains are well formed to allow such generation of data, which while low value in each instance, might allow valuable pre-training in aggregate.
Putting these elements together is an approach that could get us quite far.
The key milestone will be moving away from the need to use specific formal / symbolic domains, and to generate a pretrained system that can generalize the skills learned from those domains.
> The key milestone will be moving away from the need to use specific formal / symbolic domains, and to generate a pretrained system that can generalize the skills learned from those domains.
You do not need to solve everything at once. This approach has the potential to revolution both math and programming by moving formal verification from being a niche tool into a regular part of every practitioners toolbox.
It also completely solves (within the domain it applies) one of the most fundamental problems of AI that the current round is calling "hallucinations"; however that solution only works because we have a non AI system to prove correctness.
At a high level, this approach is not really that new. Biochem has been using AI to help find candidate molecules, which are then verified by physical experimentation.
Combinatorical game AI has been using the AI as an input to old fasion monte carlo searches
>however that solution only works because we have a non AI system to prove correctness
But this is actually a really common scenario. Checking a solution for correctness is often much easier than actually finding a correct solution in the first place.
> however that solution only works because we have a non AI system to prove correctness.
I'm not sure why you are calling it non-AI. There's no reason why some AI system has to be some single neural network like GPT and not a hacked together conglomeration of a bunch of neural networks and symbolic logic systems. Like is it cheating to use a SAT solver? Is a SAT solver itself not artificial intelligence of a kind?
No, you can't just declare a word redefined when it is still in common usage in its correct meaning, which includes both GOFAI and deep learning/neural network approaches. AI is effect defined, not architecture defined.
Interesting that the transformer used is tiny. From the paper:
"We use the Meliad library for transformer training with its base settings. The transformer has 12 layers, embedding dimension of 1,024, eight heads of attention and an inter-attention dense layer of dimension 4,096 with ReLU activation. Overall, the transformer has 151 million parameters, excluding embedding layers at its input and output heads. Our customized tokenizer is trained with ‘word’ mode using SentencePiece and has a vocabulary size of 757. We limit the maximum context length to 1,024 tokens and use T5-style relative position embedding. Sequence packing is also used because more than 90% of our sequences are under 200 in length."
This suggests there may be some more low hanging fruit in the hard sciences for transformers to bite at, so long as they can be properly formulated. This was not a problem of scaling it seems.
It's not tiny, this is a quite normal size outside the field of LLMs, e.g. normal-sized language models, or also translation models, or acoustic models. Some people even would call this large.
“What the I.M.O. is testing is very different from what creative mathematics looks like for the vast majority of mathematicians,” he said.
---
Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.
No, the analogue of competition math here is writing programs to solve leetcode problems: they emphasize quickly and reliably applying known tools, not developing new ones.
Like I said, it's got nothing to do with computers or AI. This point of view predates any kind of AI that would be capable of doing either.
The analogy is as follows. Like with with leetcode & job interviews is as follows, to excel at math competitions one must grind problems and learn tricks, in order to quickly solve problems in a high pressure environment. And, just like how solving leetcode problems is pretty different than what a typical computer scientist or software engineer does, doing math competitions is pretty different than what a typical mathematician does.
I guess it kind of depends on what a goal post should represent. If it represents an incremental goal then obviously you are correct.
I think the ultimate goal though is clearly that AI systems will be able to generate new high-value knowledge and proofs. I think the realistically the final goal post has always been at that point.
Also if you read about the structure of AlphaGeometry, I think it's very hard to maintain that it "requires intelligence." As AI stuff goes, it's pretty comprehensible and plain.
Not a subject matter expert, so forgive me if the question is unintentionally obtuse, but It seems like a reasonable statement. They seem to be inferring that problems with existing public solutions wouldn't be a good indicator of performance in solving novel problems-- likely a more important evaluative measure than how fast it can replicate an answer it's already seen. Since you couldn't know if that solution was in its training data, you couldn't know if you were doing that or doing a more organic series of problem solving steps, therefore contaminating it. What's the problem with saying that?
Ah-- I've got super bad ADHD so I usually don't even catch things like that. I'm a terrible editor. I wouldn't be surprised if the paper authors were paying attention to this thread, and gave a call to Nature after seeing the parent comment.
I'm very curious how often the LM produces a helpful construction. Surely it must be doing better than random chance, but is it throwing out thousands of constructions before it finds a good one, or is it able to generate useful proposals at a rate similar to human experts?
They say in the paper, "Because the language model decoding
process returns k different sequences describing k alternative auxiliary
constructions, we perform a beam search over these k options, using
the score of each beam as its value function. This set-up is highly parallelizable across beams, allowing substantial speed-up when there are
parallel computational resources. In our experiments, we use a beam
size of k = 512, the maximum number of iterations is 16 and the branching factor for each node, that is, the decoding batch size, is 32."
But I don't totally understand how 512 and 16 translate into total number of constructions proposed. They also note that ablating beam size and max iterations seems to only somewhat degrade performance. Does this imply that the model is actually pretty good at putting helpful constructions near the top, and only for the hardest problems does it need to produce thousands?
My understanding is that they encoded domain in several dozens of mechanical rules described in extended data table 1, and then did transformer-guided brute force search for solutions.
The problem is that LLM as a role for drawing auxiliary lines is too inefficient. It is hard to imagine people deploying a large number of machines to solve a simple IMO problem. This field must be in the early stage of development, and much work remains unfinished
It looks like there's some interesting works to connect ML with symbolic reasoning (or searching). I'm closer to layman in this area but IIUC the latter is known to be rife with yet-to-be-understood heuristics to prune out the solution space and ML models are pretty good at this area.
I'm not in a position to suggest what needs to happen to further push the boundary, but in my impression it looks like the current significant blocker is that we don't really have a way to construct a self-feedback loop structure that consistently iterates and improves the model from its own output. If this can be done properly, we may see something incredible in a few years.
I didn't look further into their method, but it seems to me that symbolic reasoning is only important insofar as it makes the solution verifiable. That still is a glorious capability, but a very narrow one.
The real TIL (to me) is that the previous state-of-the-art could solve 10 of these! I'd heard there was a decision algorithm for plane geometry problems but I didn't know it was a practical one. Some searching turned up http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf as a reference.
Yes, and even the non-neural-network, symbolic plus linear algebra component of AlphaGeometry is able to outperform the previous state of the art. So a decent amount of work here went into the components that aren't neural networks at all.
This is nice, but I suspect that a barycentric coordinate bash with the formulas in Evan Chen's book could also do 30% of the IMO (seeing that most of it is about triangles) on a modern laptop.
It was interesting. One of the reviewers noted that one of the generated proofs didn’t seem that elegant in his opinion.
Given enough compute, I wonder how much this would be improved by having it find as many solutions as possible within the allotted time and proposing the simplest one.
The issue is that the computer-generated proofs operate at a very low level, step by step, like writing a program in assembly language without the use of coherent structure.
The human proof style instead chunks the parts of a solution into human-meaningful "lemmas" (helper theorems) and builds bodies of theory into well-defined and widely used abstractions like complex numbers or derivatives, with a corpus of accepted results.
Some human proofs of theorems also have a bit of this flavor of inscrutable lists of highly technical steps, especially the first time something is proven. Over time, the most important theorems are often recast in terms of a more suitable grounding theory, in which they can be proven with a few obvious statements or sometimes a clever trick or two.
What happens to science when the most talented kids won't be able to compete in ~2 years tops? Would our civilization reach plateau or start downward trajectory as there will be no incentive to torture oneself to become the best in the world? Will it all fade away like chess once computers started beating grandmasters?
True, but the fun is currently derived from humans going up against humans as a sport. Machines are tools (for learning or cheating) but we are not interested in competition with them.
How will it work for math, where humans do useful work right now? I can not see battle math becoming a big thing, but maybe when some of the tedious stuff goes away math will be philosophy and poking the smarter system is where entertainment can be had?
Chess was the drosophila of AI - something one could study in detail and invent newer and newer approaches to solving it. It's no longer having that function, was surpassed by Go for a brief moment until that one got solved as well. A whole generation that was raised on this drosophila is slowly fading away, for the new entrants its no longer the game to beat, more like brain stimulating fun exercise/hobby and not something capturing imagination, telling us something about the very base of our intelligence anymore.
That might be true in the number of active chess players, but it's no longer viewed as a peak intellectual game and the magic is long gone, just another intense hobby some people do, but basic machines can do better.
It’a still viewed as a peak intellectual game. And the magic is still there, just watch or listen to the fans of Magnus Carlsen when they’re viewing, discussing or analyzing his games.
Maybe not the peak intellectual game, because there are overall so many other games, digital as well, but it is unaffected from the fact that computers have beat humans.
The incentive to compete in the IMO is that it's fun to do math contests, it's fun to win math contests, and (if you think that far ahead as a high schooler) it looks good on your resume. None of that incentive will go away if the computers get better at math contests.
I'd be super demoralized if anything I could do a future pocket machine could do much better and faster. Like my very best is not enough to even tread water.
I've accepted that the human form, with its ~3 pounds of not especially optimized brainpower, is basically going to be relegated to the same status as demoscene hardware for anything that matters after this century.
That's cool by me, though. This bit of demoscene hardware experiences qualia, and that combination is weird and cool enough to make me want to push myself in new and weird directions. That's what play is in a way.
Unless you can figure out AI that is available everywhere, all the time (even in the most remote jungle with no power), there will always be value in making humans smarter
If I read their paper right, this is legit work (much more legit than DeepMind's AI math paper last month falsely advertised as solving an open math research problem) but it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence.
A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the elementary geometry context has both a necessarily elementary structure and can be easily symbolically judged as true or false. When the brute search fails, an extra geometric construction is randomly added (like adding a midpoint of a certain line) to see if brute search using that extra raw material might work. [edit: as corrected by Imnimo, I got this backwards - the brute search is just pure brute search, the transformer is used to predict which extra geometric construction to add]
Also (not mentioned in the blog post) the actual problem statements had to be modified/adapted, e.g. the actual problem statement "Let AH1, BH2 and CH3 be the altitudes of a triangle ABC. The incircle W of triangle ABC touches the sides BC, CA and AB at T1, T2 and T3, respectively. Consider the symmetric images of the lines H1H2, H2H3, and H3H1 with respect to the lines T1T2, T2T3, and T3T1. Prove that these images form a triangle whose vertices lie on W." had to be changed to "Let ABC be a triangle. Define point I such that AI is the bisector of angle BAC and CI is the bisector of angle ACB. Define point T1 as the foot of I on line BC. Define T2 as the foot of I on line AC. Define point T3 as the foot of I on line AB. Define point H1 as the foot of A on line BC. Define point H2 as the foot of B on line AC. Define point H3 as the foot of C on line AB. Define point X1 as the intersection of circles (T1,H1) and (T2,H1). Define point X2 as the intersection of circles (T1,H2) and (T2,H2). Define point Y2 as the intersection of circles (T2,H2) and (T3,H2). Define point Y3 as the intersection of circles (T2,H3) and (T3,H3). Define point Z as the intersection of lines X1X2 and Y2Y3. Prove that T1I=IZ."
>A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the elementary geometry context has both a necessarily elementary structure and can be easily symbolically judged as true or false. When the brute search fails, an extra geometric construction is randomly added (like adding a midpoint of a certain line) to see if brute search using that extra raw material might work.
I don't think this is quite right. The brute force search is performed by a symbolic solver, not the transformer. When it runs out of new deductions, the transformer is asked to suggest possible extra constructions (not randomly added).
> it's still pretty striking how far away the structure of it is from the usual idea of automated reasoning/intelligence.
How so? Reasoning is fundamentally a search problem.
The process you described is exactly the process humans use: i.e. make a guess about what's useful, try to work out details mechanically. If get stuck, make another guess, etc. So the process is like searching through a tree.
People figured out this process back in 1955 (and made a working prototype which can prove theorems): https://en.wikipedia.org/wiki/Logic_Theorist but it all hinges on using good 'heuristics'. Neural networks are relevant here as they can extract heuristics from data.
What do you think is "the usual idea of automated reasoning"? Some magic device which can solve any problem using a single linear pass?
I think the intuition here is that an “intelligent” system would lean much more heavily on the heuristics than on the search, like humans. It’s hard to quantify in this case, but certainly in the case of chess, when engines were about as good as best human players, they were doing orders of magnitude larger search than humans. Which made them feel more like chess _engines_ than chess AI. AlphaZero certainly made a step in the right direction, but it’s still far from how humans play.
The key insight is this whole thread is that this Alpha Geometry only works because the search field is not a googol combinations. So, it doesn't really generalize to many other fields of math. We shouldn't expect an AlphaCategoryTheory or AlphaNumberTheory anytime soon.
I find it rather sad that the reaction to amazing research is "but it's just..." and "it might not work on ...". Like, maybe appreciate it a bit and consider a possibility that something similar to it might work?
AlphaGeometry works, in simplified terms, in two stages:
1. Heuristically add a candidate construction using an NN (a transformer)
2. Brute force search through all possible deductions from the current set of constructions using a symbolic solver
If you don't find a solution after step 2, repeat. There may be some backtracking involved to try a different set of constructions as well.
This approach only works because, in geometry, the set of possible deductions from a given construction is actually quite small.
Also, note that this approach overall is essentially an optimization, not amazing new capabilities. Replacing step 1 with a random construction still solves 10 problems on average in the given time, compared to 30 with the new approach. The existing algorithm, relying mostly on brute force search, is probably able to solve all of the geometry problems if given, say, 10 times as much time as the olympiad students (so not some absurd amount of time).
Key insight is the finiteness of reasoning parts in planar geometry that can be quickly solved by the SAT, which often does not exist in most first-order and second-order logics, such as number theory, algebra, or functional analysis
When a human has done the same thing many times they tend to try to generalize and take shortcuts. And make tools. Perhaps I missed something but I haven't seen a neural net do that.
Is that very different than the distillation and amplification process that happens during training? Where the neural net learns to predict in one step what initially required several steps of iterated execution.
IMHO, yes. It's not an (internal) invention occurring as a result of insight into the process - it's an (external) human training one model on the output of another model.
This is laughable... Neural networks also have basically unknowable abstractions encoded in their weights. There was some work not long ago which taught an ANN to do modular arithmetic, and found that it was doing Fourier transforms with the learned weights....
> When the brute search fails, an extra geometric construction is randomly added (like adding a midpoint of a certain line) to see if brute search using that extra raw material might work
That's exactly how I was taught geometry in school and I hated it with my all guts. Only after making it into the math department of the university I learned to do it properly and to enjoy it.
You can edit a comment for about an hour if I remember correctly, regardless of it being visible. You can't delete it after someone responds to it though.
The problem is that using LLM as a role for drawing auxiliary lines is too inefficient. It is hard to imagine people deploying a large number of machines to solve a simple IMO problem. This field must be in the early stage of development, and much work remains unfinished. A reasonable point of view is that the search part should be replaced by a small neural network, and the reasoning part should not be difficult, and does not require much improvement. Now is the time to use self-play to improve performance, treating the conclusions that need to be proved in plane geometry problems as a point in the diagram and the conditions as another point in the diagram. Then two players try to move towards each other as much as possible and share data, so that the contribution made by each player in this process can be used as an analogy for calculating wins and losses in Go, and thus improve performance through self-play.
I appreciate that the authors released code and weights with their paper! This is the first high-profile DeepMind paper I can recall that has runnable inference code + checkpoints released. (Though I'm happy to be corrected by earlier examples I've missed)
I don't yet see a public copy of the training set / example training code, but still this is a good step towards providing something other researchers can build on -- which is after all the whole point of academic papers!
Yeap. I'm missing the datasets as well. They have generated 100M synthetic examples ... Were these examples generated with AlphaGeometry? Where is the filtering code and initial input to generate these synthetics?
Im I'm wrong that they are using t5 model? At least they are using the sentencepiece t5 vocabulary.
How many GPU hours have they spend training this model? Which training parameters were used?
Don't get me wrong, I find this system fascinating it is what applied engineering should look like. But I'd like to know more about the training details and the initial data they have used as well as the methods of synthetic data generation.
Google DeepMind keeps publishing these things while having missed the AI-for-the-people train, that I'm getting more and more the feeling that they have such a huge arsenal of AI-tech piling up in their secret rooms, as if they're already simulating entire AI-based societies.
As if they're stuck in a loop of "let's improve this a bit more until it is even better", while AGI is already a solved problem for them.
Or they're just an uncoordinated, chaotic bunch of AI teams without a leader who unifies them. With leader I don't mean Demis Hassabis, but rather someone like Sundar Pichai.
Brute searching all possible mathematical constructs, theorems, etc. to see which one fits the problem would probably take you practiacally an infinite amount of time.
This works tbh, how I see it, very closely to how a human does - via "instinct" it gathers relevant knowledge based on the problem and then "brute searches" some combinations to see which one holds. But this "intuition" is the crucial part where brute search completely fails and you need very aggressive compression of the knowledge space.
> Brute searching all possible mathematical constructs, theorems, etc. to see which one fits the problem would probably take you practiacally an infinite amount of time.
What they did here is one of the first steps towards an AI that generates nontrivial and correct mathematical proofs. (An alternative benchmark would be IMO-level inequalities. Other topics such as algebra, combinatorics and number theory are probably no easier than the rest of mathematics, thus less useful as stepping stones.)
And an AI that generates nontrivial and correct mathematical proofs would, in turn, be a good first step towards an AI that can "think logically" in the common-sense meaning of the word (i.e., not just mess around with words and sentences but actually have some logical theory behind what it is saying). It might be a dead end, but it might not be. Even if it is, it will be a boon to mathematics.
I don’t get the criticism. It seems like basic research and the kind of thing that would lead the way to “AGI” (combining llm-style prediction with logical reasoning). Unless you’re talking about what’s the point of publishing Nature papers - then it’s probably that the people involved want some concrete recognition in their work up to this point. And I supposed tech/investor press until they get something useful out from it.
176 comments
[ 3.0 ms ] story [ 213 ms ] thread- linking the (increasingly powerful) "system 1" tools that are most of current ML with more structured "system 2" tools, like logical proof generation, which can plan and and check the veracity / value of output. - System 2 chugs along 'till it gets stuck, then system 1 jumps in to provide an intuitive guess on what part of state space to check next. - Here they leveraged the ability to generate proofs by computer to create a data set of 100m proofs, enabling scalable self-supervised learning. Seem to me the symbolic domains are well formed to allow such generation of data, which while low value in each instance, might allow valuable pre-training in aggregate.
Putting these elements together is an approach that could get us quite far.
The key milestone will be moving away from the need to use specific formal / symbolic domains, and to generate a pretrained system that can generalize the skills learned from those domains.
You do not need to solve everything at once. This approach has the potential to revolution both math and programming by moving formal verification from being a niche tool into a regular part of every practitioners toolbox.
It also completely solves (within the domain it applies) one of the most fundamental problems of AI that the current round is calling "hallucinations"; however that solution only works because we have a non AI system to prove correctness.
At a high level, this approach is not really that new. Biochem has been using AI to help find candidate molecules, which are then verified by physical experimentation.
Combinatorical game AI has been using the AI as an input to old fasion monte carlo searches
But this is actually a really common scenario. Checking a solution for correctness is often much easier than actually finding a correct solution in the first place.
I'm not sure why you are calling it non-AI. There's no reason why some AI system has to be some single neural network like GPT and not a hacked together conglomeration of a bunch of neural networks and symbolic logic systems. Like is it cheating to use a SAT solver? Is a SAT solver itself not artificial intelligence of a kind?
https://www.nature.com/articles/s41586-023-06747-5
"We use the Meliad library for transformer training with its base settings. The transformer has 12 layers, embedding dimension of 1,024, eight heads of attention and an inter-attention dense layer of dimension 4,096 with ReLU activation. Overall, the transformer has 151 million parameters, excluding embedding layers at its input and output heads. Our customized tokenizer is trained with ‘word’ mode using SentencePiece and has a vocabulary size of 757. We limit the maximum context length to 1,024 tokens and use T5-style relative position embedding. Sequence packing is also used because more than 90% of our sequences are under 200 in length."
Looking at NeurIPS 2023:
https://openreview.net/group?id=NeurIPS.cc/2023/Conference#t...
Some random spotlight papers:
- https://openreview.net/pdf?id=YkBDJWerKg: Transformer (VPT) with 248M parameters
- https://openreview.net/pdf?id=CAF4CnUblx: Vit-B/16 with 86M parameters
- https://openreview.net/pdf?id=3PjCt4kmRx: Transformer with 282M parameters
Also, in my field (speech recognition, machine translation, language modeling), all using Transformer variants, this is a pretty normal model size.
($10m prize for models that can perform well at IMO)
It’s our maths. No one else owns it?
Funny game the AI field is playing now. One-upmanship seems to be the aim of the game.
“Our” doesn’t always imply ownership/title. I do not own my dad.
Not to pick on this guy, but this is ridiculous goal post shifting. It's just astounding what people will hand-wave away as not requiring intelligence.
An analogy with software is that math competitions are like (very hard) leetcode.
There was an article posted on HN recently that is related: https://benexdict.io/p/math-team
We test developer skill by giving them leetcode problems, but leetcode while requiring programming skill is nothing like a real programmer's job.
The analogy is as follows. Like with with leetcode & job interviews is as follows, to excel at math competitions one must grind problems and learn tricks, in order to quickly solve problems in a high pressure environment. And, just like how solving leetcode problems is pretty different than what a typical computer scientist or software engineer does, doing math competitions is pretty different than what a typical mathematician does.
It isn't untrue, but both are considered metrics by the community. (Whether rightfully or not seems irrelevant to ML).
I think the ultimate goal though is clearly that AI systems will be able to generate new high-value knowledge and proofs. I think the realistically the final goal post has always been at that point.
Also if you read about the structure of AlphaGeometry, I think it's very hard to maintain that it "requires intelligence." As AI stuff goes, it's pretty comprehensible and plain.
> Note that the performance of GPT-4 performance on IMO problems can also be contaminated by public solutions in its training data.
Doesn't anybody proofread in Nature?
Not that it's a big deal. I notice problems like this slip into my writing more and more without detection as I get older :/
I don't see the sentence in the Nature paper, though.
Paper: https://www.nature.com/articles/s41586-023-06747-5
Section title: Geometry theorem prover baselines
Second paragraph under that. 3rd sentence from the end of the para.
Section title: Geometry theorem prover baselines
Second paragraph under that. 3rd sentence from the end of the para.
Section title: Geometry theorem prover baselines
Second paragraph under that. 3rd sentence from the end of the para.
They say in the paper, "Because the language model decoding process returns k different sequences describing k alternative auxiliary constructions, we perform a beam search over these k options, using the score of each beam as its value function. This set-up is highly parallelizable across beams, allowing substantial speed-up when there are parallel computational resources. In our experiments, we use a beam size of k = 512, the maximum number of iterations is 16 and the branching factor for each node, that is, the decoding batch size, is 32."
But I don't totally understand how 512 and 16 translate into total number of constructions proposed. They also note that ablating beam size and max iterations seems to only somewhat degrade performance. Does this imply that the model is actually pretty good at putting helpful constructions near the top, and only for the hardest problems does it need to produce thousands?
But let's try -- TL;DR 262,144, but don't take it literally:
- The output of a decoding function is a token. ~3/4 of a word. Let's just say 1 word.
- Tokens considered per token output = 262,144 Total number of token considerations for 1 output token = beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144.
- Let's take their sample solution and get a word count. https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
- Total tokens for solution = 2289
- Total # of tokens considered = 600,047,616 = 262,144 * 2289
- Hack: ""number of solutions considered"" = total tokens considered / total tokens in solution
- 262,144 (same # as number of tokens we viewed at each iteration step, which makes sense)
(via https://news.ycombinator.com/item?id=39030186, but we'll merge that thread hither)
Given enough compute, I wonder how much this would be improved by having it find as many solutions as possible within the allotted time and proposing the simplest one.
The human proof style instead chunks the parts of a solution into human-meaningful "lemmas" (helper theorems) and builds bodies of theory into well-defined and widely used abstractions like complex numbers or derivatives, with a corpus of accepted results.
Some human proofs of theorems also have a bit of this flavor of inscrutable lists of highly technical steps, especially the first time something is proven. Over time, the most important theorems are often recast in terms of a more suitable grounding theory, in which they can be proven with a few obvious statements or sometimes a clever trick or two.
How will it work for math, where humans do useful work right now? I can not see battle math becoming a big thing, but maybe when some of the tedious stuff goes away math will be philosophy and poking the smarter system is where entertainment can be had?
No one needs these contest math problems solved -- by requirement, they are solved before any student attempts them.
That's cool by me, though. This bit of demoscene hardware experiences qualia, and that combination is weird and cool enough to make me want to push myself in new and weird directions. That's what play is in a way.
A transformer is trained on millions of elementary geometry theorems and used as brute search for a proof, which because of the elementary geometry context has both a necessarily elementary structure and can be easily symbolically judged as true or false. When the brute search fails, an extra geometric construction is randomly added (like adding a midpoint of a certain line) to see if brute search using that extra raw material might work. [edit: as corrected by Imnimo, I got this backwards - the brute search is just pure brute search, the transformer is used to predict which extra geometric construction to add]
Also (not mentioned in the blog post) the actual problem statements had to be modified/adapted, e.g. the actual problem statement "Let AH1, BH2 and CH3 be the altitudes of a triangle ABC. The incircle W of triangle ABC touches the sides BC, CA and AB at T1, T2 and T3, respectively. Consider the symmetric images of the lines H1H2, H2H3, and H3H1 with respect to the lines T1T2, T2T3, and T3T1. Prove that these images form a triangle whose vertices lie on W." had to be changed to "Let ABC be a triangle. Define point I such that AI is the bisector of angle BAC and CI is the bisector of angle ACB. Define point T1 as the foot of I on line BC. Define T2 as the foot of I on line AC. Define point T3 as the foot of I on line AB. Define point H1 as the foot of A on line BC. Define point H2 as the foot of B on line AC. Define point H3 as the foot of C on line AB. Define point X1 as the intersection of circles (T1,H1) and (T2,H1). Define point X2 as the intersection of circles (T1,H2) and (T2,H2). Define point Y2 as the intersection of circles (T2,H2) and (T3,H2). Define point Y3 as the intersection of circles (T2,H3) and (T3,H3). Define point Z as the intersection of lines X1X2 and Y2Y3. Prove that T1I=IZ."
I don't think this is quite right. The brute force search is performed by a symbolic solver, not the transformer. When it runs out of new deductions, the transformer is asked to suggest possible extra constructions (not randomly added).
How so? Reasoning is fundamentally a search problem.
The process you described is exactly the process humans use: i.e. make a guess about what's useful, try to work out details mechanically. If get stuck, make another guess, etc. So the process is like searching through a tree.
People figured out this process back in 1955 (and made a working prototype which can prove theorems): https://en.wikipedia.org/wiki/Logic_Theorist but it all hinges on using good 'heuristics'. Neural networks are relevant here as they can extract heuristics from data.
What do you think is "the usual idea of automated reasoning"? Some magic device which can solve any problem using a single linear pass?
You mean like a calculator?
Using heuristics, beam search, etc, = "not brute force".
Calling something smart "brute force" is wrong.
> We shouldn't expect an AlphaCategoryTheory or AlphaNumberTheory anytime soon.
There's already a number of papers demonstrating use of LLMs for math in general:
"Autoformalization with Large Language Models" https://arxiv.org/abs/2205.12615
"Large language models can write informal proofs, translate them into formal ones, and achieve SoTA performance in proving competition-level maths problems!" https://twitter.com/AlbertQJiang/status/1584877475502301184
"Magnushammer: A Transformer-based Approach to Premise Selection" https://twitter.com/arankomatsuzaki/status/16336564683345879...
I find it rather sad that the reaction to amazing research is "but it's just..." and "it might not work on ...". Like, maybe appreciate it a bit and consider a possibility that something similar to it might work?
1. Heuristically add a candidate construction using an NN (a transformer)
2. Brute force search through all possible deductions from the current set of constructions using a symbolic solver
If you don't find a solution after step 2, repeat. There may be some backtracking involved to try a different set of constructions as well.
This approach only works because, in geometry, the set of possible deductions from a given construction is actually quite small.
Also, note that this approach overall is essentially an optimization, not amazing new capabilities. Replacing step 1 with a random construction still solves 10 problems on average in the given time, compared to 30 with the new approach. The existing algorithm, relying mostly on brute force search, is probably able to solve all of the geometry problems if given, say, 10 times as much time as the olympiad students (so not some absurd amount of time).
It’s just that usually these abstractions are fuzzy and hard to formalize, so they aren’t shared. It doesn’t mean that they don’t exist.
That's exactly how I was taught geometry in school and I hated it with my all guts. Only after making it into the math department of the university I learned to do it properly and to enjoy it.
I don't yet see a public copy of the training set / example training code, but still this is a good step towards providing something other researchers can build on -- which is after all the whole point of academic papers!
Im I'm wrong that they are using t5 model? At least they are using the sentencepiece t5 vocabulary.
How many GPU hours have they spend training this model? Which training parameters were used?
Don't get me wrong, I find this system fascinating it is what applied engineering should look like. But I'd like to know more about the training details and the initial data they have used as well as the methods of synthetic data generation.
As if they're stuck in a loop of "let's improve this a bit more until it is even better", while AGI is already a solved problem for them.
Or they're just an uncoordinated, chaotic bunch of AI teams without a leader who unifies them. With leader I don't mean Demis Hassabis, but rather someone like Sundar Pichai.
This works tbh, how I see it, very closely to how a human does - via "instinct" it gathers relevant knowledge based on the problem and then "brute searches" some combinations to see which one holds. But this "intuition" is the crucial part where brute search completely fails and you need very aggressive compression of the knowledge space.
That's not the kind of search which is being done. Read this paper: https://doi.org/10.1023/A:1006171315513
Didnt they already have scaled down simulations of this?
And an AI that generates nontrivial and correct mathematical proofs would, in turn, be a good first step towards an AI that can "think logically" in the common-sense meaning of the word (i.e., not just mess around with words and sentences but actually have some logical theory behind what it is saying). It might be a dead end, but it might not be. Even if it is, it will be a boon to mathematics.
Not even one thing they did was without an associated Nature paper, and the paper was always first.