@nasqret: I've been doing a lot of experiments with auto-research in the last few weeks, especially in algebra. Here are a couple…

I’ve been doing a lot of experiments with auto-research in the last few weeks, especially in algebra. Here are a couple of thoughts I want to share about sparks of generalization.

1. Once the problem can be reduced to a constructive question about rings and becomes a finite computation, I can use a model to basically develop the code from scratch. You don’t even need a specialized CAS for that, Rust is enough.

2. If the question is about a highly abstract object, you can still turn it into a format in which all the constraints can be manipulated formally. You can use functional programming to model the abstraction through constraints. The best situation is when you can actually encode the abstraction in one of the many logics that are friendly to SMT solvers.

3. Most of the time, the difficulty of the problem lies in the lack of clear connections between some of the encoded predicates. This is where it starts getting interesting. When you play with code generation, you can accidentally discover such missing rules and abstract them from the calculations.

4. Here, there is a chance that the model will spontaneously generalize the pattern into an abstraction. This is, in general, very hard because the models are not designed to produce something unusual. Quite the contrary: they usually do not get very far beyond their training.

5. This is where something strange must happen with the model: an accidental guess, multi-agent search, etc. I have already seen some very small sparks of new ideas or accidental generalization in my auto-research loops. I suspect this will scale up with compute.

6. Now the difficult part begins for humans: those abstracted rules might be provable, or even formalizable in Lean, but they are completely new and foreign to humans. I have seen this in my research into invertible cellular automata. I see a claim that is true—there is a proof—but I don’t understand its deeper meaning. I don’t know how to internalize it off the bat.

7. When you keep pushing your agents, you end up in a place where no soul has been before. The mathematics is completely foreign, and the notation is concocted and unfamiliar. Your instinct is to say that it is all wrong, but it isn’t. It is just alien.

In the coming days, I will publish several such examples straight from my loops. I suspect this is an early instance of spontaneous and very weak generalization. It feels like the early hacks with GPT-3.5 that produced something resembling “thinking.” It is very bad, but it is something. Maybe ideation is mechanical and can be scaled up with a lot of effort?

Where are we going?

Pretty close tbh @skominers

Sorry, this is just a glimpse into the new internals I’ve been thinking about. Mostly to keep them alive and turn into concrete paper.

Thank you Kamil! Very happy that you are reading my wild thoughts. It’s like Pensieve for me and things might be very rough. But it’s better rough than too lat. And I want to know from people if this might be potentially plain stupid!

Thanks!