5 ms·

This is really an argument about test-time scaling, even though the post never uses the term. These days "test-time scaling" mostly means letting the model tal

by h_mirin 2mo ago

This is really an argument about test-time scaling, even though the post never uses the term. These days "test-time scaling" mostly means letting the model talk to itself for longer, but the first genuinely surprising results came from plain sampling. Google's AlphaCode generated millions of candidate programs and filtered them down to a handful of submissions, which beat the average human programmer in 2022, before ChatGPT even showed up. Sampling is what AI is good at. Making examples and doing LeetCode are similar in that verification is clear and cheap. Compared to that, "proof" is still a vague concept, except where Lean works. See the fuss over the ABC conjecture. So humans are still needed. The interesting question to me is what happens after enough learning from "sampling." Isn't AlphaGo's move 37 an AI's nose? If that happens in mathematics, we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying.

laszlojamf 2mo ago
for somebody who's out of the loop: what's the fuss over the ABC conjecture?
- pringk02 2mo ago
  https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCller_theory https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll... Wikipedia is maybe the narrow end of a wedge into this topic but the controversy revolves around a very large and very complex paper that few people are equipped to understand and some of those who are able believe the proof is false.
- steinwinde 2mo ago
  This is a reference to Inter-Universal Teichmüller Theory. Its Wikipedia article gives a good overview (https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCller_theory https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...). In maths lasting disagreements over a published "proof" are rare, but IUTT is an example of it. What the article misses: There is a more recent, ongoing effort to formalize the published proof in Lean under the name of "LANA" (e.g. see https://zen.ac.jp/news/zmcpostevent0717e https://zen.ac.jp/news/zmcpostevent0717e and https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... for a recent update). I guess most mathematicians agree that a successful compile of the proof in Lean would confirm its validity. My personal impression is that the process got stuck at the very point Peter Scholze and Jakob Stix pointed out 8 years ago. Officially LANA has still not reached a conclusion.
  - dj_axl 2mo ago
    > Peter Scholze and Jakob Stix pointed out 8 years ago Interesting read! https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
  - yellowmoonx 2mo ago
    Teichmullogy, wassit all about?
  - josteinhylin 2mo ago
    [dead]
- brazzy 2mo ago
  TDLR for the other two comments: a Japanese mathematician is claiming to have a proof for it, but it is based on an entirely new very complex field of maths which he invented. Getting into it takes years, so other mathematicians are hesitant to invest that much time only to find out that the proof is broken and the field isn't otherwise useful. It doesn't help that the author is rather withdrawn and not willing to spend any effort in making it more approachable. Some tried, and said they found gaps in the proof, to which the author responded, but they were not convinced. And that's essentially the situation since 2018.
jgalt212 2mo ago
> Google's AlphaCode generated millions of candidate programs The trick is avoiding the infinite monkey problem. If your problem is amenable to RL, then you probably don't even need an LLM, Monte Carlo Tree Search gets you there with less expensive hardware.
- deleted 2mo ago
  [deleted]
zahlman 2mo ago
> Sampling is what AI is good at. You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game_show) https://en.wikipedia.org/wiki/Countdown_(game_show) (which a Python script can brute-force on my 12-year-old hardware in half a second) and it made an elementary arithmetic error that's decidedly not human-like.
- TuringTest 2mo ago
  LLMs are terrible at anything systematic. They're incredibly good at anything heuristic, so it makes sense that they can explore wide mathematical spaces fast and converge towards interesting regions. But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. You need to combine them with a proper logical problem solver to get the best parts of both.
  - wyager 2mo ago
    > But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!
    - deleted 2mo ago
      [deleted]
    - TuringTest 2mo ago
      Yeah but the LLM can only handle proofs that hold inside its context window. Proofs for novel theories requiring thousands of pages with dozen millions of steps will need support from external tools to organize the full structure of the formal document; it cannot be done by the LLM inference process alone, which was my point. It would be like asking a mathematician to proof theorems without pen and paper; external tooling is a must, the statistical essential nature of generating content from weights is 1) error prone and 2) not suitable for chains of systematic reasoning that are longer than the attention span. The proofs will be only as good as the framework for linking successive instances of reasoning.
jvanderbot 2mo ago
> we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying sounds like quantum mechanics

by h_mirin 2mo ago

laszlojamf 2mo ago

for somebody who's out of the loop: what's the fuss over the ABC conjecture?

pringk02 2mo ago
https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCller_theory https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll... Wikipedia is maybe the narrow end of a wedge into this topic but the controversy revolves around a very large and very complex paper that few people are equipped to understand and some of those who are able believe the proof is false.
steinwinde 2mo ago
This is a reference to Inter-Universal Teichmüller Theory. Its Wikipedia article gives a good overview (https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCller_theory https://en.wikipedia.org/wiki/Inter-universal_Teichm%C3%BCll...). In maths lasting disagreements over a published "proof" are rare, but IUTT is an example of it. What the article misses: There is a more recent, ongoing effort to formalize the published proof in Lean under the name of "LANA" (e.g. see https://zen.ac.jp/news/zmcpostevent0717e https://zen.ac.jp/news/zmcpostevent0717e and https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf https://github.com/katobungen/LANA_report_202607/blob/pdf/LA... for a recent update). I guess most mathematicians agree that a successful compile of the proof in Lean would confirm its validity. My personal impression is that the process got stuck at the very point Peter Scholze and Jakob Stix pointed out 8 years ago. Officially LANA has still not reached a conclusion.
- dj_axl 2mo ago
  > Peter Scholze and Jakob Stix pointed out 8 years ago Interesting read! https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
- yellowmoonx 2mo ago
  Teichmullogy, wassit all about?
- josteinhylin 2mo ago
  [dead]
brazzy 2mo ago
TDLR for the other two comments: a Japanese mathematician is claiming to have a proof for it, but it is based on an entirely new very complex field of maths which he invented. Getting into it takes years, so other mathematicians are hesitant to invest that much time only to find out that the proof is broken and the field isn't otherwise useful. It doesn't help that the author is rather withdrawn and not willing to spend any effort in making it more approachable. Some tried, and said they found gaps in the proof, to which the author responded, but they were not convinced. And that's essentially the situation since 2018.

jgalt212 2mo ago

> Google's AlphaCode generated millions of candidate programs The trick is avoiding the infinite monkey problem. If your problem is amenable to RL, then you probably don't even need an LLM, Monte Carlo Tree Search gets you there with less expensive hardware.

deleted 2mo ago
[deleted]

zahlman 2mo ago

> Sampling is what AI is good at. You might think so, but I tried asking ChatGPT to solve one of the puzzles from https://en.wikipedia.org/wiki/Countdown_(game_show) https://en.wikipedia.org/wiki/Countdown_(game_show) (which a Python script can brute-force on my 12-year-old hardware in half a second) and it made an elementary arithmetic error that's decidedly not human-like.

TuringTest 2mo ago
LLMs are terrible at anything systematic. They're incredibly good at anything heuristic, so it makes sense that they can explore wide mathematical spaces fast and converge towards interesting regions. But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. You need to combine them with a proper logical problem solver to get the best parts of both.
- wyager 2mo ago
  > But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!
  - deleted 2mo ago
    [deleted]
  - TuringTest 2mo ago
    Yeah but the LLM can only handle proofs that hold inside its context window. Proofs for novel theories requiring thousands of pages with dozen millions of steps will need support from external tools to organize the full structure of the formal document; it cannot be done by the LLM inference process alone, which was my point. It would be like asking a mathematician to proof theorems without pen and paper; external tooling is a must, the statistical essential nature of generating content from weights is 1) error prone and 2) not suitable for chains of systematic reasoning that are longer than the attention span. The proofs will be only as good as the framework for linking successive instances of reasoning.

jvanderbot 2mo ago

> we may end up with results that are correct, machine checkable, and not explainable in any way we find satisfying sounds like quantum mechanics