3 ms·

Current LLMs, we do not know that we cannot have future LLMs which can be almost formal. Think mathematics written in English and LaTeX

card_zero 2y ago
If using an LLM meant carefully crafting a complex, precise, formal prompt that specified only one possible output, I might be interested. But then I wonder if the prompt would be very much shorter. Thinking about it, this depends on which differences we consider aspects of the output program, and which ones we consider trivial differences that don't count. If you say "build an RPG about dragons with a party of magic using heroes" and the LLM spits one out, you reached a level of abstraction where many choices relating to taste and feeling and atmosphere (and gameplay too) are waved aside as trivial details. You might extend the prompt to add a few more, but the whole point of creating a program this way is not to care about most of the details of the resulting experience. Those can be allowed to be generic and bland, right? Unless you care about leaving your personal touch on, say, all of them.
nyrikki 2y ago
Things constructivist mathematics cannot do: 1) Prove Addition of natural numbers. 2) Prove two real numbers are equal. RNNs are only TC with infinite precision and unlimited resources, once you have finite precision they are very limited. LLMs do not have recursion at all and can't even emulate finite automations. In fact soft attention can only emulate TC_0 Feed forward networks are effectively DAGs and with soft attention, DAGs built with AND,OR, NOT, and threshold circuits. One of the state of the art inference in code methods is bi-abduction, probably best described here. https://fbinfer.com/docs/separation-logic-and-bi-abduction/ https://fbinfer.com/docs/separation-logic-and-bi-abduction/ But this localization makes it computationally possible, and has limits. The qualification and frame problems, combined with the very limited computational power of transformers is another lens. LLMs being formalized doesn't solve the problem. Fine tuning and RAG can help with domain specificity, but hallucinations are a fundamental feature of LLMs, not a bug. Either a use case accepts the LLM failure mode (competent, confident, and inevitably wrong) or another model must be found. Gödel showed us the limits of formalization, unless we find he was wrong, that won't change.
- trueismywork 2y ago
  Thanks for your insightful comment. I'll read the links later. I had just assumed that RNNs were TC, didn't think of limitation put on by bounded precision since I assumed that any bounded precision could be compensated by growing memory module. So, after your comment, I went literature searching and I found this: https://papers.nips.cc/paper_files/paper/2021/hash/ef452c63f81d0105dd4486f775adec81-Abstract.html https://papers.nips.cc/paper_files/paper/2021/hash/ef452c63f... I haven't read it yet. But if it is true, then RNN would seem to be TC
  - nyrikki 2y ago
    Note from the open review of that paper. > As discussed in the paper and pointed out by the reviewer, the growing memory module is non-differentiable, and so it cannot be trained directly by SGD. We acknowledge this observation. Two stack FSA/RNN are interesting, but as of now, not usable in practice.

card_zero 2y ago

If using an LLM meant carefully crafting a complex, precise, formal prompt that specified only one possible output, I might be interested. But then I wonder if the prompt would be very much shorter. Thinking about it, this depends on which differences we consider aspects of the output program, and which ones we consider trivial differences that don't count. If you say "build an RPG about dragons with a party of magic using heroes" and the LLM spits one out, you reached a level of abstraction where many choices relating to taste and feeling and atmosphere (and gameplay too) are waved aside as trivial details. You might extend the prompt to add a few more, but the whole point of creating a program this way is not to care about most of the details of the resulting experience. Those can be allowed to be generic and bland, right? Unless you care about leaving your personal touch on, say, all of them.

nyrikki 2y ago

Things constructivist mathematics cannot do: 1) Prove Addition of natural numbers. 2) Prove two real numbers are equal. RNNs are only TC with infinite precision and unlimited resources, once you have finite precision they are very limited. LLMs do not have recursion at all and can't even emulate finite automations. In fact soft attention can only emulate TC_0 Feed forward networks are effectively DAGs and with soft attention, DAGs built with AND,OR, NOT, and threshold circuits. One of the state of the art inference in code methods is bi-abduction, probably best described here. https://fbinfer.com/docs/separation-logic-and-bi-abduction/ https://fbinfer.com/docs/separation-logic-and-bi-abduction/ But this localization makes it computationally possible, and has limits. The qualification and frame problems, combined with the very limited computational power of transformers is another lens. LLMs being formalized doesn't solve the problem. Fine tuning and RAG can help with domain specificity, but hallucinations are a fundamental feature of LLMs, not a bug. Either a use case accepts the LLM failure mode (competent, confident, and inevitably wrong) or another model must be found. Gödel showed us the limits of formalization, unless we find he was wrong, that won't change.

trueismywork 2y ago
Thanks for your insightful comment. I'll read the links later. I had just assumed that RNNs were TC, didn't think of limitation put on by bounded precision since I assumed that any bounded precision could be compensated by growing memory module. So, after your comment, I went literature searching and I found this: https://papers.nips.cc/paper_files/paper/2021/hash/ef452c63f81d0105dd4486f775adec81-Abstract.html https://papers.nips.cc/paper_files/paper/2021/hash/ef452c63f... I haven't read it yet. But if it is true, then RNN would seem to be TC
- nyrikki 2y ago
  Note from the open review of that paper. > As discussed in the paper and pointed out by the reviewer, the growing memory module is non-differentiable, and so it cannot be trained directly by SGD. We acknowledge this observation. Two stack FSA/RNN are interesting, but as of now, not usable in practice.