isn't it clearly split between verifiable not verifiable ? what is interesting about that question.
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.
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.
most gains are still coming from data. isnt that supposed to 'run out' though?
You could view this as just continually patching a leaky ship. But it seems to work.
I thought this is mostly RL data. In my previous comment i was referring to pertaining data.
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.
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.