6 ms·
The ability to use automatic verification + synthetic data is basically common knowledge among practitioners. But all these organizations have also explored end
by aabhay 2y ago
The ability to use automatic verification + synthetic data is basically common knowledge among practitioners. But all these organizations have also explored endlessly the different ways to overfit on such data and the conclusion is the same -- the current model architecture seems to plateau when it comes to multi-step logical reasoning. You either drift from your common knowledge pre-training too far or you never come up with the right steps in instances where there's a vast design space.
Think -- why has nobody been able to make an LLM play Go better than AlphaZero while still retaining language capabilities? It certainly would have orders of magnitude more parameters.
- danielmarkbruce 2y agoAlphaZero is a system including models and search capabilities. This isn't a great example.
- aabhay 2y agoAlphaZero is not an llm though? Its primarily a convolutional network with some additional fully connected layers that guide an MCTS at inference time.
- danielmarkbruce 2y agoThat too! It's definitely not an LLM. It would be a bad architecture choice (almost certainly...). For math an LLM would be a good choice. Arbitrary length input, sequential data, unclear where/which symbols to pay most attention to. Math notation is a human built language just like english. Search is a great tool for AI, but you have to have a reasonable search space (like chess or go or poker). I'm not close enough to Lean to understand if it can do something like that (i believe not), but math doesn't feel like a thing where you can reasonably "search" next steps, for most problems.
- danenania 2y ago> It would be a bad architecture choice (almost certainly...) Naively, it would seem like transformers could line up nicely with turn-based games. Instead of mapping tokens to language as in an LLM, they could map to valid moves given the current game state. And then instead of optimizing the next token for linguistic coherence as LLMs do, you optimize for winning the game.
- danielmarkbruce 2y agoA lot of the games usually used are markov. All the state is right there in front of you, doesn't matter how you got there. As an example - chess - it matters not how you got to state X (... someone will get the edge cases..).
- michaelnny 2y agoOne important aspect of the success of AlphaGo and its successor is the game environment is closed domain, and has a stable reward function. With this we can guide the agent to do MCTS search and planning for the best move in every state. However, such reward system is not available for LLM in an open domain setting.
- llm_trw 2y agoTransformers are fundamentally linear, proofs are either tree like or dag like. You'd need a new attention mechanism to allow hierarchical reasoning.
- disconcision 2y agonot obviously the case. natural language also has tree/dag structure yet transformers do okay with it. encoding higher order structure in linear sequences seems necessary for transformers to be able to do most anything
- llm_trw 2y agoNot to arbitrary depth. Empirically the majority of text has depth less than 6 when represented as a tree. Proofs on the other hand have no a priori limits to their depth.
- looofooo0 2y agoBut isn't math strucutured in the same way subdivided in lemmas, theorems, corollarys with limited depth.
- llm_trw 2y agoNo. It's pretty common to have depth 20+ on even relatively simple proofs when you start looking at decomposing proofs to their axioms. The old joke about 1 + 1 = 2 being on page 360 of Principia Mathematica still largely holds.
- auggierose 2y agoThat depends on the granularity of your proof steps. That old joke doesn't hold for a very long time now (take a look at Isabelle/Isar proofs), yet people keep bringing it up.
- 2y ago
- deleted 2y ago[deleted]