10 ms·

> 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.

by xcv123 3y ago

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.)
    - xcv123 3y ago
      Yes that's exactly right. NLP problem solving abilities are a consequence of the fact that in order to predict the next token it actually needs to "understand" all of the previous tokens and how they relate to the next predicted token, and determine that the new output is "logically" coherent in context.

> 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.

by 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.)
  - xcv123 3y ago
    Yes that's exactly right. NLP problem solving abilities are a consequence of the fact that in order to predict the next token it actually needs to "understand" all of the previous tokens and how they relate to the next predicted token, and determine that the new output is "logically" coherent in context.