111–120 of 177 posts
>To train AlphaGeometry's language model, the researchers had to create their own training data to compensate for the scarcity of existing geometric data. They generated nearly half a billion random geometric diagrams and fed them to the symbolic engine. This engine analyzed each diagram and produced statements about their properties. These statements were organized into 100 million synthetic proofs to train the lang…
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 e…
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 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…
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…
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?
Chess is immensely more popular since Deep Blue beat Kasparov.
Earlier quoted context omitted.
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…
The methods section of the paper describes the training data generation as well as the model settings: https://www.nature.com/articles/s41586-023-06747-5#Sec16
I was all ready to be skeptical for most of these kind of works its outputs are 'not like human proofs' but then I saw Evan Chen's quote that it is indeed clean human-readable proof. Evan Chen is a prominent member of Olympiad math community and an author of famous Olympiad geometry book[1] so this time I will have to concede that machines indeed have conquered part of the IMO problems. [1]: https://web.evanchen.cc/g…
It has the right idea of O2 being on the nine point circle though.
edit: I retract my statement. It looks like it is using directed angles[2] which then the statement becomes correct.
[1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
[2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...
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 th…
This is at almost the polar opposite end of the spectrum from "AGI," it's centered on brute search.
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.
I was all ready to be skeptical for most of these kind of works its outputs are 'not like human proofs' but then I saw Evan Chen's quote that it is indeed clean human-readable proof. Evan Chen is a prominent member of Olympiad math community and an author of famous Olympiad geometry book[1] so this time I will have to concede that machines indeed have conquered part of the IMO problems. [1]: https://web.evanchen.cc/g…
But then again, there's an error in the proof of IMO P3, in Fig1.f and Step 26. of the full proof in supplimentary material[1], which it states that ∠GMD = ∠GO2D, which is incorrect. It should be ∠GMD + ∠GO2D = π. I am trying to follow its logic but I cannot parse Step 25. Did it hallucinate this step? It has the right idea of O2 being on the nine point circle though. edit: I retract my statement. It looks like it is…
I was all ready to be skeptical for most of these kind of works its outputs are 'not like human proofs' but then I saw Evan Chen's quote that it is indeed clean human-readable proof. Evan Chen is a prominent member of Olympiad math community and an author of famous Olympiad geometry book[1] so this time I will have to concede that machines indeed have conquered part of the IMO problems. [1]: https://web.evanchen.cc/g…
But then again, there's an error in the proof of IMO P3, in Fig1.f and Step 26. of the full proof in supplimentary material[1], which it states that ∠GMD = ∠GO2D, which is incorrect. It should be ∠GMD + ∠GO2D = π. I am trying to follow its logic but I cannot parse Step 25. Did it hallucinate this step? It has the right idea of O2 being on the nine point circle though. edit: I retract my statement. It looks like it is…