3 ms·

I didn't know "automated reasoning" was an actual technical term. I didn't mean this by "reasoning". To me, Coq does not reason (in the meaning I intended). It

by jraph 3y ago

I didn't know "automated reasoning" was an actual technical term. I didn't mean this by "reasoning". To me, Coq does not reason (in the meaning I intended). It checks proofs are well-formed and assists proof writing. But yes, there's some implementation of logic in Coq. It applies (a specific form of) logic. Again, LLMs output probable text. They don't do logic. They do statistics on language. Coq works on the actual objects themselves directly, not on the text that presents them. LLMs usually fail to answer to riddles correctly for this reason. We saw plenty of occurrences of this in recent times. Each time LLMs are benchmarked, people think of trying riddles and it works to some extent because something that looks like these riddles are in the training set but it eventually fails. Humans also make mistakes when solving riddles, but not for the same reasons (the process is not the same, they are not "processing text", the are really processing logic, even if the process is fallible).

Sharlin 3y ago
So you just replaced the nebulously defined word "think" with an equally nebulously defined word, "reason"? Not a very convincing argument. You do not know what humans do, no human does, as we don't have such an access to our internal representations. You neither know what LLMs do, no human does, as even though we have full access to their internals, we have little to no idea how to interpret said internals. The most interesting thing about LLMs is the degree that they have learned to model the real world while only being exposed to words. Because those words are highly correlated not just with each other, but with an external entity unknown to the LLM, it's very likely that by learning to model that external entity, the LLM's word-predicting power will increase. LLMs are likely to have converged on a world-model simply because it makes the most sense given the available evidence. This is no different from how human scientists create models of things they cannot directly see based on what they can see. And of course, "seeing" is not directly perceiving the external reality either! Sensory data merely correlates with what's really going on, and the brain has learned to model the world – an unknown external entity – based on the correlations that exist in the sensory language.
- jraph 3y ago
  > So you just replaced the nebulously defined word "think" with an equally nebulously defined word, "reason"? I'll admit I did this. I tried to frame / convey my perspective on the word "think". > Not a very convincing argument. I tried to detail a bit more though. > You do not know what humans do No, but I'm pretty sure I don't try to predict the next word when solving a logical problem through statistical text processing. I would probably do something more like this if I were to bullshit someone or give an insipid political speech, but I think I'm quite bad at it. (nothing to answer on the rest of your comment, it's interesting and I quite agree) (edit: but see https://news.ycombinator.com/item?id=37912319 https://news.ycombinator.com/item?id=37912319)
  - xcv123 3y ago
    > No, but I'm pretty sure I don't try to predict the next word when solving a logical problem through statistical text processing. Neither do transformer / deep learning LLMs. They build an internal representation of the text that captures various relationships and structures within the broader context. They are not Markov chains.
xcv123 3y ago
> Coq works on the actual objects themselves directly, not on the text that presents them. Coq parses the text to an abstract representation and so do LLMs.
- jraph 3y ago
  This does not say much. What's interesting is what do they do with this abstract representation, and what is represented in this representation and how. Compilers translate their abstract interpretation to another programming language, usually native assembly code or bytecode. Coq applies / verifies logical (inductive) inferences on logical objects (rules, proofs, axioms, predicates) (not a Coq expert, details should be checked). LLMs predict next words.
  - xcv123 3y ago
    > LLMs predict next words. That's an oversimplification. Deep learning LLMs such as ChatGPT are designed to solve natural language processing (NLP) tasks, not just next-word prediction. In order to "predict next words" they create a model and "reason" about it. They are not simple Markov processes. There's a lot happening in that ~100 layer neural network.
    - jraph 3y ago
      Okay, it seems I should dig more on the topic. Thanks!
      - xcv123 3y ago
        Well as the other commenter here clarified, you're right about transformer LLMs doing next word prediction, but my point is that's only the tip of the iceberg. The complexity of the model doing the prediction is incredible. Not basic stats.
    - IshKebab 3y ago
      Technically they are designed to solve next-word prediction. It just turns out that good next-word prediction requires understanding the world. (And you can equally view humans as "next word predictors" anyway.)

by jraph 3y ago

Sharlin 3y ago

So you just replaced the nebulously defined word "think" with an equally nebulously defined word, "reason"? Not a very convincing argument. You do not know what humans do, no human does, as we don't have such an access to our internal representations. You neither know what LLMs do, no human does, as even though we have full access to their internals, we have little to no idea how to interpret said internals. The most interesting thing about LLMs is the degree that they have learned to model the real world while only being exposed to words. Because those words are highly correlated not just with each other, but with an external entity unknown to the LLM, it's very likely that by learning to model that external entity, the LLM's word-predicting power will increase. LLMs are likely to have converged on a world-model simply because it makes the most sense given the available evidence. This is no different from how human scientists create models of things they cannot directly see based on what they can see. And of course, "seeing" is not directly perceiving the external reality either! Sensory data merely correlates with what's really going on, and the brain has learned to model the world – an unknown external entity – based on the correlations that exist in the sensory language.

jraph 3y ago
> So you just replaced the nebulously defined word "think" with an equally nebulously defined word, "reason"? I'll admit I did this. I tried to frame / convey my perspective on the word "think". > Not a very convincing argument. I tried to detail a bit more though. > You do not know what humans do No, but I'm pretty sure I don't try to predict the next word when solving a logical problem through statistical text processing. I would probably do something more like this if I were to bullshit someone or give an insipid political speech, but I think I'm quite bad at it. (nothing to answer on the rest of your comment, it's interesting and I quite agree) (edit: but see https://news.ycombinator.com/item?id=37912319 https://news.ycombinator.com/item?id=37912319)
- xcv123 3y ago
  > No, but I'm pretty sure I don't try to predict the next word when solving a logical problem through statistical text processing. Neither do transformer / deep learning LLMs. They build an internal representation of the text that captures various relationships and structures within the broader context. They are not Markov chains.

xcv123 3y ago

> Coq works on the actual objects themselves directly, not on the text that presents them. Coq parses the text to an abstract representation and so do LLMs.

jraph 3y ago
This does not say much. What's interesting is what do they do with this abstract representation, and what is represented in this representation and how. Compilers translate their abstract interpretation to another programming language, usually native assembly code or bytecode. Coq applies / verifies logical (inductive) inferences on logical objects (rules, proofs, axioms, predicates) (not a Coq expert, details should be checked). LLMs predict next words.
- xcv123 3y ago
  > LLMs predict next words. That's an oversimplification. Deep learning LLMs such as ChatGPT are designed to solve natural language processing (NLP) tasks, not just next-word prediction. In order to "predict next words" they create a model and "reason" about it. They are not simple Markov processes. There's a lot happening in that ~100 layer neural network.
  - jraph 3y ago
    Okay, it seems I should dig more on the topic. Thanks!
    - xcv123 3y ago
      Well as the other commenter here clarified, you're right about transformer LLMs doing next word prediction, but my point is that's only the tip of the iceberg. The complexity of the model doing the prediction is incredible. Not basic stats.
  - IshKebab 3y ago
    Technically they are designed to solve next-word prediction. It just turns out that good next-word prediction requires understanding the world. (And you can equally view humans as "next word predictors" anyway.)