Formal verification and control theory recur as safety building blocks
The same small toolkit of formal-methods and control-theory ideas keeps resurfacing across the five problem areas of Concrete Problems (2016), quietly doing the technical work behind several unrelated-looking proposals. This theme collects that toolkit and traces where each piece recurs.
Reachability analysis and robust policy improvement turn up first, borrowed to build conservative baseline policies, and the trail ends at Asimov's first law, the earliest and least formal attempt at the same goal.
Across the paper's five problem areas, the same handful of prior formal-methods and control-theory tools keep reappearing as the technical substrate for proposed remedies. Formal verification, exemplified by the complete verification of the federal aircraft collision-avoidance system, stands as the paper's benchmark for what a rigorously safe system can look like, and motivates careful engineering as a reward-hacking remedy. Reachability analysis and robust policy improvement, both imported from control theory, recur specifically as tools for constructing conservative baseline policies against which impact regularizers and bounded exploration are defined. H-infinity control, a framework for minimizing worst-case response to bounded disturbance, underlies bounded exploration in the same way. Model repair extends the idea to a post-hoc setting, altering an already-trained model to restore a specified safety property. Asimov's first law rounds out the group as an early, informal attempt, later taken up seriously within classical AI planning by Weld and Etzioni, to make a safety property machine-checkable at all. This theme's claim is that formal guarantees are not one proposal among many but recurring infrastructure the paper draws on repeatedly.