I spent a few years of my career in formal verification. As a result of that, I suspect that the desiderata of “technical alignment” research is most likely und

I spent a few years of my career in formal verification. As a result of that, I suspect that the desiderata of “technical alignment” research is most likely undecidable, and the existing RLHF and prompt engineering approaches are probably the best we can do. A neural network is a large, nonlinear function. In many applications, such as those that release their source code and allow fine tuning, it is adaptive. Internally the weights evolve according to solutions of differential equations. All of these things smell of undecidability when trying to prove safety/alignment properties of them: - The theory of differential equations (which governs the evolution of the weights during training and retraining) is undecidable - Nonlinear functions have decidable cases as long as we stick to polynomials, but even then the decision algorithms are doubly exponential—-much higher complexity than anything in NP-complete, so practically undecidable for very large functions - The neural network is a very large function In summary, they are large, nonlinear, and adaptive, these three characteristics make the problem smell intractable and likely undecidable to me.