๐ฎ๐๐๐๐๐ -- that all sounds plausible enough, at first glance.
However, are there any other domains of security or safety in which formal theorem-proving is considered helpful, relevant, and/โor reliable?
Consider crash test safety for vehicles, home security against burglars, computer system security against hackers, consensus mechanisms for crypto, political security of nuclear launch codes, military counter-intelligence, anti-counterfeiting measures for fiat currency, etc.
I canโt think of any of these security domains in which formal theorem-proving is actually very helpful. So why should we trust it for AI safety?
I know for one that computer system security and consensus mechanisms for crypto rely on proofs and theorems to guide them. It is a common when you want a highly secure computer system to provably verify its security, and consensus mechanisms rely much on mechanism design. Similarly for counter-intelligence: cryptography is invaluable in this area.
Even in deep learning, proofs have by and large been a failure. Proofs would be important, and there are many people trying to find angles of attack for having useful proofs for deep learning systems, so it is hard to say it is neglected. Unfortunately useful proofs are rarely tractable for complex systems such as deep learning systems. Compared to other interventions I would not bet a substantial amount on proofs for deep learning systems given its important, neglectedness, and tractability.
I believe that planes and trains are a success story of proof engineeringโI only believe this anecdotally because proof engineers bring up planes and trains a lot when the topic of non-academic jobs comes up.
But crucially, I think Cinera is discussing a mathematical process of defining and understanding and communicating, where articulating the theorem in the first place or setting up lemmas for the proof can sometimes be โmostโ of the work. This process is, from a computer science perspective, โinformalโ because of how much human judgment and natural language is involved. So the question is less about formal verification than I think the direction youโre taking it is.
๐ฎ๐๐๐๐๐ -- that all sounds plausible enough, at first glance.
However, are there any other domains of security or safety in which formal theorem-proving is considered helpful, relevant, and/โor reliable?
Consider crash test safety for vehicles, home security against burglars, computer system security against hackers, consensus mechanisms for crypto, political security of nuclear launch codes, military counter-intelligence, anti-counterfeiting measures for fiat currency, etc.
I canโt think of any of these security domains in which formal theorem-proving is actually very helpful. So why should we trust it for AI safety?
I know for one that computer system security and consensus mechanisms for crypto rely on proofs and theorems to guide them. It is a common when you want a highly secure computer system to provably verify its security, and consensus mechanisms rely much on mechanism design. Similarly for counter-intelligence: cryptography is invaluable in this area.
What about testing code for quality, that is, verifying code correctness, thereby reducing bugs?
Even in deep learning, proofs have by and large been a failure. Proofs would be important, and there are many people trying to find angles of attack for having useful proofs for deep learning systems, so it is hard to say it is neglected. Unfortunately useful proofs are rarely tractable for complex systems such as deep learning systems. Compared to other interventions I would not bet a substantial amount on proofs for deep learning systems given its important, neglectedness, and tractability.
I believe that planes and trains are a success story of proof engineeringโI only believe this anecdotally because proof engineers bring up planes and trains a lot when the topic of non-academic jobs comes up.
But crucially, I think Cinera is discussing a mathematical process of defining and understanding and communicating, where articulating the theorem in the first place or setting up lemmas for the proof can sometimes be โmostโ of the work. This process is, from a computer science perspective, โinformalโ because of how much human judgment and natural language is involved. So the question is less about formal verification than I think the direction youโre taking it is.
Geoffrey, you might enjoy my post from last year.