On Sun, Aug 2, 2020 at 11:38 AM Jon P <[email protected]> wrote:
> Thanks so much for your nice response Mario. I think the work you’re doing > is really awesome and I’m very thankful that you would take your time to > explain things to me. I feel similarly with everyone else in this > community, I’m so impressed by everyone here. > > I dig the idea that each independent check decreases the probability of > being wrong, so I can see how formal proofs in multiple proof assistants on > multiple machines makes it unlikely that MM0 is flawed, that makes a lot of > sense. I also see why having MM0 be as small as possible is very good. I > also guess there are philosophical problems around creating something > provably logically infallible. > > Can I ask about how MMC proofs work? So I had a little look at formal > verification for software and it showed techniques like exhaustively > searching the state space or using automated induction, are you thinking > along these lines where the computer will run a standard algorithm for each > program? > That is certainly an approach that is used to check program correctness, but (1) it's not particularly well suited to formal proof and (2) it doesn't cover most actual proofs of interest. Of course the reason we want a theorem prover in the mix is so that we can state and prove theorems of arbitrary mathematical complexity about programs. For example, if we have a program that enumerates primes, we can use the proof that there are infinitely many primes to show that it will never finish (or rather, it will overflow before finishing). > Or is it more like an MM proof where there are explicit steps? For example > Prime(X) is the sort of function which I can’t really imagine checking in > an automated way as there are so many inputs, though maybe there is some > nice induction depending on how it works (a sieve of Eratosthenes might be > amenable to an inductive proof for example). > The kind of proofs that MMC works with are fully symbolic proofs. The original proponent of this approach was Tony Hoare, and Hoare logic ( https://en.wikipedia.org/wiki/Hoare_logic) is a logic where you prove properties of the form "if P holds on entry to code segment C, then C will not crash and after finitely many steps, C will complete with Q holding afterwards", abbreviated {P} C {Q}. This has a nice compositional structure, for example if {P} C1 {Q} and {Q} C2 {R} then {P} (C1; C2) {R}. This has since been refined into Separation logic in order to avoid the expressions P,Q,R talking about the entire state of the machine but rather only the part that matters for the code segment in question. > Does the user have to specify the steps themselves or can the compiler > help generate them or is it a totally different system? If MMC produces > proofs which are checkable by MM0 does that mean they are similar to MM > proofs in style? It’s interesting to me that MM0 can check both MM proofs > and x86 proofs and yet remain small, that is very intriguing. > x86 is just a definition, like you would make in set.mm. It's just a very large and complicated definition split into many sub-functions. Every individual theorem is relatively small, and it is possible to prove the semantics of a single instruction without too much difficulty, just like one might unfold the definition of a group to prove that multiplication is associative. The user provides a proof at the level of the input language, which looks like C with this separation logic layered on top. The compiler will progressively refine this C code through several intermediate stages, until eventually arriving at x86 machine code, and stage has its own semantics and each transformation is associated with a semantics preservation theorem. So while the code is being refined down, the proof is being built up simultaneously, so that when you get to the end, you have machine code but also a proof of semantic correctness using that original separation logic proof as the guide. So it's partially human written and partially constructed by the compiler. The actual proof object that is generated is essentially a MM theorem, using lots of carefully constructed lemmas. It shouldn't be egregiously large, but it probably won't be especially readable. If so there has been a lot of work to build up the set.mm database of > proofs, is there a similar process to build up MMC functions and their > associated proofs? For example given a verified addition function you could > build a multiplication function and then a function for the multiplication > of matrices or something. > Yes, in a sense. I mentioned that the compiler needs carefully constructed lemmas for the translation between intermediate stages. These lemmas have to be proven manually, and essentially form a part of the compiler. Without them, the compiler can't compile (or at least, it can't compile to produce a proof). But there are more lemmas that can be proven beyond the basics, and what these do is effectively make the language itself more expressive, adding new types and new code constructs in the programming language. For example one might define a "for" loop in terms of "while", prove some lemmas about the lowering process, and then MMC will have a "for" loop. The other half of the work is writing specific programs in the language. Because proofs are embedded in the code, this is a nontrivial task, and in a sense represents the "meat" of the work for a particular program. If you have a program that enumerates primes, this is where facts about primality get involved. Here reuse is also possible, forming a "verified software library" of functions with proven properties. I'm not making any serious effort to modularize the verifier in this way, but for general use this is certainly something that should be developed. > I think these formal methods are obviously the future of mathematics so > it’s really cool to be able to watch them develop. I also think there may > be interesting applications to The AI Control Problem, for example letting > an AI expand its capabilities iff it can prove the expanded system is > constrained in the same way it is constrained itself. There is some similar > paradigm to what you are doing about a system verifying itself (or it's > offspring). This sounds like it might make it feasible to control an > arbitrarily sophisticated system which is cool because without control > there are a lot of worries. I asked Stuart Russel about it in a Reddit AMA > and he said he’s considered formal proofs as a method for AI Control which > is interesting. I’ve watched enough Stargate SG-1 to know I don’t want to > have to deal with replicators. > :) Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsBiOG9BW5Qqm_d1ZHi9Xo3w7pfWcooFvMd1HsYCMX8Sw%40mail.gmail.com.
