5 ms·

> It sounds like it will be able to crack some hard math problems, but not actually do mathematics. What, do you say that because format of the FrontierMath pr

> It sounds like it will be able to crack some hard math problems, but not actually do mathematics. What, do you say that because format of the FrontierMath problems is a bit contrived? I think I must misunderstanding you; a benchmark can't rule out something it doesn't test. And saying solving these problems requiring "deep domain expertise" isn't real mathematics sure sounds like a No True Scotsman argument. Why shouldn't o3 be able to produce novel mathematical proofs? It's got plenty of maths textbooks and papers to train on, the same thing mathematicians train on.

pegasus 2y ago
Those proofs are not by far enough - which is why the raw frontier models don't do that well on this test. The oN models are trained on synthetic data: so generated mathematical theorems and associated proofs. If we could generate legitimately new math we would already have accomplished the hard task, so the generated theorems are going to feel contrieved. I.e. they won't be theorems that ever make it into a future math book. Doesn't mean they won't be useful to mathematicians, they will, just like computers in general are useful in doing maths today.
- versteegen 2y ago
  Think about what happens when a student solves some math exercises using some maths they don't fully understand, or some example they contrived to test what they read. They might make some false starts, work through some steps, make reference to other ideas that they do understand, and finally find a path to the solution. This is actually incredibly analogous to LLM-generated synthetic training data. And nobody's going to print those crossed-out scrawls in a textbox either! But then the student learns from the chain-of-reasoning which arrived at the result. They learn what steps they should have followed one after the other so they can apply it effortlessly next time, what mathematical tool A on problem type B results in, and so forth. They distill some insights from it. Well LLMs can also learn many of these same things. They certainly don't learn as well or as much as humans (just look at their appalling data requirements), but my point is synthetic training data really does work. So expect training compute used on frontier models to keep scaling.
  - isotypic 2y ago
    > and finally find a path to the solution. But how does the student, or in your case the LLM, know that it actually has the solution? For students, this is done by: a grader grading the homework, asking the professor at OH, working on problems with other peers who crosscheck as you go. I see no reason why this LLM produced synthetic data, without this correction factor, would not devolve into a mess of incorrect, maybe even not-even-wrong style "proofs". And then how can training on this yield anything?
    - cevi 2y ago
      When you get good enough at mathematics, you can tell if your proofs are correct or not without asking a TA to grade them for you. Most mathematicians reach this level before they finish undergrad (a rare few reach it before they finish high school). While AI hasn't reached this level yet, there is no fundamental barrier stopping it from happening - and for now, researchers can use formal proof-checking software like Lean, Coq, or Isabelle to act as a grader. (In principle, it should be also be possible to get good enough at philosophy to avoid devolving into a mess of incoherence while reasoning about concepts like "knowledge", "consciousness", and "morality". I suspect some humans have achieved that, but it seems rather difficult to tell...)
      - isotypic 2y ago
        > When you get good enough at mathematics, you can tell if your proofs are correct or not without asking a TA to grade them for you. This is simply not true - you can get a very good sense of when your argument is correct, yes. But having graded for (graduate, even!) courses, even advanced students make mistakes. It's not limited to students, either; tons of textbooks have significant errata, and its not as if no retraction in math has ever been issued. These get corrected by talking with other people - if you have an LLM spew out this synthetic chain-of-reasoning data, you probably get at least some wrong proofs, and if you blindly try to scale with this I would expect it to collapse. Even tying into a proof-checker seems non-trivial to me. If you work purely in the proof-checker, you never say anything wrong - but the presentations in proof checking language is very different from textual ones, so I would anticipate issues of the LLM leveraging knowledge from, say, textbooks in its proofs. You might also run into issues of the AI playing a game against the compiler rather than building understanding (you see elements of this in the proofs produced by AlphaProof). And if you start mixing natural language and proof checkers, you've just kicked the verification can up the road a bit, since you need some way of ensuring the natural language actually matches the statements being shown by the proof checker. I don't think these are insurmountable challenges, but I also don't think its as simple as the "generate synthetic data and scale harder" approach the parent comment thinks. Perhaps I'm wrong - time will tell.
pegasus 2y ago
Look at the sample problems and it will be obvious. For example, look at all the arbitrary constants here: "Let an for n ∈ Z be the sequence of integers satisfying the recurrence formula1 an = (1.981 × 1011)an−1 + (3.549 × 1011)an−2 − (4.277 × 1011)an−3 + (3.706 × 108 )an−4 with initial conditions ai = i for 0 ≤ i ≤ 3. Find the smallest prime p ≡ 4 mod 7 for which the function Z → Z given by n 7→ an can be extended to a continuous function on Zp."

pegasus 2y ago

Those proofs are not by far enough - which is why the raw frontier models don't do that well on this test. The oN models are trained on synthetic data: so generated mathematical theorems and associated proofs. If we could generate legitimately new math we would already have accomplished the hard task, so the generated theorems are going to feel contrieved. I.e. they won't be theorems that ever make it into a future math book. Doesn't mean they won't be useful to mathematicians, they will, just like computers in general are useful in doing maths today.

versteegen 2y ago
Think about what happens when a student solves some math exercises using some maths they don't fully understand, or some example they contrived to test what they read. They might make some false starts, work through some steps, make reference to other ideas that they do understand, and finally find a path to the solution. This is actually incredibly analogous to LLM-generated synthetic training data. And nobody's going to print those crossed-out scrawls in a textbox either! But then the student learns from the chain-of-reasoning which arrived at the result. They learn what steps they should have followed one after the other so they can apply it effortlessly next time, what mathematical tool A on problem type B results in, and so forth. They distill some insights from it. Well LLMs can also learn many of these same things. They certainly don't learn as well or as much as humans (just look at their appalling data requirements), but my point is synthetic training data really does work. So expect training compute used on frontier models to keep scaling.
- isotypic 2y ago
  > and finally find a path to the solution. But how does the student, or in your case the LLM, know that it actually has the solution? For students, this is done by: a grader grading the homework, asking the professor at OH, working on problems with other peers who crosscheck as you go. I see no reason why this LLM produced synthetic data, without this correction factor, would not devolve into a mess of incorrect, maybe even not-even-wrong style "proofs". And then how can training on this yield anything?
  - cevi 2y ago
    When you get good enough at mathematics, you can tell if your proofs are correct or not without asking a TA to grade them for you. Most mathematicians reach this level before they finish undergrad (a rare few reach it before they finish high school). While AI hasn't reached this level yet, there is no fundamental barrier stopping it from happening - and for now, researchers can use formal proof-checking software like Lean, Coq, or Isabelle to act as a grader. (In principle, it should be also be possible to get good enough at philosophy to avoid devolving into a mess of incoherence while reasoning about concepts like "knowledge", "consciousness", and "morality". I suspect some humans have achieved that, but it seems rather difficult to tell...)
    - isotypic 2y ago
      > When you get good enough at mathematics, you can tell if your proofs are correct or not without asking a TA to grade them for you. This is simply not true - you can get a very good sense of when your argument is correct, yes. But having graded for (graduate, even!) courses, even advanced students make mistakes. It's not limited to students, either; tons of textbooks have significant errata, and its not as if no retraction in math has ever been issued. These get corrected by talking with other people - if you have an LLM spew out this synthetic chain-of-reasoning data, you probably get at least some wrong proofs, and if you blindly try to scale with this I would expect it to collapse. Even tying into a proof-checker seems non-trivial to me. If you work purely in the proof-checker, you never say anything wrong - but the presentations in proof checking language is very different from textual ones, so I would anticipate issues of the LLM leveraging knowledge from, say, textbooks in its proofs. You might also run into issues of the AI playing a game against the compiler rather than building understanding (you see elements of this in the proofs produced by AlphaProof). And if you start mixing natural language and proof checkers, you've just kicked the verification can up the road a bit, since you need some way of ensuring the natural language actually matches the statements being shown by the proof checker. I don't think these are insurmountable challenges, but I also don't think its as simple as the "generate synthetic data and scale harder" approach the parent comment thinks. Perhaps I'm wrong - time will tell.

pegasus 2y ago

Look at the sample problems and it will be obvious. For example, look at all the arbitrary constants here: "Let an for n ∈ Z be the sequence of integers satisfying the recurrence formula1 an = (1.981 × 1011)an−1 + (3.549 × 1011)an−2 − (4.277 × 1011)an−3 + (3.706 × 108 )an−4 with initial conditions ai = i for 0 ≤ i ≤ 3. Find the smallest prime p ≡ 4 mod 7 for which the function Z → Z given by n 7→ an can be extended to a continuous function on Zp."