3 ms·

Can you summarize what you are saying?

• graycat 3y ago
  Summary: I'd like to see some progress in software for automation of significant cases of reliable mathematical reasoning, but, sorry, from what I know about such reasoning and LLMs, I just don't see LLMs as a promising path to such reasoning. I'd like to see some promising paths to the desired reasoning, with/without the LLM "architecture". Maybe that's a good summary.
  • da39a3ee 3y ago
    Thanks! I wonder if it would work better on proofs expressed in a formal proof-assistant language. Like, if we took something with GPT's training but also specifically exposed it to large amounts of Lean/Agda/Coq/whatever, might it learn to construct proofs in the formal language better than it can in English/LaTeX?
    • graycat 3y ago
      Commonly in high school, students learn to do proofs in a few days/weeks from a few dozen examples. Sorry, best I can guess, the basic technology of ChatGPT can't learn an equivalent way of doing proofs even from millions of proofs. It would be really interesting if the ChatGPT learning could learn proof writing, but my guess is that with ChatGPT too much is missing. Here is a point: Earth is awash in animals with brains that are built a lot like human brains, but I can't think of even one such animal that has a chance of keeping up with a standard course in plane geometry. Why? Something is missing, humans have it and only humans. Yes, your suggestion of adding structure to the data has a chance. Maybe with enough structure proof writing can reduce to looking for a path through a network, roughly what, say, a chess program has to do.