3 ms·

I do not think it is so clear. Programming has verifiable and non-verifiable aspects. Competitive programming, passing tests, and performance can all be verifi

I do not think it is so clear. Programming has verifiable and non-verifiable aspects. Competitive programming, passing tests, and performance can all be verified. But translating English requirements into actual software, software architecture, taste, or UI design cannot. And yet over the last couple years we’ve seen huge lifts in all of these areas, not just the verifiable ones. Verifiable areas I think are clearly seeing the most improvement, or are the quickest to see improvement. But we are seeing lots of progress in non-verifiable areas as well. How much of the non-verifiable progress is a function of labs purchasing expert data vs. the models improving with compute is maybe another interesting question, but fundamentally I don’t see spend on expert data as something that can’t grow if AI revenues keep growing as well. And as models get better taste they can also help filter and generate new synthetic data for their next versions to train on. The limits of this approach are not so clear.

porridgeraisin 2mo ago
That is because there is human annotated data there. Every session you or I used, then of course paid human feedback on repos (such as the recently famous example of meta forcing their employees to). This is _much better_ data than 1/0 verification, it is as good as a gradient. Automatically verifiable tasks improve faster since well, its automated.
dominotw 2mo ago
> we’ve seen huge lifts in all of these areas, not just the verifiable ones. most gains are still coming from data. isnt that supposed to 'run out' though?
- sothatsit 2mo ago
  Labs spend billions hiring experts to generate new data, and better models can better filter existing training data and generate new synthetic data. There’s no reason for that to run out, it’s just expensive. You could view this as just continually patching a leaky ship. But it seems to work.
  - dominotw 2mo ago
    > Labs spend billions hiring experts to generate new data I thought this is mostly RL data. In my previous comment i was referring to pertaining data.
    - sothatsit 2mo ago
      I remember listening to Andrej Karpathy talk in a podcast about how synthetic data in particular is used to generate more data for pre-training. I see no reasons for that to have changed. I think it is likely a lot of the new data they are paying for contributes to pre-training as well. I would also be very shocked if they weren't filtering or prioritising existing pre-training data as well, for example to do curriculum learning or to avoid data that degrades performance.
- DoctorOetker 2mo ago
  thats the whole point of turning to formal verification: Imagine a hypothetical oracle, call her MyladyMath, imagine you can turn to MyladyMath, submit a correctly formed dossier of axioms and definitions, theorems with proofs, and then a newly putatively proven theorem T. MyladyMath will complain if your dossier is malformed, and point out where and why. If the dossier is not malformed it will eventually read in the claimed theorem T, evaluate its proof and then either point out a which step is erroneous and why, or ultimately accept the proof. Instead of a large corpus of human authored text, this map from dossier/theorem -> accept / reject is a huge implicit array of bits, something fundamental, and this weird gigantic array of bits that effectively describe all accept/reject responses MyladyMath would return exactly. We would never run out of "corpus" when it comes to math, if humans had access to such an oracle. And we do have access to this oracle, and possess compact algorithms that describe the accept / reject bits. One of them is called MetaMath, a minimalistic verifier, which keeps the concepts of prover and verifier separated, this choice results in concrete proof objects (a sequence of step label references). The machines are going to comb through all possible paths of the next N steps, for progressively larger N, efficiently compress those results in the weights of an LLM and then use the gained experience as the intuition for guided "not-so-brute"-force proof search, using the prior iterations intuitions to grade the surprisal of the N+1't iteration of results, etc. The money will not stop flowing in that direction: all power blocs, nation states, militaries, banks, ecommerce, ... depend on cryptography. And the machines will soon do more rigorous proof search grounded in more balanced and objective observations. There is no responsible disclosure mechanism for flawed hardness assumptions in cryptography. It's going to get rocky, and the common man will wonder why the gods have gone crazy, wonder why they don't just pull the plug out of the machines, but nobody will in a staring contest to see who dares keep the plug in the longest (and dominate global cybersecurity). It's the end of the age of artisanal mathematics, it will now become industrialized mathematics.

porridgeraisin 2mo ago

That is because there is human annotated data there. Every session you or I used, then of course paid human feedback on repos (such as the recently famous example of meta forcing their employees to). This is _much better_ data than 1/0 verification, it is as good as a gradient. Automatically verifiable tasks improve faster since well, its automated.

dominotw 2mo ago

> we’ve seen huge lifts in all of these areas, not just the verifiable ones. most gains are still coming from data. isnt that supposed to 'run out' though?

sothatsit 2mo ago
Labs spend billions hiring experts to generate new data, and better models can better filter existing training data and generate new synthetic data. There’s no reason for that to run out, it’s just expensive. You could view this as just continually patching a leaky ship. But it seems to work.
- dominotw 2mo ago
  > Labs spend billions hiring experts to generate new data I thought this is mostly RL data. In my previous comment i was referring to pertaining data.
  - sothatsit 2mo ago
    I remember listening to Andrej Karpathy talk in a podcast about how synthetic data in particular is used to generate more data for pre-training. I see no reasons for that to have changed. I think it is likely a lot of the new data they are paying for contributes to pre-training as well. I would also be very shocked if they weren't filtering or prioritising existing pre-training data as well, for example to do curriculum learning or to avoid data that degrades performance.
DoctorOetker 2mo ago
thats the whole point of turning to formal verification: Imagine a hypothetical oracle, call her MyladyMath, imagine you can turn to MyladyMath, submit a correctly formed dossier of axioms and definitions, theorems with proofs, and then a newly putatively proven theorem T. MyladyMath will complain if your dossier is malformed, and point out where and why. If the dossier is not malformed it will eventually read in the claimed theorem T, evaluate its proof and then either point out a which step is erroneous and why, or ultimately accept the proof. Instead of a large corpus of human authored text, this map from dossier/theorem -> accept / reject is a huge implicit array of bits, something fundamental, and this weird gigantic array of bits that effectively describe all accept/reject responses MyladyMath would return exactly. We would never run out of "corpus" when it comes to math, if humans had access to such an oracle. And we do have access to this oracle, and possess compact algorithms that describe the accept / reject bits. One of them is called MetaMath, a minimalistic verifier, which keeps the concepts of prover and verifier separated, this choice results in concrete proof objects (a sequence of step label references). The machines are going to comb through all possible paths of the next N steps, for progressively larger N, efficiently compress those results in the weights of an LLM and then use the gained experience as the intuition for guided "not-so-brute"-force proof search, using the prior iterations intuitions to grade the surprisal of the N+1't iteration of results, etc. The money will not stop flowing in that direction: all power blocs, nation states, militaries, banks, ecommerce, ... depend on cryptography. And the machines will soon do more rigorous proof search grounded in more balanced and objective observations. There is no responsible disclosure mechanism for flawed hardness assumptions in cryptography. It's going to get rocky, and the common man will wonder why the gods have gone crazy, wonder why they don't just pull the plug out of the machines, but nobody will in a staring contest to see who dares keep the plug in the longest (and dominate global cybersecurity). It's the end of the age of artisanal mathematics, it will now become industrialized mathematics.