AlphaGeometry: An Olympiad-level AI system for geometry

Post by qrian » Thu, Jan 18, 2024, 12:23 AM UTC

polygamous_bat wrote: post #119

qrian wrote: post #117

Earlier quoted context omitted.

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 haven’t checked the proof yet, but could it be possible that it’s using directed angles? Threw me off initially when I first learned it as well, but it can be handy for different configurations.

Post by artninja1988 » Thu, Jan 18, 2024, 12:38 AM UTC

cubefox wrote: post #111

artninja1988 wrote: post #67

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

It's the topic of this fascinating paper: https://arxiv.org/abs/2207.14502

Post by hacketthfk » Thu, Jan 18, 2024, 12:47 AM UTC

qwertox wrote: post #58

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…

Post by lucubratory » Thu, Jan 18, 2024, 12:53 AM UTC

cubefox wrote: post #108

empath-nirvana wrote: post #101

Earlier quoted context omitted.

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

In modern terminology, AI = machine learning model. The hand coded GOFAI from the past is just called software.

Post by hyh1048576 » Thu, Jan 18, 2024, 1:03 AM UTC