4 ms·

So, the goal of the paper in https://cdn.openai.com/improving-mathematical-reasoning-with-process-supervision/Lets_Verify_Step_by_Step.pdf https://cdn.openai.c

So, the goal of the paper in https://cdn.openai.com/improving-mathematical-reasoning-with-process-supervision/Lets_Verify_Step_by_Step.pdf https://cdn.openai.com/improving-mathematical-reasoning-with... is "Improving Mathematical Reasoning with Process Supervision". Since I hold a Ph.D. in pure/applied math from a famous US research university, I'm at least curious, maybe impressed, by the goal of "improving mathematical reasoning". In particular, one goal in the paper is "To train more reliable models ..." One of the techniques reported in the paper is "active learning" ... "used to train our best reward model." to improve the "reward" system to reduce "hallucinations", apparently also to obtain "more reliable models". And apparently part of the work is to be "step by step"? Okay: From my background in writing proofs in math the work can be seen as "step by step". E.g., the common high school special format for writing proofs in plane geometry looks "step by step". Then, for "step by step" for a goal of "more reliable models" there are at least hundreds of examples nearly 100% "reliable" in well known math books by P. Halmos, W. Rudin, R. Buck, J. Neveu, and many more, apparently back at least to Euclid. So, it appears that the effort in "Improving Mathematical Reasoning with Process Supervision". is in a sense to solve again a problem already solved with a nearly perfectly "reliable" solution back at least to Euclid. In addition, in my experience as a math student and teacher, commonly already in just the first few weeks of high school plane geometry, students get good at writing proofs that are very "reliable", and how those students learn does not look much like what is described in "Improving Mathematical Reasoning with Process Supervision". So, my guess would be, for the broad goal of having AI do "reliable" math, need a quite different approach. Math that is not "reliable"? From my experience applying math, e.g., to some important problems in US business and national security, in our society math that is not "reliable" stands to be less welcome than week old fish. Indeed, at this point, for the unique crown jewel of STEM, I nominate nearly 100% reliable mathematical proof as in Halmos, ..., Euclid.

MacsHeadroom 3y ago
AI Provers (math models) are an entirely different class of model from LLMs. This paper and method is about getting language models to be better at math without changing their architecture. Math models already do math much better than language models.
- graycat 3y ago
  > This paper and method is about getting language models to be better at math without changing their architecture. My understanding, memory is that already decades ago there was some software that was good at doing calculus manipulations. The software was Mac... something or other. Just now a search gave the name Macsyma and a PDF Reference Manual at https://people.eecs.berkeley.edu/~fateman/macsyma/docs/refman16.pdf https://people.eecs.berkeley.edu/~fateman/macsyma/docs/refma... So, right, long ago there was some software good at some of "Mathematical Reasoning" and, I'd believe, also "reliable". For "mathematical reasoning" in an LLM (large language model), when ChatGPT 4 entered the news I gave ChatGPT 4 two exercises, one from high school plane geometry and one from first calculus. The results for "mathematical reasoning" were no progress at all. From what I know about the LLM approaches and about mathematical reasoning, I don't see any promise for "reliable" results. Then I repeat, math results that are not "reliable" will be about as welcome as week old fish. But just now there is a lot of interest in LLMs as a case of AI. As I glanced at some of the news, apparently the value of Nvidia is now $1 trillion. Sooo, a lot of interest. And we can regard the work on LLMs as research and expect in a few years either (1) reliable mathematical reasoning or (2) not and, thus, evidence that LLMs are not a promising path to such reasoning and AI. We can spend years concluding (2). Heck, I participated in an earlier popular approach to AI. I wrote software, gave talks at Wharton and Stanford, published papers. But I kept looking for anything worthwhile in that work and never found any. Now that work is no longer "popular" and apparently nearly no one believes that there is anything worthwhile there. I'd like to see some progress in software for automation of significant cases of reliable mathematical reasoning, but, sorry, again from what I know about such reasoning and LLMs, I just don't see LLMs as a promising path to such reasoning. So, it is likely the case that for LLMs doing significant cases of reliable mathematical reasoning, people can believe me now or spend some months/years and believe me later. I'd like to see some promising paths to the desired reasoning, with/without the LLM "architecture".
da39a3ee 3y ago
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.

MacsHeadroom 3y ago

AI Provers (math models) are an entirely different class of model from LLMs. This paper and method is about getting language models to be better at math without changing their architecture. Math models already do math much better than language models.

graycat 3y ago
> This paper and method is about getting language models to be better at math without changing their architecture. My understanding, memory is that already decades ago there was some software that was good at doing calculus manipulations. The software was Mac... something or other. Just now a search gave the name Macsyma and a PDF Reference Manual at https://people.eecs.berkeley.edu/~fateman/macsyma/docs/refman16.pdf https://people.eecs.berkeley.edu/~fateman/macsyma/docs/refma... So, right, long ago there was some software good at some of "Mathematical Reasoning" and, I'd believe, also "reliable". For "mathematical reasoning" in an LLM (large language model), when ChatGPT 4 entered the news I gave ChatGPT 4 two exercises, one from high school plane geometry and one from first calculus. The results for "mathematical reasoning" were no progress at all. From what I know about the LLM approaches and about mathematical reasoning, I don't see any promise for "reliable" results. Then I repeat, math results that are not "reliable" will be about as welcome as week old fish. But just now there is a lot of interest in LLMs as a case of AI. As I glanced at some of the news, apparently the value of Nvidia is now $1 trillion. Sooo, a lot of interest. And we can regard the work on LLMs as research and expect in a few years either (1) reliable mathematical reasoning or (2) not and, thus, evidence that LLMs are not a promising path to such reasoning and AI. We can spend years concluding (2). Heck, I participated in an earlier popular approach to AI. I wrote software, gave talks at Wharton and Stanford, published papers. But I kept looking for anything worthwhile in that work and never found any. Now that work is no longer "popular" and apparently nearly no one believes that there is anything worthwhile there. I'd like to see some progress in software for automation of significant cases of reliable mathematical reasoning, but, sorry, again from what I know about such reasoning and LLMs, I just don't see LLMs as a promising path to such reasoning. So, it is likely the case that for LLMs doing significant cases of reliable mathematical reasoning, people can believe me now or spend some months/years and believe me later. I'd like to see some promising paths to the desired reasoning, with/without the LLM "architecture".

da39a3ee 3y ago

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.