MIRI Research Fellow Benya Fallenstein and Research Associate Ramana Kumar have co-authored a new paper on machine reflection, “Proof-producing reflection for HOL with an application to model polymorphism.”
HOL stands for Higher Order Logic, here referring to a popular family of proof assistants based on Church’s type theory. Kumar and collaborators have previously formalized within HOL (specifically, HOL4) what it means for something to be provable in HOL, and what it means for something to be a model of HOL.1 In “Self-formalisation of higher-order logic,” Kumar, Arthan, Myreen, and Owens demonstrated that if something is provable in HOL, then it is true in all models of HOL.
“Proof-producing reflection for HOL” builds on this result by demonstrating a formal correspondence between the model of HOL within HOL (“inner HOL”) and HOL itself (“outer HOL”). Informally speaking, Fallenstein and Kumar show that one can always build an interpretation of terms in inner HOL such that they have the same meaning as terms in outer HOL. The authors then show that if statements of a certain kind are provable in HOL’s model of itself, they are true in (outer) HOL. This correspondence enables the authors to use HOL to implement model polymorphism, the approach to machine self-verification described in Section 6.3 of “Vingean reflection: Reliable reasoning for self-improving agents.”2
This project is motivated by the fact that relatively little hands-on work has been done on modeling formal verification systems in formal verification systems, and especially on modeling them in themselves. Fallenstein notes that focusing only on the mathematical theory of Vingean reflection might make us poorly calibrated about where the engineering difficulties lie for software implementations. In the course of implementing model polymorphism, Fallenstein and Kumar indeed encountered difficulties that were not obvious from past theoretical work, the most important of which arose from HOL’s polymorphism.
Fallenstein and Kumar’s paper was presented at ITP 2015 and can be found online or in the associated conference proceedings. Thanks to a grant by the Future of Life Institute, Kumar and Fallenstein will be continuing their collaboration on this project. Following up on “Proof-producing reflection for HOL,” Kumar and Fallenstein’s next goal will be to develop toy models of agents within HOL proof assistants that reason using model polymorphism.
- Kumar showed that if there is a model of set theory in HOL, there is a model of HOL in HOL. Fallenstein and Kumar additionally show that there is a model of set theory in HOL if a simpler axiom holds. ↩
- For more on the role of logical reasoning in machine reflection, see Fallenstein’s 2013 conversation about self-modifying systems. ↩
