I like your strategy sketch.

There's the guard literature in RL theory which might be nice for step one.

I agree with step two, favoring non-learned components over learned components whenever possible. I deeply appreciate thinking of learned components as an attack surface; shrink it when you can.

Really excited about step three. Estimation and evaluation and forecasting is deeply underrated. It's weird to say because relative to the rest of civilization the movement overrates forecasting, and maybe the rest of the world will be vindicated and forecasting will go the way of esperanto, but I don't think we should think in relative terms. Anyway, I feel like if you had the similarity metric and control that you want for this, it'd be easier to just say "don't do anything drastic" in a blanket way (of course competitive pressures to be smarter and bolder than anyone else would ruin this anyway).

Step four is more oof an implementation reality than a part of the high level strategy, but yeah.

Thanks a ton for the comment, it's exactly the type of thing I wanted my post to generate.

Agree. The product stack has non-learned components in it. Let's throw the kitchen sink at those components.

Some techniques that go under the banner of formal verification are not applied type theory (deduction), usually in the model checking family, or maybe with abstract interpretation. For the record I only have my applied type theory experience, I'm a coq dev, I've spent a cumulative like two hours over the past 3 years pondering abstract interpretation or model checking. That's why I said "formal proof" in the title instead of "formal verification". I could've called it "proof engineering" or "applied type theory" maybe, in the title, but I didn't.

In order for there to be alpha in applied type theory for the learned components, a great deal of things need to fall into place mostly in mechinterp, then some moderate applied type theory work, then a whole lot of developer experience / developer ecosystems work. That's what I believe.

Sorry for abbreviating. Mechinterp in my post refers to the entire field of mechanistic interpretability (the statistically learned program's analogue to reverse engineering a .c file from an executable produced by a c compiler) not to a specific post.

I think a coq bug or the type of mistakes that are easy to make in formalization are more likely than a transistor failure or a bad bit flip bubbling up through the stack, but still not what I'm talking about.

In the background, I'm thinking a little about this terry tao post, about how the process of grokking the proof (and being graceful with typos, knowing which typos are bad and which are harmless, and so on) is where the state of the art mathematics lies, not in the proof itself.

I was discussing your comment with a friend, who suggested what I'm calling factored cognition parallel auditing (FCPA): she asked why don't we just divide the 1e6 lines of coq into 1000-line segments and send it out to 1000 experts each of whom make sense of their segment? The realities would be a little messier than linearly stitching together segments, but this basic setup (or something that emphasizes recursion, like a binary search flavored version) would I think buy us roughly 2-3x the assurance that RH true over just blindly trusting the type theory / laptop to execute Riemann.v in the coq session.

In the current comment, let's assume a background of russell-like "enfeeblement" or christiano-like "losing control of the world/future in a slow burn", filtering out the more yudkowsky-like threatmodels. Not to completely discount malicious injections in Riemann.v, but they don't seem productive to emphasize. I will invoke the vague notions of "theorem intricacy" and "proof length", but it should be possible to not read this footnote^[1] and still follow along with the goals of the current comment.

This isn't really about RH, RH isn't necessarily important, etc. I was actually alluding to / vaguely criticizing a few different ideas at once in the paragraph you quoted.

1. The proof assistants or applied type theory technologies will help agent foundations researchers progress and/or teach. I'm bearish on this largely because I think agent foundations researchers care more about the aforementioned Tao blogpost than about the Kevin Buzzard side of the aisle (recall that Kevin Buzzard is the guy leading the charge to put all math department operations on Lean, from undergrad coursework to the state of the art). I don't think FCPA would help with Tao's notion of mathematical sophistication and understanding, barring pretty drastic advances in HCI/BCI. If theorem intricacy and proof length escapes us in agent foundations, formalization doesn't solve many of the problems that would present.
2. Alignment itself turns out to be deeply inelegant. In these worlds, we may be using a flavor of codegen to even write down the theorem/spec, not to mention the proofs. Let's assume type theory is secure (no leak or unbox related attack surface) and trustworthy (no false positives or false negatives). Then, I don't know how to beat FCPA at arbitrary theorem intricacy and proof size. Maybe a massive FCPA regime could "understand alignment" in an "institutions as distributed cognition" sense. I find this unsatisfying, but it may be the best we can do.
3. The LLM does alignment research for us, and communicates it to us via type theory (there are flavors of this approach that do not invoke type theory, and I think those are even worse). Even when we assume type theory is secure and trustworthy, we have the same problems I highlighted in the preceding list entries. But SGD and the programs it writes are untrusted, so the standard of grokking the old fashion way should be really high. Trusting an auditing process like FCPA to be adequate here feels really dicey to me.

I think we should be sensitive to "which parts of the proof are outsourced to SGD or the programs it writes?" as a potential area of research acceleration. I should be willing to be convinced that parts of the proof are harmless to automate or not pay close attention to, deferring to the type theory or some proof automation regime that may even involve SGD in some way.

If we're relying on computational processes we don't understand, we still get enfeeblement and we still risk losing control of the world/future over time even if type theory is a bajillion times more secure and trustworthy than SGD and the programs it writes.

I hope that makes my worldview more crisp.

Executable textbooks are fun but the odds that playing one cultivates the parts of alignment research that are hard or important seem slim to me.

Crucially to your comment though, what work is "implicitly" doing? Implicitly is where most preparadigmatic work happens! This is loosely related to the false sense of security. Formalization starts when you admit your assumptions as a premise. Formal methods do not second guess assumptions.

If I recall correctly the Cardano team's paper on agile formal methods may have had some comments on this, but I'm not 100% sure.

sounds pretty damn hard, but maybe research workers at google who worked on autoformalization (similar papers) might be able to help this happen at significant scale. if you, like me, find videos far easier to get through than text, here's a talk on the topic that was given recently: