I'm not so sure. People had been trying to use brute force to find counterexamples before.

AI is great at reducing the search space and using human-like reasoning (in a brute-force way) to carry out the brute-force search. I'm not surprised by this result. This is exactly what AI should excel at, with human guidance.

▲

igravious a day ago | parent [-]

"using human-like reasoning (in a brute-force way)"

that's self-contradictory -- what brute force means is doing an exhaustive search of a search space (brute forcing it)

using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree

▲

YeGoblynQueenne 11 hours ago | parent [-]

LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.

▲

tptacek 9 hours ago | parent | next [-]

That's not what happened here. This isn't a proof; it's a counterexample. The model was perfectly capable of verifying its correctness. You could have verified it by hand if you wanted; the verification is trivial. Finding it was the hard part.

	▲	YeGoblynQueenne 2 hours ago \| parent [-]
		>> The model was perfectly capable of verifying its correctness. It's an LLM. It can't do that.

▲

astrange 10 hours ago | parent | prev [-]

Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.

▲

YeGoblynQueenne 10 hours ago | parent [-]

What are the search algorithms then? DFS, BFS, A*, etc, can you name them?

▲

tptacek 9 hours ago | parent [-]

Why are you asking them which basic computer science graph traversal algorithms a frontier model used?

	▲	YeGoblynQueenne 2 hours ago \| parent [-]
		OP: >> using human-like(?) reasoning means cutting down the search space by having some sort of insight or intuition which allows you to prune branches from the entire tree So according to the OP there's a search of a tree and it also uses pruning btw, so I want to know what search they mean. Why are you asking?