undefined

points

[-]

This is not "brute-force" though. It's an iterative search algorithm. You learn things at each iteration. You also don't search blindly. You use "something" (heuristics, experience, intuition) to come up with "ideas" at each iteration. You don't try 650 random programs. You try 650 different ideas each learning from the results of previous trials.

Yes this is the "Universal Problem Solving Algorithm". It's actually the same algorithm used by Evolution.

Also this algorithm is vastly different than "monkeys with typewriters". Monkeys don't learn or evolve their writing. There is no memory, no constraints, no learning-curve. At each iteration they freshly sample from a Uniform Distribution. Expected time for a solution is infinitely long.

"The Universal Algorithm" on the other hand is incredibly fast. Humans (designers, researchers) also use the same algorithm but they are much slower to iterate than computers. Instead of trying 650 different ideas at a single run, we have 100s of researchers each try few different ideas independently.

by famouswaffles1 hours ago|

parent|

[-]

Thank you. I've never seen 'brute force' and 'type writing monkeys' abused so much than these LLM discussions.

by lg56891 hours ago|

prev|

[-]

LLMs are indeed very special compared to past efforts at automated theorem proving. The search tree for proofs is enormous, even short textbook exercises (i.e. a few dozen lines of Lean) were difficult with GOFAI techniques. Adding a few orders of magnitude to your compute budget barely moves the needle, since the search space increases exponentially for every line of the proof.

Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.

by yorwba4 hours ago|

prev|

[-]

> We've had the ability to brute-force all of mathematics "eventually"

In a way, yes. You can easily write a program that recursively enumerates all provable theorems in some order. But if you want a proof of a specific theorem, how do you find it in the list? You need to encode the theorem in a formal syntax first, and since mathematics is built on towers of definitions referencing other definitions, that alone is a significant amount of work before you can even write down what you want to prove.

If you want brute force alone, specialized solvers are likely a better choice than LLMs, but what LLMs add to the table is the ability to work with mathematics as it has already been written down. And even though they're bad at brute-forcing, they're still better at it than humans.

An example of a good division of labor is the SAT Attack on Tarski's High School Algebra Problem https://arxiv.org/abs/2608.08421 where they construct a formula with O(n⁴) variables and O(n⁶) clauses and use a SAT solver to show that it is unsatisfiable for n ≤ 11 but satisfiable for n = 12. Then they use an LLM to help them write a Lean proof that the SAT solver input is equivalent to the human-readable description of what they wanted to prove.

by YeGoblynQueenne4 hours ago|

parent|

[-]

>> In a way, yes. You can easily write a program that recursively enumerates all provable theorems in some order. But if you want a proof of a specific theorem, how do you find it in the list? You need to encode the theorem in a formal syntax first, and since mathematics is built on towers of definitions referencing other definitions, that alone is a significant amount of work before you can even write down what you want to prove.

My current framing of this is that the advantage of LLMs lies in their ability to generate the text of a proof without having derived each of its steps in order, like a theorem prover (automated or not) would have to. There's nothing forcing an LLM to derive conclusions from premises (or indeed making it at all capable to do that).

They don't have to understand what the proof they generate means, or to be able to tell whether it's true. In fact, they can't do either. But that's fine as long as it's possible to check the proof with an external verifier.

So most LLM-based proofs use the LLM as the generator and an external verifier as the tester, either a solver like Lean or a mathematician. That's the best of both worlds as far as generate-and-test goes. A powerful generator tied to a powerful tester.

EDIT: yeah, like this:

>> An example of a good division of labor is the SAT Attack on Tarski's High School Algebra Problem https://arxiv.org/abs/2608.08421 where they construct a formula with O(n⁴) variables and O(n⁶) clauses and use a SAT solver to show that it is unsatisfiable for n ≤ 11 but satisfiable for n = 12. Then they use an LLM to help them write a Lean proof that the SAT solver input is equivalent to the human-readable description of what they wanted to prove.

I'm not disergarding the fact that LLMs don't generate text completely at random. They generate likely text. I suspect that can make it more likely to generate the text of some correct proofs. But I have no idea how likely that "more likely" is or what proofs are those.