Coq parses the text to an abstract representation and so do LLMs.
Coq parses the text to an abstract representation and so do LLMs.
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.
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.
It just turns out that good next-word prediction requires understanding the world.
(And you can equally view humans as "next word predictors" anyway.)