Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AlphaProof's Greatest Hits

rishimehta.xyz

Post reply on HN
Print view View original

71–80 of 140 posts

Re: AlphaProof's Greatest Hits

#71

Post by thesz »

samweb3 wrote: post #63
sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!

You are building an SQL in disguise.

First, you need to encode "memes" and relations between them at scale. This is not a language problem, it is data handling problem.

Second, at some point of time you will need to query memes and relations between them, again, at scale. While expression of queries is a language problem, an implementation will heavily use what SQL engines does use.

And you need to look at Cyc: https://en.wikipedia.org/wiki/Cyc

It does what you are toing do for 40 (forty) years now.

Re: AlphaProof's Greatest Hits

#72

Post by nybsjytm »

letitgo12345 wrote: post #58
nybsjytm wrote: post #15

Earlier quoted context omitted.

This has to come with an asterisk, which is that participants had approximately 90 minutes to work on each problem while AlphaProof computed for three days for each of the ones it solved. Looking at this problem specifically, I think that many participants could have solved P6 without the time limit. (I think you should be very skeptical of anyone who hypes AlphaProof without mentioning this - which is not to suggest…

Think more is made of this asterix than necessary. Quite possible adding 10x more GPUs would have allowed it to solve it in the time limit.

Very plausible, but that would also be noteworthy. As I've mentioned in some other comments here, (as far as I know) we outside of DeepMind don't know anything about the computing power required to run alphaproof, and the tradeoff between computing power required and the complexity of problems it can address is really key to understanding how useful it might be.

Re: AlphaProof's Greatest Hits

#73

Post by meindnoch »

samweb3 wrote: post #63
sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!

Looks like an incomplete Prolog.

Re: AlphaProof's Greatest Hits

#74

Post by meindnoch »

zarzavat wrote: post #9
wslh wrote: post #3

If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.

Probably a bad example, P vs NP is the most likely of the millennium problems to be unsolvable, so the answer may be "never". I'll bet the most technical open problems will be the ones to fall first. What AIs lack in creativity they make up for in ability to absorb a large quantity of technical concepts.

Ok, then the AI should formally prove that it's "unsolvable" (however you meant it).

Re: AlphaProof's Greatest Hits

#75

Post by uptownfunk »

wslh wrote: post #32
uptownfunk wrote: post #29

Earlier quoted context omitted.

Ok but how do you get around needing a 10k or 100k h100 cluster

It is well known that cloud services like Google Cloud subsidizes some projects and we don't even know if in a few years improvements will arise.

Possible but unlikely given how much demand there is and the pressure to deliver returns to shareholders, however sure it is possible. Right now search is very inefficient, the search space is massive. That is the main problem. You can have many sequences of text that sound plausible, but of them a much smaller number will be logically valid. This is the main challenge. Once we can search efficiently not just in semantically valid space but I suppose what you can call syntactically valid space then we will be able to crack this.

Re: AlphaProof's Greatest Hits

#76

Post by nine_k »

nybsjytm wrote: post #68
sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving…

You can't talk about formally verifiable truthiness until you solve epistemology. This can be achieved formally in mathematics, with known principal limitations. Here strict theorem-proving, Lean-style, is viable.

It can also be achieved informally and in a fragments way in barely-mathematical disciplines, like biology, linguistics, and even history. We have chains of logical conclusions that do not follow strictly, but with various probabilistic limitations, and under modal logic of sorts. Several contradictory chains follow under the different (modal) assumptions / hypotheses, and often both should be considered. This is where probabilistic models like LLMs could work together with formal logic tools and huge databases of facts and observations, being the proverbial astute reader.

In some more relaxed semi-disciplines, like sociology, psychology, or philosophy, we have a hodgepodge of contradictory, poorly defined notions and hand-wavy reasoning (I don't speak about Wittgenstein here, but more about Freud, Foucault, Derrida, etc.) Here, I think, the current crop of LLMs is applicable most directly, with few augmentations. Still a much, much wider window of context might be required to make it actually productive, by the standards of the field.

Re: AlphaProof's Greatest Hits

#77

Post by jdietrich »

throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

Humans are terrible at anything you learn at university and incredibly good at most things you learn at trade school. In absolute terms, mathematics is much easier than laying bricks or cutting hair.

https://en.wikipedia.org/wiki/Moravec%27s_paradox

Re: AlphaProof's Greatest Hits

#78

Post by Davidzheng »

uptownfunk wrote: post #10
wslh wrote: post #3

If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.

The hard part is in the creation of new math to solve these problems not in the use of existing mathematics. So new objects (groups rings fields) etc have to be theorized, their properties understood, and then that new machinery used to crack the existing problems. I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects. I don’t think it’s one of tech…

I think there's significant financial incentives for big tech given the scarcity of benchmarks for intelligence which are not saturated

Re: AlphaProof's Greatest Hits

#79

Post by Davidzheng »

nybsjytm wrote: post #16
hiddencost wrote: post #6

Earlier quoted context omitted.

No one is focused on those. They're much more focused on more rote problems. You might find them used to accelerate research math by helping them with lemmas and checking for errors, and formalizing proofs. That seems realistic in the next couple of years.

There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of prognostication is definitely out there.

link to this prediction? The famous old prediction of Szegedy was IMO gold by 2026 and that one is basically confirmed right? I think 2027/2028 personally is a breakeven bet for superhuman mathematician.

Re: AlphaProof's Greatest Hits

#80

Post by Davidzheng »

nybsjytm wrote: post #64
titanomachy wrote: post #62

Earlier quoted context omitted.

I’m sure AI can “solve” the Riemann hypothesis already, since a human proved it and the proof is probably in its training data.

No, nobody has proved it. Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present chatbot like ChatGPT to handle, and nothing like AlphaProof is able either since the scope of the proof is well out of the reach of Lean or any other formal theorem proving environment.

what does this even mean? Surely an existing AI could reguritate all of Perelman's arxiv papers if we trained them to do that. Are you trying to make a case that the AI doesn't understand the proof it's giving? Because then I think there's no clear goal-line.
Post reply on HN