Comment by igravious
2 months ago
"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
LLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.
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.
>> The model was perfectly capable of verifying its correctness.
It's an LLM. It can't do that.
7 replies →
Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.
What are the search algorithms then? DFS, BFS, A*, etc, can you name them?
9 replies →