Request for areas of confusion about AI safety and formal physics and engineering

[Steve Omohundro]

I've been in a lot of discussions recently about the use of mathematical proof in formal physics and engineering models to provide safety and correctness guarantees. For example, these two LessWrong posts and their comments: "Provably Safe AI: Worldview and Projects" https://www.lesswrong.com/posts/P8XcbnYi7ooB2KR2j/provably-safe-ai-worldview-and-projects and "Limitations on Formal Verification for AI Safety" https://www.lesswrong.com/posts/B2bg677TaS4cmDPzL/limitations-on-formal-verification-for-ai-safety

In those discussions, I have seen a lot of misunderstanding and skepticism about the current state of physics, it's relationship to the basic engineering disciplines (eg. https://en.wikipedia.org/wiki/List_of_engineering_branches), how fundamental physics and experimental data combine to create today's engineering models, the formalization of fundamental physics and engineering models, and the nature of safety and correctness guarantees and their relationship to mathematical proofs in these formal models. 

I am going to put together a document summarizing these topics in hopes of creating greater shared understanding. If there are particular topics you think it would be helpful for me to cover, please send me an email. Thanks!

Best,

Steve

[Jobst Heitzig]

dear steve,

very laudable! my main issue has always been that it seems impossible to prove anything about the real world, one can only ever prove anything about a formal model, and since all models are wrong to some extent, it is unclear what the seeming "guarantee" actually guarantees. but i guess this is something you plan to address anyway :-)

another question, motivated by my skepticism regarding the suitability of probabilistic models for human behavior and for unique large-scale events such as existential risks, is about the formal type of world models that should be used. i noticed that davidad emphasizes in his texts the need to include non-probabilistic forms of uncertainty, and i would be interested in your take on it. to me it seems natural to use something similar to the worst-case (e.g. maximin) approach of decision making under ambiguity when thinking about "guarantees".

thank you for all your work!
jobst