7 ms·

Note that for the purposes of this paper a “problem” just means a formally decidable problem or a formal language, and the proof is that by creatively arranging

by lsy 2y ago

Note that for the purposes of this paper a “problem” just means a formally decidable problem or a formal language, and the proof is that by creatively arranging transformers you can make individual transformer runs behave like individual Boolean circuits. However, this is a long way from any practical application of transformers: for one thing, most problems we care about are not stated as formal languages, and we already have an exceptionally more efficient way to implement Boolean circuits.

shawntan 2y ago
If a "problem we care about" is not stated as a formal language, does it mean it does not exist in the hierarchy of formal languages? Or is it just as yet unclassified?
- tsimionescu 2y ago
  It means that there are two problems: one, to formalize the problem as stated while capturing all relevant details, and two, solving the resulting formal problem. Until you solve problem one, you can't use formal methods to say anything about the problem (it's not even clear a priori that a problem is even solvable). Unfortunately, the task of a formalizing an informal problem is itself an informal problem that we don't know how to formalize, so we can't say much about it. So overall, we can't say much about how hard the general problem "given a problem statement from a human, solve that problem" is, whether any particular system (including a human!) can solve it and how long that might take with what resources.
  - viraptor 2y ago
    > task of a formalizing an informal problem is itself an informal problem I couldn't find details about this - do you know of a paper or some resource which digs into that idea?
    - tsimionescu 2y ago
      No, but it's pretty obvious, isn't it? If you have an informal problem statement, say "I want this button to be bigger", formalizing it can't be a formal process.
      - viraptor 2y ago
        It's... "knee-jerk obvious". But is it actually true? People seem to be interested in the concept in formal logic arguments for example https://www.researchgate.net/publication/346658578_How_to_Formalize_Informal_Logic https://www.researchgate.net/publication/346658578_How_to_Fo... (which uses formal process for part of formalization), so maybe it's not as simple as it seems initially. I mean, if we're already talking about formal problems, it could use a stronger proof ;)
        tsimionescu 2y ago
        At best, this is a formal process for manipulating certain kinds of statements. But the general problem, "take a human's statement of a problem and translate it into a formal statement of a problem that, if solved, will address what the human was asking for" is far harder and more nebulous. Ultimately, it's exactly the problem that LLMs have been invented for, so it has been studied in that sense (and there is a broad literature in AI for NLP, algorithm finding, expert systems, etc). But no one would claim that they are even close to having a formal specification of this problem that they could analyze the complexity of.
      - moi2388 2y ago
        Why not? Bigger is a measure of size and ought to be easy enough to formalise. Apply a transformation to B which increases its area and leaves the proportion of its sides equal. Why would this statement not be formalisable?
        Zhyl 2y ago
        But here's the thing, it's not that the statement isn't formalisable, it's the method that you used to formalise it isn't formalisable.
- wslh 2y ago
  My 2 cents: Since LLMs (Large Language Models) operate as at least a subset of Turing machines (which recognize recursively enumerable languages), the chain of thought (CoT) approach could be equivalent to or even more expressive than that subset. In fact, CoT could perfectly be a Turing machine. If we leave CoT aside for a moment, it's worth exploring the work discussed in the paper "Neural Networks and the Chomsky Hierarchy"[1], which analyzes how neural networks (including LLMs) map onto different levels of the Chomsky hierarchy, with a particular focus on their ability to recognize formal languages across varying complexity. [1] https://ar5iv.labs.arxiv.org/html/2207.02098v1 https://ar5iv.labs.arxiv.org/html/2207.02098v1
  - flir 2y ago
    > In fact, CoT could perfectly be a Turing machine. Are we going to need an infinite number of LLMs, arranged on a tape?
julienreszka 2y ago
> most problems we care about are not stated as formal languages then a way would be to translate them to formal language

by lsy 2y ago

shawntan 2y ago

If a "problem we care about" is not stated as a formal language, does it mean it does not exist in the hierarchy of formal languages? Or is it just as yet unclassified?

tsimionescu 2y ago
It means that there are two problems: one, to formalize the problem as stated while capturing all relevant details, and two, solving the resulting formal problem. Until you solve problem one, you can't use formal methods to say anything about the problem (it's not even clear a priori that a problem is even solvable). Unfortunately, the task of a formalizing an informal problem is itself an informal problem that we don't know how to formalize, so we can't say much about it. So overall, we can't say much about how hard the general problem "given a problem statement from a human, solve that problem" is, whether any particular system (including a human!) can solve it and how long that might take with what resources.
- viraptor 2y ago
  > task of a formalizing an informal problem is itself an informal problem I couldn't find details about this - do you know of a paper or some resource which digs into that idea?
  - tsimionescu 2y ago
    No, but it's pretty obvious, isn't it? If you have an informal problem statement, say "I want this button to be bigger", formalizing it can't be a formal process.
    - viraptor 2y ago
      It's... "knee-jerk obvious". But is it actually true? People seem to be interested in the concept in formal logic arguments for example https://www.researchgate.net/publication/346658578_How_to_Formalize_Informal_Logic https://www.researchgate.net/publication/346658578_How_to_Fo... (which uses formal process for part of formalization), so maybe it's not as simple as it seems initially. I mean, if we're already talking about formal problems, it could use a stronger proof ;)
      - tsimionescu 2y ago
        At best, this is a formal process for manipulating certain kinds of statements. But the general problem, "take a human's statement of a problem and translate it into a formal statement of a problem that, if solved, will address what the human was asking for" is far harder and more nebulous. Ultimately, it's exactly the problem that LLMs have been invented for, so it has been studied in that sense (and there is a broad literature in AI for NLP, algorithm finding, expert systems, etc). But no one would claim that they are even close to having a formal specification of this problem that they could analyze the complexity of.
    - moi2388 2y ago
      Why not? Bigger is a measure of size and ought to be easy enough to formalise. Apply a transformation to B which increases its area and leaves the proportion of its sides equal. Why would this statement not be formalisable?
      - Zhyl 2y ago
        But here's the thing, it's not that the statement isn't formalisable, it's the method that you used to formalise it isn't formalisable.
wslh 2y ago
My 2 cents: Since LLMs (Large Language Models) operate as at least a subset of Turing machines (which recognize recursively enumerable languages), the chain of thought (CoT) approach could be equivalent to or even more expressive than that subset. In fact, CoT could perfectly be a Turing machine. If we leave CoT aside for a moment, it's worth exploring the work discussed in the paper "Neural Networks and the Chomsky Hierarchy"[1], which analyzes how neural networks (including LLMs) map onto different levels of the Chomsky hierarchy, with a particular focus on their ability to recognize formal languages across varying complexity. [1] https://ar5iv.labs.arxiv.org/html/2207.02098v1 https://ar5iv.labs.arxiv.org/html/2207.02098v1
- flir 2y ago
  > In fact, CoT could perfectly be a Turing machine. Are we going to need an infinite number of LLMs, arranged on a tape?

julienreszka 2y ago

> most problems we care about are not stated as formal languages then a way would be to translate them to formal language