141–150 of 177 posts
Earlier quoted context omitted.
It's a quote from the article. The argument is naturally there.
I was referring to your leetcode analogy; those too are hard for humans.
AD = DE = EC.
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…
They are optimizing for Nature papers, not general usability. Not even one thing they did was without an associated Nature paper, and the paper was always first.
As soon as ChatGPT got released, I tried to make it solve IMO-style problems. It failed. If this is legit, this is huge. Finding geometric proofs means proving things, and proving propositions is what an intelligence does. In my opinion, this is the closest we have gotten so far to AGI. Really excited to see what the future holds.
Proving propositions has been computer work for several decades. This is not a pure LLM. Search algorithms are obviously incredibly powerful at solving search problems. The LLM contribution is an "intuitive" way to optimize the search.
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…
Earlier quoted context omitted.
Chess never faded away. It actually has never been as big as it is today.
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.
As soon as ChatGPT got released, I tried to make it solve IMO-style problems. It failed. If this is legit, this is huge. Finding geometric proofs means proving things, and proving propositions is what an intelligence does. In my opinion, this is the closest we have gotten so far to AGI. Really excited to see what the future holds.
Have you tried the same questions with ChatGPT 4? It is a transformational change (no pun intended) over the earlier releases, and over all open-source models.
Just today, I needed to interpret some awkwardly-timestamped log data. I asked it a few questions along the lines of "What time it was 10,000 seconds before xx:yy:zz?" It didn't give me the answer, but it wrote and executed a Python program that did.
As a former problem designer for IMO and similar contests, I deeply enjoyed reading this paper. At the same time, I'd like to point out that it was clear Geometry had to be the first topic to give up against AI (i.e., smart knowledge and inference-method indexing) Among math olympiad topics, Geometry problems are often the most "mechanical." Once you can express the problem in terms of coordinates (think XY or comple…
After verifying solvability, what is the process for selecting the specific problems that will show up in the finished set? Is it by vote or some other evaluation?
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…
how did you edit your comment after it got visible to others?