24 ms·
"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
by igravious 3mo 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
- YeGoblynQueenne 3mo agoLLMs don't search trees. They generate plausible proofs and a human has to check it's true. Repeat until.
- astrange 3mo agoAgents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.
- YeGoblynQueenne 3mo agoWhat are the search algorithms then? DFS, BFS, A*, etc, can you name them?
- tptacek 3mo agoWhy are you asking them which basic computer science graph traversal algorithms a frontier model used?
- YeGoblynQueenne 3mo agoOP: >> 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?
- tptacek 3mo agoBecause your question doesn't make sense; this isn't how implicit search works.
- YeGoblynQueenne 3mo ago"Implicit search" with pruning?
- tptacek 3mo agoI don't understand why you're scare quoting "implicit search".
- YeGoblynQueenne 3mo agoIt's a direct quotation from your comment, not a "scare quote". How does "implicit search" do pruning? Can you explain? Edit: Turns out "implicit search" is actually a thing in the literature, albeit introduced in a single paper I could find that claims Diffusion Modelling does it: https://arxiv.org/abs/2502.19805 https://arxiv.org/abs/2502.19805 I don't think anyone has picked that term up. One more for the scrapheap then, oh well, next paper. No mention of pruning though. So what did you, or the other guys mean?
- wmorgan 3mo agoWhy not? Lasker said, “when you see a good move, look for a better one.” That was tree pruning advice for an implicit search.
- deleted 3mo ago[deleted]
- YeGoblynQueenne 3mo agoSorry, that's just egregious abuse of terminology. Either you're pruning the branches of a tree (or other graph, potentially) when you're doing a tree search, or you don't do pruning. Specifically advice taking (if that's what you mean) is not pruning.
- tptacek 3mo agoThat'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 3mo ago>> The model was perfectly capable of verifying its correctness. It's an LLM. It can't do that.
- tptacek 3mo agoAre you doing the "LLMs don't know how many R's are in 'Raspberry'" thing here? A bunch of people on the original thread about the Conjecture were like "we need to wait and see if real mathematicians verify this proof it's probably just LLM psychosis", because they don't understand that the counterexample is a trivial calculation. Checking it isn't hard; any AP calc student can do it quickly. It's finding the counterexample that's the challenge. It's as if someone presented a SHA-2 collision, which anyone could just feed to `openssl sha256` to see, and then naysayers were like "we need to wait for independent verification because the LLM can't know if that collision was real".
- deleted 3mo ago[deleted]
- YeGoblynQueenne 3mo ago>> Are you doing the "LLMs don't know how many R's are in 'Raspberry'" thing here? I don't know. Are you doing the thing were you're arguing against something you don't like that the other person never said?
- tptacek 3mo agoThe model is very capable of checking this counterexample, was my point.