4 ms·
> finding geometric constructions Finding optimal geometric constructions. Every problem is an optimisation because AlphaEvolve is an optimiser. > This is not
by omnicognate 1y ago
> finding geometric constructions
Finding optimal geometric constructions. Every problem is an optimisation because AlphaEvolve is an optimiser.
> This is not correct. The evaluation function is arbitrary.
You say this and then show details of how the score is calculated. AlphaEvolve needs a number to optimise, because it is optimiser. It can't optimise true/false.
> The feedback that you've constructed a graph of size K with some property does not tell you what you need to do to construct a graph of size K + M with the same property.
The feedback that you've constructed a graph of size K tell you that you've constructed a bigger graph than a competing solution that only constructed a graph of size K-1 and are therefore a more promising starting point for the next round of mutation
If you're trying to solve a "does there exist an X" problem, the information that none of your candidates found (or was) an X doesn't give you any information about which of them you should retain for mutation in the next step. You need a problem of the form "find the best X" (or, rather "find a good X") and for that you need a score of how well you've done. If you can find a score that actually improves steadily until you find the thing you're trying to prove the existence of then great, but generally these problems are "find the best X" where it's easy to come up with a load of competing Xs.
> The novelty here is that the LLM replaces the human expert.
That's not the claim at all. Tao said the benefits are scaling, robustness and interpretability, not that it can be operated by someone who doesn't know what they're doing.
- ants_everywhere 1y ago> not that it can be operated by someone who doesn't know what they're doing. It's operated by an LLM, not a human. There is no human in the loop.
- omnicognate 1y agoThe LLM doesn't write the objective function. It only generates candidate solutions to be evaluated by it. The human writes the objective function. That's how you define the optimisation to perform.
- ants_everywhere 1y agoThe 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 making progress on the problem. With those constraints no human could do mathematics either or really anything else.
- omnicognate 1y agoWhat's the objective function for the Langlands Program?
- ants_everywhere 1y agoThe Langlands Program is a research program not a single mathematical problem. It consists of many open conjectures with various levels of progress toward them. However, I think it's quite a victory that the goal posts have moved from "LLMs can't solve problems" to "LLMs probably can't solve all open conjectures in Langlands Program in one shot. But as I said way up above, if you have the statement of any particular problem you can just use the function that evaluates proofs as your objective function. If you were to do this in Lean, for example, you'd get compiler output that contains information you can use to see if you're on the right track. In addition to the output of the proof program you'd probably want to score sub-computations in the proof as metrics. E.g. if you want to show that a map has finite fibers, you may want to record the size of the fibers, or a max over the size. If you need to know an element is not contained in some Levi subgroup then you may want to record information about the relevant Levi decomposition. This mimics things that humans know to score their progress as they're doing computations.
- omnicognate 1y agoIf you want a simple, well defined problem that a child can understand the statement of, how about giving me the objective function for the Collatz Conjecture?