Done! I’m not going to argue about whether it’s more just to test against FairBot or CooperateBot. I’m just copying the standard JustBot.
joseph_c
Karma: 356
The JustBot I was copying in fact simulates against FairBot, not CooperateBot. You’re right that I did have two typos—but those were in missing quotes. I’ve now fixed it.
Also, your quotation of
cooperate-botis incorrect, because quote as a special form simply says to look at the next expression and treat it as literal data, so if an expression has already been loaded and evaluated (to give you your functioncooperate-bot), you can’t get its code by just putting a quote before the symbol referring to that function. That would take some kind of environment inspection.
Yes! The prover is really any function with two semantic guarantees:
If
(eval exp)returns#f, so does(prove exp).(prove exp)does not do unbounded computation, and always returns either#tor#f.
The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of
provein the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.
A sort of meta-comment on modal agents: I dislike the way they are presented mathematically, in terms of logical expressions and formulas. I think it would be simpler to use some model of computation, such as the lambda calculus, and then make the agents programs instead of formulas.
For example: We first define a runtime with an evaluator,
(eval exp), and then a macro(prove exp)which hands the expression to a theorem prover, and returns true if and only if the theorem prover determines that the expression will terminate and the resulting value will be true. We can also use the special form(quote exp)to quote an expression, the replacement for declaring that some parts of formulas are implicitly encoded as Gödel numbers.An agent becomes simply a function
(agent my-code opponent-code). During testing against other agents, the runtime provides the agent with its own quoted code and the opponent’s quoted code. (It’s not strictly necessary to provide the agent’s own code to itself, but doing so makes it easier to avoid having to write quines.) The runtime then evaluates both functions, to see who cooperates and who defects. Note that the agent might never terminate—which is an ambiguity that the mathematical presentation doesn’t really resolve. One way to resolve this ambiguity is to say that such is undefined behavior, and the runtime may choose cooperate or defect as it wishes.Some examples of agents in this framework, using a Lisp-like syntax:
;; DefectBot (define (defect-bot my-code opponent-code) #f) ;; False stands for defection, true for cooperation ;; CliqueBot (define (clique-bot my-code opponent-code) (equal? my-code opponent-code)) ;; FairBot (define (fair-bot my-code opponent-code) (prove `(,opponent-code ',opponent-code ',my-code))) ;; Payorian FairBot (define (payorian-fair-bot my-code opponent-code) (define (implies X Y) (or (not X) Y)) (prove `(implies (prove `(,my-code ',my-code ',opponent-code)) (,opponent-code ',opponent-code ',my-code)))) ;; JustBot (define (just-bot my-code opponent-code) (prove `(,opponent-code ',opponent-code ;; Play the opponent against a copy of FairBot's code, not JustBot's code: '(λ (my-code opponent-code) (prove `(,opponent-code ',opponent-code ',my-code))))))Maybe I should vibe-code this so we can have a tournament :)
I don’t think that is a good bar to set. AlphaGo works so well because it is directly running an algorithm to play Go. With AlphaGo, the neural network directly outputs scores and policies for Go positions. However, auto-regressive LLMs don’t do this. They can learn to play Go, but they do this not by directly running a Go-winning algorithm, but by simulating a Go-winning algorithm with their stream of thoughts. I don’t think an auto-regressive LLM would do nearly as well as AlphaGo, simply because this simulation step is inefficient. It’s the same reason that a human can’t add 1,000,000 numbers together in a second, even though we’ve had computers that could do that for 50 years. The human brain isn’t designed for adding lots of numbers together.
The biggest novel capability I see from OPSD is that it enables language models to learn from natural language feedback, which is 99% of how humans learn intellectual skills. The fact that when humans go to school, they are taught using words rather than whips and sugar cubes, makes me believe that this is a very important capability.
Have you read section 4.2 (Main Results) of that same paper? In particular:
Notably, OPSD achieves these gains using only a single rollout per problem and converges within 100 steps, with each problem requiring only 1024 sampled tokens, whereas GRPO requires 8 rollouts of 16k tokens each and may exhibit performance degradation in later steps due to entropy collapse.
The correct figure if you want to see sample efficiency in action is Figure 3.
Furthermore, the comparisons in Figure 3 and Table 2 don’t update the OPSD teacher as they train. In another paper I have read (“Reinforcement Learning via Self-Distillation”), the authors demonstrate that if they repeatedly do a rollout and then update the OPSD student (and consequently teacher, since they are the same model), they get significant improvements. (See Figure 10 on page 11. Note that this figure only shows that the teacher improves significantly with bootstrapping, but this seems to me to also indicate that the student would—note how the student breaks through the barrier set by the initial teacher.)
Next, OPSD works significantly better for continual learning than naive GRPO, but I don’t know how much of an advantage that is because there are other methods that work decently.
Finally, OPSD is still a rather new technique, so unlike GRPO, researchers haven’t found all the little tricks that make it work better, and it’s still crushing GRPO. The OPSD technique is also very flexible, you can throw all kinds of extra context at the teacher to help it, and so there is an entire new direction for optimization.
I think OPSD is a very powerful technique. But maybe all the capabilities researchers had already heard of it, if you and Caleb Biddulph are any indication.
I think it was a blunder for you to publicize this technique. I’m sure some AI researchers knew of the technique already, but it was pretty under the radar. Even the recent Kimi K3 was trained on a variant of PPO. I also had not seen any mention of that paper online before, despite it being published all the way back in January.
Because GRPO/PPO/DPO are so much less sample efficient than the self-distillation method, pretty much only the big AI labs could make a model like Kimi K3. Now pretty much anyone can.
I kind of agree, but for what it’s worth, I thought it was amusing.
Yes, that makes sense! Thanks for explaining.
I think it would have made more sense to me if the GL derivation was written as
We also have another theorem of PA asserting that this theorem is provable:
Is this theorem a premise, or derived from another theorem? I disagree with the inclusion of this theorem.
I’m not disagreeing about what your argument would prove, if the premises were all correct. I agree that it does, indeed, prove an equivalence between the Payorian FairBot and the Löbian FairBot, modulo certain other assumptions. But those other assumptions are non-trivial, and the two FairBots are in fact different, precisely when those other assumptions break down.
Yes, I agree that the GL derivation, with both of those premises, establishes that the Löbian FairBot
cooperates at most as often as the Payorian FairBotis semantically a Payorian FairBot. But why are you allowed to have both premises? You don’t have both premises in the definition of either bot.Edit: I think there are edge cases where the second premise does not hold, and so the Löbian FairBot might behave differently from the Payorian FairBot.
I think that your GL derivation is correct, assuming the premises are true, though I haven’t looked at it very carefully. I’m confused about why you have both of the following premises, instead of just one of them:
I can see you choosing either one as a reasonable definition of “FairBot”, depending on whether you are describing its code or the implementation of that code as a running program (i.e., to actual run the agent, you need some kind of theorem prover—should our logical language describe the syntax of the agent’s code, or the semantics of how the agent runs on the theorem prover?). But how are you acquiring both premises simultaneously? I think that is mixing things up slightly, and in fact, this conflation is masking a real difference between the Payorian FairBot and the Löbian FairBot. The Löbian FairBot will, when run, depending on the implementation, either cooperate with
fewerother sorts of FairBots than the Payorian FairBot, or fail to terminate sometimes.
A few comments:
The statement
You seem to be doing one of two things: Either extracting
I think it makes sense to define the code of FairBot as simply
I think you are mixing up the implementation with the code, and this is where you are coming up with an additional assumption which you shouldn’t be.
We are assuming Löbian fairness, so we have available as premises
\begin{align*}
P \leftrightarrow \Box Q\
\Box(P \leftrightarrow \Box Q)
\end{align*}I thought that the Löb fairbot was simply
If we imagine that each player submits a computer program which takes in the source code of the other player, then the second premise is essentially an assertion that your program terminates on your opponent’s input. That seems like a reasonable goal of a correct program to have, but how can you actually guarantee that as the language designer? Perhaps you could make such a guarantee within the program itself (i.e., semantically it terminates, but you can’t prove it), but this seems like it would have to be a bare assumption about the program itself, not anything proved about itself.
Perhaps another way to go about this is to introduce GL modal logic. Instead of creating shares in
The part I’m confused about is why Bob converts
Also, I think a weak part of this idea in either conception is that you have to provide a proof to make these exchanges. I think it would be neat for an exchange to have a proof-verifier, but that doesn’t really seem to hold up to the promise of Alice and Bob working collectively to prove
Suppose you have a neural network which classifies handwritten digits. It has 10 outputs for 10 logits, and its “choice” is the highest logit it outputs, given an input image. This is what I mean by a choice.
I don’t understand what it means to say an entity “COULD HAVE” output a different action than what they outputted, other than talking about either (1) a stochastic function, or (2) a claim that there exists a hypothetical other function which would have output something else. I think the second case is the right picture to have in your head, but you seem to have some other picture in your head. Would you mind explaining it?
However, I think this is the wrong model to have for the possibility of choosing otherwise. Instead, you should imagine that a different choice function in your place might choose a different action
But do you know that? Surely establishing how the capacity for choice actually works requires empirical investigation.
You appear not to have answered that question.
I was using the word “model” to mean “picture in your head”, not “theorized laws which capacity for choice follow”. I was arguing that it was an error to define capacity for choice in a split-brain way, and that you should instead define it in a substitution-brain way. I didn’t answer your question because it wasn’t really engaging with what I had said. It’s probably my fault for being sloppy in my word choice.
I agree that establishing how choosing actually works in brains requires empirical investigation.
The only difference from your model is the inclusion of indeterminism
My model was agnostic about indeterminism, and still is.
Special, meaning it’s the only uncaused cause.
You’re sure using special to mean more than that later on!
Momentous things matter more than trivial thungs by definition.
If you read the second part of my sentence after the semicolon, and the sentence after that paragraph, it is clear that I am just saying that being more momentous doesn’t affect the truth value of a proposition, not that momentous things matter less.
But not to the same extent , as I argued at length.
Not really. You mostly just repeated “more momentous” in various ways, such as more real, more special, and so on. If you want me to care more about choices in the world where choices are non-deterministic than the world where choices are deterministic, I think you would have to tell me something about how that would change the world. For example, perhaps if choices are non-deterministic, we can reduce crime rates by studying psychology, whereas if choices are deterministic, crime rates will never go down no matter how much psychology we as a civilization learn. Therefore, in the first world, it’s useful to study psychology, while in the second world it is not. I don’t believe that is the case, though. But that’s the kind of argument that would get me to care one way or the other.
You do mention something about the world being doomed/not necessarily doomed, but again, I don’t think that actually is a matter of determinism or not. At some point in the future, the world will either be doomed or not doomed, and our actions will decide which is the case. We should therefore take actions to avoid the doomed world, and our brains are configured to follow this precept in either world. Adding true randomness back in just makes it so that there is now aleatoric uncertainty about the future, not simply epistemic uncertainty.
But you seem to be arguing for something more than just “a brain which uses a truly random source of entropy to run a random algorithm”. I don’t want to comment on it, because clearly I don’t understand.
I don’t believe in your 2, and never said anything along those lines.
Sorry.
An inward firing account of choice, the brain mechanisms that enable it, does not answer all the questions, because some of them are outward firing questions about how people interact and societies work
I feel like these are separate areas that can be solved individually. The first area is a question of modelling the brain: How does the brain learn? How does it map information to better than random actions? The second area is a question of social responsibility: As a society, when should we hold people responsibility so that we can accomplish X? What system of rewards and punishments helps us develop a healthy society?
The first area is about psychology, neuroscience, and AI. The second area is about ethics, economics, and game theory. It’s true that answers in the first area can inform us about answers in the second area, but I don’t see the case for the other direction.
It is of course both. You have no moral responsibility alone on a desert island; but also none if you live in a society but don’t have the appropriate brain functions
I disagree. I think it is not both. Who we choose to hold responsible and for what actions is solely a social problem, though of course we should use material facts and mathematical laws to inform us of how to do that well.
Yes, but you can also have a richer model as well.
Richer than what? I haven’t proposed any model of social responsibility.
Potentially, yes, because an interpreter can include a sandbox , that prevents the code from doing what it thinks it’s doing.
This is an interesting perspective. I personally take the perspective that two things are identical if you can’t distinguish between them, so code running in a sandbox is just as real to the program as when it is not in a sandbox, as long as the sandbox faithfully simulates interacting with the outside world. Nevertheless, to an outside observer, these situations do not look identical, so there is a sense in which the program running in the sandbox is less real to the outside observer. But I think this stretches the meanings of “real” and “unreal” beyond their typical use-case of distinguishing between ideas and the material world or between truth and fabrication. It’s probably more useful to coin a new term like “root” or “base” to distinguish between a simulated universe and a universe not running in a simulation.
I actually believe in empiricism.
I wasn’t trying to say you don’t believe in empiricism! I was trying to argue that it would be more pragmatic to simply describe the world instead of worrying about whether the label “real” or “unreal” applies.
But I don’t have a fully equipped neurology lab, so I can’t test my testable model of free will.
You mentioned libertarian free will, which according to Google says that human beings can make choices undetermined by prior causes, physical laws, or divine predetermination. Would brains taking advantage of true randomness in the universe count, provided it exists? Or does there need to be some special substance which is only used in choice-making? Or am I just completely missing the mark?
I don’t really find the distinction between “a brain uses a random algorithm which takes advantage of true randomness” and “a brain uses a random algorithm which uses chaos for its ‘entropy’” very important for understanding how choice-making works.
I would be very interested in hearing a test you could perform to validate/invalidate your model of free will. I’m still not really sure what you mean by free will, see, and I think that would help a lot.
I assume you’re in the same position.
Pretty much.
What were you expecting me to do, that I’m in a position to do, and yet not doing? And, are you doing it yourself?
Right now I would mostly appreciate you explaining what your model of free will is.
No, I mean “each choice is not a choice, it’s just following the configuration”. “learning” is across time, and is about changes in configuration. But at each choice-point, there is no actual choice.
That depends on what you mean by “actual choice”. From a mechanistic definition of choice, there is a choice: An action was output based on input information. I don’t know what a sensible definition of a choice looks like other than this. I also don’t understand what keeps this from being an “actual” choice. Is it that you feel like it’s not really you making the choice, if it’s just your brain running an algorithm? But you are that algorithm running on that brain. It is you who is making the choice.
Well, no. You can program it to use pseudorandom data in an algorithm, or even “hardware-random”, which isn’t necessarily random, just unpredictable by humans. ―Dagon
Compare what you said with what I said:
It is, though, an interesting question whether true randomness exists, or whether everything that appears random is just chaos. ―joseph_c
I am not claiming that true randomness necessarily exists, just that I can program a computer to use a random algorithm, so nondeterminism isn’t a mysterious question: Just supply true randomness to a random algorithm.
I downvoted your post for this. How do you know that the person who has given you the good things in your life is Jesus of Nazareth? Did you directly observe him giving you these things, or did your church simply tell you that blessings come from Jesus, and you now have the inference hardcoded backwards in your head?
To explain, the correct direction of inference is “I observe Jesus giving me good things, therefore Jesus is good.” The incorrect direction is “Jesus is good, therefore he gives me good things.” Unless you have significant other evidence that Jesus is, in fact, good and tends to give the majority of good things, it does not make sense to conclude that Jesus gave you your good things.