8 ms·
Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.
by astrange 2mo ago
Agents can generate formal proofs that are checked with an oracle like Lean and can run in a loop.
- YeGoblynQueenne 2mo agoWhat are the search algorithms then? DFS, BFS, A*, etc, can you name them?
- tptacek 2mo agoWhy are you asking them which basic computer science graph traversal algorithms a frontier model used?
- YeGoblynQueenne 2mo 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 2mo agoBecause your question doesn't make sense; this isn't how implicit search works.
- YeGoblynQueenne 2mo ago"Implicit search" with pruning?
- tptacek 2mo agoI don't understand why you're scare quoting "implicit search".
- YeGoblynQueenne 2mo 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 2mo 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 2mo ago[deleted]
- YeGoblynQueenne 2mo 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.