danielmarkbruce

The idea that all billionaires work together is hilarious. No real adult could possibly believe such nonsense.

and taken to it's extreme.... isn't the atmosphere secretly taking the vibrations in the air right outside out mouth and propagating them through a physical medium, making them available to anyone to capture?

Yeah, good catch. I was under the impression they did the proof in lean from the get go, but you are right.

I guess the nature of the problem lent itself to the 10k agents. Ie, there isn't something general to take here.

You are hitting the google model through openrouter or directly?

There might not be a good abstraction. I've built a few harnesses for different types of workflows, and the details are so different I struggle to see a good abstraction. It's also not clear there should be - if you look at most complex software systems, it's a collection of smaller abstractions/tools/systems pulled together to achieve X.

Yup, and maybe the law will need to evolve.

Fwiw, imo, you should assume everything you say (and write) is recorded going forward.

People generally don't think of keeping bits in memory for some short period of time as "recording".

From a legal perspective you can't record something in many us states. Using the microphone, keeping the bits in memory while you turn it into text, probably doesn't meet any reasonable definition of "record".

You've always been allowed to transcribe (ie, write) out a conversation. Recording is a different thing. A person can always claim, easily and believably, that the transcription is made up. It's just text.

Agree, it is effectively understanding human biology - which we suck at, have little data on, have few good models for.

So, it doesn't appear there is any way to avoid the clinical trial process. And it won't speed up, and it won't get cheaper.

Am I wrong?

It's closer to strategizing once you've run a model through RL. It's optimized to take steps which will lead it to a good outcome down the road.

Well, amazon and apple haven't done great either. One might reasonably claim they weren't as well placed as goog or msft, but it might just be "big company can't do genuinely new thing".

No, it won't. How do you verify some causal claim in biology?

The reason AI is doing so well in math proof writing is that it can verify every idea it has, quickly.

Maybe. Maybe not. Look at AI drug design - it's not really speeding up the important part - drug trials. There isn't really a coherent plan to use AI for the most complex part of drug discovery at all.

If you can create a graph of independent work, which you can with many such problems, agents can work together nicely. Again, thank Lean and the tooling around it.

Highly capable of writing math proofs, no doubt.

It's really unclear that this entire line of work (training LLMs for proof writing) has much real value outside of writing math proofs. It is reasonably clear that, similar to Deep Blue at the time, people are extrapolating the results to general intelligence because the people who usually write proofs are insanely smart (just like world class chess players).

If you look closely at the gains in math, it's largely in proof writing. The reason is Lean, it's not some general intelligence jump, and the number of people actually working on proofs in life rounds to zero.

With Lean, math has become a really well suited problem for LLMs. We will likely see large gains for many years from here, just doing more and more rlvr, like continuously, non stop. No need to train from scratch. It really doesn't speak to the general intelligence of models though. It does speak to how good these things can become when a problem space has verifiable rewards, especially when you can verify one step at a time like Lean enables.

Ok. This all makes sense I guess.

Good going, hope it goes well.

It's more responsible than the use of electricity for a messaging board for people to argue minutiae.

Why not specify 2-3 problems? Won't you have people show up having already spent a bunch of time on their self chosen problem? Which sort of defeats the point of seeing what you can do in a short period of time?

But the next move is self evident if you have a prediction of the value of being in each of the states possible.

Your initial comment says "reward". Reward and return are not the same thing. The policy is choosing the moves based off of returns at the next state, not the immediate rewards. One choice might have reward 0 and expected return 100. Another reward 10 and expected return 20.

And, the expected return from a state is often estimated rather than an explicit trajectory run out all the way. A value function can estimate expected return without explicitly predicting the future states or individual rewards that make up that return.

Fwiw, I use the phrase "total reward" above and use it as a synonym for "return", which is lazy use of language too.

I'm not the one hiding behind a fake name.

If you want to understand how this stuff works, there are totally decent books about building them from scratch. It's not that hard, and you'll likely find it interesting. Sebastian Raschka and Nathan Lambert have good books out, and the Allen Institute has available all the code and data they have used for several projects.

When you are done with the section on RLVR, consider whether the model is predicting tokens, or making moves. There is a reason the word "policy" is used in RL.

Many people are in fact claiming the thing you are saying they are not - even if you are not. The reason they are claiming it is that it was true at one point, and most intro courses/blog posts/videos still describe them that way and then hand wave some "other stuff at the end". You can even see a comment here that refers to the gpt-2 paper. LLMs were trained to predict the next token, produced a distribution to do so, were scored against their prediction v the truth, and the weights updated so that the probability distribution made it more likely to predict the truth from that sample next time. They were, in every sense of the word, a next token predictor.

They are no longer that thing due to post training. They simply aren't making a prediction, and they aren't even optimized for the next token. If I give a distribution of the heights of the population, I'm not giving a prediction either. Distributions don't imply predictions.

Why the desperation to hang onto the word "prediction"?

Brush up :)

The policy is optimized to maximize the the total reward, defined as the sum of the reward at each step, discounted by some factor.

Mine was sarcasm. People who actually understand cars have built them. Until you build something, you don't understand it.

Nathan Lambert wrote a good book recently, and he and his team wrote the paper below about Tulu 3 (Allen Institute). Both are good reads.

https://arxiv.org/pdf/2411.15124

The policy is not learned token by token during RLHF and RLVR. The reward model doesn't score token by token.