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

101–110 of 135 posts

Re: Mathematical exploration and discovery at scale

#101

Post by wizzwizz4 »

HarHarVeryFunny wrote: post #96
wizzwizz4 wrote: post #42

Earlier quoted context omitted.

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…

If you can extract anything resembling a declarative rule from the weights of a transformer, I will put you in for a Turing award.

Expert systems are a specific kind of thing (see https://en.wikipedia.org/wiki/Expert_system#Software_archite...): any definition you've read is a description. If the definition includes GPT models, the definition is imprecise.

Re: Mathematical exploration and discovery at scale

#102

Post by ants_everywhere »

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…

> It seems like the person you're responding to has decided a type checker... should be considered a scoring function

To clarify, I didn't decide this, this is a valid scoring function in AlphaEvolve. The scoring function is generic and can even be an LLM writing prose giving feedback on the solution followed by another LLM scoring that prose numerically. There needs to be a numeric score to rank solutions. Typically type checkers give more output than 1 or 0, though. For example, they'll often give you information about where the first error occurred.

That doesn't mean it's a great scoring function or even a good one. But it is a scoring function and without any scoring function at all progress would be impossible. To the extent that math is about writing proofs, it's a valid and essential scoring function for any problem. In practice, to make progress you need more than just the ability to write a logical proof, you need to build on previous results, add extra conditions, compute examples, etc. But in the context of the discussion, the point is that there is always some way to measure progress, which is why AlphaEvolve includes this mechanism.

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

This is true, but it's also true that typically mathematicians fix a logic or universe before getting down to work. So AlphaEvolve and human mathematicians are on equal footing in that respect.

Re: Mathematical exploration and discovery at scale

#103

Post by measurablefunc »

ants_everywhere wrote: post #102
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…

> It seems like the person you're responding to has decided a type checker... should be considered a scoring function To clarify, I didn't decide this, this is a valid scoring function in AlphaEvolve. The scoring function is generic and can even be an LLM writing prose giving feedback on the solution followed by another LLM scoring that prose numerically. There needs to be a numeric score to rank solutions. Typically…

> it's also true that typically mathematicians fix a logic or universe before getting down to work

This is true for programmers, it's not true for mathematicians. You can say programming is a subset of mathematics but mathematics is more than programming so proof search does not exhaust all the activities of a mathematician but it does exhaust all the activities of a programmer.

Re: Mathematical exploration and discovery at scale

#104

Post by HarHarVeryFunny »

wizzwizz4 wrote: post #101
HarHarVeryFunny wrote: post #96

Earlier quoted context omitted.

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…

If you can extract anything resembling a declarative rule from the weights of a transformer, I will put you in for a Turing award. Expert systems are a specific kind of thing (see https://en.wikipedia.org/wiki/Expert_system#Software_archite... ): any definition you've read is a description . If the definition includes GPT models, the definition is imprecise.

Well, OK, perhaps not a declarative rule, more a procedural one (induction heads copying data around, and all that) given the mechanics of transformer layers, but does it really make a conceptual difference?

Would you quibble if an expert system was procedurally coded in C++ rather than in Prolog? "You see this pattern, do this".

Re: Mathematical exploration and discovery at scale

#105

Post by griffzhowl »

ants_everywhere wrote: post #99
griffzhowl wrote: post #95

Earlier quoted context omitted.

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

Yes, some good ones and some garbage, and the LLMs had no idea which was which. The good solutions were arrived at by an iterative procedure which depended on the scoring function written by the mathematicians, and it seems plenty of other ingenuity besides.

It's a fascinating use of LLMs by mathematicians to produce new results, but the LLMs are just one component of the tools used to get the results.

Re: Mathematical exploration and discovery at scale

#106

Post by omnicognate »

measurablefunc wrote: post #100
omnicognate wrote: post #97

Earlier quoted context omitted.

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…

From that chess paper:

> Each position in the ECM test suite has a predetermined “best move”. Each chromosome processes all of the 879 positions, and for each position it attempts to find this predetermined best move as fast as possible.

> Instead of counting the number of correctly “solved” positions (number of positions for which the organism found the best move), we used the number of nodes the organism had to process in order to find the best move.

That isn't a 1-or-0 objective function, and the paper isn't an example of using an evolutionary loop in which the objective function doesn't give you any information on which candidates are better in a given iteration. Because that isn't possible.

Re brute forcing by evaluating the countable set of correct proofs within a given formal system, people have been trying that since computers were invented and it hasn't resulted in the magic proof factory yet. People continue to work on better and better heuristics for trimming the search and I understand some of the stuff people have been doing in that direction with Lean is actually useful now, but there hasn't been a huge breakthrough in it and nobody expects a system like that to spit out a proof of the Collatz Conjecture any time soon. More to the point of this discussion, it's not what AlphaEvolve does.

Anyway, I need to go to bed. It's been fun.

Re: Mathematical exploration and discovery at scale

#107

Post by 11101010001100 »

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…

In other words, proofs of existence are measure zero in the space of evolution?

Re: Mathematical exploration and discovery at scale

#108

Post by measurablefunc »

omnicognate wrote: post #106
measurablefunc wrote: post #100

Earlier quoted context omitted.

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…

From that chess paper: > Each position in the ECM test suite has a predetermined “best move”. Each chromosome processes all of the 879 positions, and for each position it attempts to find this predetermined best move as fast as possible. > Instead of counting the number of correctly “solved” positions (number of positions for which the organism found the best move), we used the number of nodes the organism had to pro…

The same applies to proof search. Once you fix a finite foundational set of axioms the game proceeds exactly as in chess.

Re: Mathematical exploration and discovery at scale

#109

Post by jungturk »

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…

Looks like he's updated the text, striking through "robustness" and substituting "adaptability"

Re: Mathematical exploration and discovery at scale

#110

Post by ants_everywhere »

measurablefunc wrote: post #103
ants_everywhere wrote: post #102

Earlier quoted context omitted.

> It seems like the person you're responding to has decided a type checker... should be considered a scoring function To clarify, I didn't decide this, this is a valid scoring function in AlphaEvolve. The scoring function is generic and can even be an LLM writing prose giving feedback on the solution followed by another LLM scoring that prose numerically. There needs to be a numeric score to rank solutions. Typically…

> it's also true that typically mathematicians fix a logic or universe before getting down to work This is true for programmers, it's not true for mathematicians. You can say programming is a subset of mathematics but mathematics is more than programming so proof search does not exhaust all the activities of a mathematician but it does exhaust all the activities of a programmer.

> it's not true for mathematicians

It actually is true for mathematicians.

Most of us work in ZFC. Some people choose to work in constructive logic. Some people choose to only use countable choice. But we always know what logic we're working in and which theorems we can invoke. E.g. if you choose not to accept the axiom of choice you also have a sense of which results depend on Zorn's lemma and have to work around them. All of this is normal background for mathematicians.

So there's no need to allow the foundations of mathematics to vary unless you're working in logic and need to quantify over foundational systems or compare them. You would certainly never start a problem and then switch the logic midway through. That sort of thing wouldn't even be coherent.

Post reply on HN