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

Mathematical exploration and discovery at scale

terrytao.wordpress.com

Post reply on HN
Print view View original

91–100 of 135 posts

Re: Mathematical exploration and discovery at scale

#91

Post by ajfkfkdjsfi »

laterium wrote: post #75
kzz102 wrote: post #29

It's really tiring that LLM fans will claim every progress as breakthrough and go into fantasy mode on what they can do afterwards. This is a really good example of how to use the current capabilities of LLM to help research. The gist is that they turned math problems into problems for coding agents. This uses the current capabilities of LLM very well and should find more uses in other fields. I suspect the Alpha evo…

It's really tiring that LLM skeptics will always talk about LLM fans every time AI comes up to strawman AI and satisfy their fragile fantasy world where everything is the sign of an AI bubble. But, yes this is a good way to use LLMs. Just like many other mundane and not news-worthy ways that LLMs are used today. The existence of fans doesn't require a denouncement of said fans at every turn.

> The existence of fans doesn't require a denouncement of said fans at every turn.

When said 'fans' are harmful it really does.

Here's a counterexample to your hypothesis. Fans of Nazis require denouncement at every turn.

Re: Mathematical exploration and discovery at scale

#92

Post by measurablefunc »

omnicognate wrote: post #80
ants_everywhere wrote: post #77

Earlier quoted context omitted.

The objective function is the problem. The objective function is given in all problems. In "find an X such that Y" the objective function is "is this an X? is Y satisfied?". In induction you have P and n to ratchet up the proof by increasing n such that P(n) holds. Combining this reply with your previous one, it sounds like you're setting up a situation where the LLM can neither know the problem nor whether it's maki…

What's the objective function for the Langlands Program?

It seems like the person you're responding to has decided a type checker that outputs 1 when the proof object is valid according to the rules & 0 otherwise should be considered a scoring function. The objective function in this case is not differentiable so the usual techniques from deep learning will not work & genetic search algorithms like AlphaEvolve can in theory be used in these cases. Someone still has to come up w/ the type system & verify the soundness of the rules b/c there is no finite codification of all valid & sound type systems like there are for problems in the linked blog post.

Re: Mathematical exploration and discovery at scale

#94

Post by tug2024 »

lacker wrote: post #78

The point I found most interesting is what the author calls "robustness". Another advantage of AlphaEvolve was robustness: it was relatively easy to set up AlphaEvolve to work on a broad array of problems, without extensive need to call on domain knowledge of the specific task in order to tune hyperparameters. In software world "robustness" usually implies "resistance to failures", so I would call this something diff…

[dead]

Re: Mathematical exploration and discovery at scale

#95

Post by griffzhowl »

ants_everywhere wrote: post #84
griffzhowl wrote: post #82

Earlier quoted context omitted.

An LLM as a component of a tool, plus a team of research mathematicians, did research level math

Yes mathematicians chose problems for the LLM to solve, and then the LLM solved them. That's how we know they were good open problems and that this is research level math.

The LLMs generated candidate solutions which were evaluated by a scoring function written by hand by the mathematicians. No LLM produced these results by itself

Re: Mathematical exploration and discovery at scale

#96

Post by HarHarVeryFunny »

wizzwizz4 wrote: post #42
dpflan wrote: post #28

Earlier quoted context omitted.

Yes, applied research has yielded the modern expert system, which is really useful to experts who know what they are doing.

It's not the "modern expert system", unless you're throwing away the existing definition of "expert system" entirely, and re-using the term-of-art to mean "system that has something to do with experts".

I don't know what the parent was referring to, but IMO "expert system" is one of the more accurate and insightful ways of describing LLMs.

An expert system is generically a system of declarative rules, capturing an expert's knowledge, that can be used to solve problems.

Traditionally expert systems are symbolic systems, representing the rules in a language such as Prolog, with these rules having been laboriously hand derived, but none of this seems core to the definition.

A pre-trained LLM can be considered as an expert system that captures the rules of auto-regressive language generation needed to predict the training data. These rules are represented by the weights of a transformer, and were learnt by SGD rather than hand coded, but so what?

Re: Mathematical exploration and discovery at scale

#97

Post by omnicognate »

measurablefunc wrote: post #92
omnicognate wrote: post #80

Earlier quoted context omitted.

What's the objective function for the Langlands Program?

It seems like the person you're responding to has decided a type checker that outputs 1 when the proof object is valid according to the rules & 0 otherwise should be considered a scoring function. The objective function in this case is not differentiable so the usual techniques from deep learning will not work & genetic search algorithms like AlphaEvolve can in theory be used in these cases. Someone still has to come…

An evolutionary algorithm doesn't need a differentiable objective function, but it can't work with a simple "1 if you got it right, 0 otherwise". It is an iterative approach and at each step it needs to be able to distinguish "better" from "worse" candidates. You certainly can't just say to AlphaEvolve "off you go, I'll tell you when you got it right".

Taking the Collatz Conjecture I used as an example just now, you can trivially write an objective function that outputs 1 for a correct Lean proof of it and 0 for an incorrect one, but AlphaEvolve won't be able to work on that. It needs to be able to assess a collection of incorrect proofs to identify the most promising ones for the next step. I don't know how you'd even start on that, and it's certainly not what they've been doing with AlphaEvolve.

Re: Mathematical exploration and discovery at scale

#98

Post by griffzhowl »

mariusor wrote: post #19
nl wrote: post #18

Hopefully this will finally stop the continuing claims[1] that LLMs can only solve problems they have seen before! If you listen carefully to the people who build LLMs it is clear that post-training RL forces them to develop a world-model that goes well beyond a "fancy Markov chain" that some seem to believe. Next step is building similar capabilities on top of models like Genie 3[2] [1] eg https://news.ycombinator.c…

For the less mathematically inclined of us, what is in that discussion that qualifies as a problem that has not been seen before? (I don't mean this combatively, I'd like to have a more mundane explanation)

This is a useful summary given by another poster here

https://news.ycombinator.com/item?id=45833892

The novel results seem to be incremental improvements on some obscurely-named inequalities that I'm not personally familiar with, but I'm far from this field of maths

Re: Mathematical exploration and discovery at scale

#99

Post by ants_everywhere »

griffzhowl wrote: post #95
ants_everywhere wrote: post #84

Earlier quoted context omitted.

Yes mathematicians chose problems for the LLM to solve, and then the LLM solved them. That's how we know they were good open problems and that this is research level math.

The LLMs generated candidate solutions which were evaluated by a scoring function written by hand by the mathematicians. No LLM produced these results by itself

yes the LLM produced the results themselves

Re: Mathematical exploration and discovery at scale

#100

Post by measurablefunc »

omnicognate wrote: post #97
measurablefunc wrote: post #92

Earlier quoted context omitted.

It seems like the person you're responding to has decided a type checker that outputs 1 when the proof object is valid according to the rules & 0 otherwise should be considered a scoring function. The objective function in this case is not differentiable so the usual techniques from deep learning will not work & genetic search algorithms like AlphaEvolve can in theory be used in these cases. Someone still has to come…

An evolutionary algorithm doesn't need a differentiable objective function, but it can't work with a simple "1 if you got it right, 0 otherwise". It is an iterative approach and at each step it needs to be able to distinguish "better" from "worse" candidates. You certainly can't just say to AlphaEvolve "off you go, I'll tell you when you got it right". Taking the Collatz Conjecture I used as an example just now, you…

It can and it does work w/ such objective functions. Lots of people have used evolutionary algorithms to evolve chess playing neural networks¹ & they have been successful w/ very sparse reward signals where the the final trajectory is scored w/ 0 or 1 according to a win condition. You can say this is not likely to work for proof search & I'd be inclined to agree but the strategy has proven to work in simpler settings so whether it can be used in more complex settings is yet to be determined. If Collatz is not independent of existing axiomatic foundations then a brute force search will find a solution so any heuristics added on top of it that cut out paths to unsuccessful attempts will increase the probability of finding the proof object.

¹https://arxiv.org/abs/1711.08337

Post reply on HN