Viewing a single comment thread. View all comments

visarga t1_ixa9md9 wrote

Reply to comment by purple_hamster66 in When they make AGI, how long will they be able to keep it a secret? by razorbeamz

> They even used a Genetic Evolution algorithm to find new proofs, and got a few that no human had thought of before

This shows you haven't been following the state of the art in theorem proving.

> AGI is an illusion, although a very good one that’s useful.

Hahaha. Yes, enjoy your moment until it comes.

2

purple_hamster66 t1_ixi0cu4 wrote

Can you point me to more advanced work, please?

1

visarga t1_ixiec41 wrote

The main idea here is to use

  • a method to generate solution candidates - a language model

  • a method to filter/rank the candidates - ensemble of predictions or running a test (such as in testing code)

Minerva - https://ai.googleblog.com/2022/06/minerva-solving-quantitative-reasoning.html

AlphaCode

FLAN-PaLM - https://paperswithcode.com/paper/scaling-instruction-finetuned-language-models (top score on MMLU math problems)

DiVeRSe - https://paperswithcode.com/paper/on-the-advance-of-making-language-models (top score MetaMath)

1

purple_hamster66 t1_ixis7x3 wrote

Thanks!

But the Wolfram GA generator still outpaces these language models. The question to be answered is: invent new primal & significant math never seen before, not a specific problem like if you eat 2 apples how many are left? Which of the solutions you mention could invent Pythagorean’s c = sqrt( a^2 + b^2 ), or Euler’s formula, or any other basic math that depends on innovative thinking, with the answer not being in the training set?

Which of these could invent a new field of math, such as that used to solve Rubik’s cube?

Which of these could prove Fermat’s Last Theorem?

Reading thru these:

  • Minerva seems to neither invent proofs nor even understand logic; it is simply choosing the best from existing proofs. It seems like solutions need to be in the training set. The parsing is quite impressive, tho.
  • AlphaCode writes only simple programs. Does it also write the units tests for these programs, and use the output from those to refine the code?
  • I’m not sure I understand what PALM has to do with inventing math
  • Diverse looks like it might be capable. It would need several examples of inventing new math, tho, in the training set. (That’s a legit request, IMHO).
1

visarga t1_ixmbq7v wrote

AI is not that creative yet, maybe in the future, but how many mathematicians are? Apparently it is able to solve hard problems that are not in the training set:

> Meta AI has built a neural theorem prover that has solved 10 International Math Olympiad (IMO) problems — 5x more than any previous AI system.

> trained on a dataset of successful mathematical proofs and then learns to generalize to new, very different kinds of problems

This is from 3 weeks ago: link

1

purple_hamster66 t1_ixmi7gj wrote

BTW, I took the IMO in high school and scored the second highest grade in the city. [We had a few prep classes that other schools lacked, so I don’t think it was a fair skill evaluation.] Looking back on college and graduate tests, the IMO was perhaps the hardest test I’d ever taken because it had questions I’d never even imagined could exist. So for an AI to score well is really good news.

1