Comment by js8

Comment by js8 a day ago

8 replies

View on Hacker News

Formal verification is ultimately an epistemological problem, how do we know that our model of reality corresponds to reality?

People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in.

For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X.

By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions.

Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.

WJW 16 hours ago

> We can take a definition of a rose from a neural network that recognizes what a rose is

Can we? That just shifts the problem to building such a NN.

I think it would already be pretty tricky to get a decent sized panel of humans to agree on what a "rose" is. Do rose-shaped but yellow flowers count? How about those genetically altered thornless ones? How about perfectly imitatations that are made of plastic? Images of roses? The flowers from the list at https://www.epicgardening.com/rose-lookalikes/?

And of course there's the problem of getting a NN to recognise just roses. The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications. I very much doubt humanity could build a neural network that perfectly recognises roses and only roses.

Reply View 1 reply
  • js8 an hour ago

    > The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications.

    I think we differ in how we see the formal methods. IMHO they are not supposed to give you 100% guarantees, because you can always cast doubt over your assumptions. Rather, I think they're a practical tool that give you a better guarantee; so in this context, a paint program verified using NN's definition of a rose is better than one that has been verified only on couple examples of a rose.

    Another way to look at it - there is Curry-Howard isomorphism which states that (idealized) execution of a computer program is the same as doing logical inference, i.e. proving a formal statement. So if you're calculating 2+2, you're effectively proving that 2+2=4.

    This means all software testing is a special case of a formal method. For example, when you run the test suite of your program with a new Java runtime, you are proving a statement, on these inputs my program will give the expected output, assuming we run with the new runtime. So the new runtime becomes the assumption (about the environment program runs in).

    My point is, people already use formal methods, they just don't call them that. It's natural then to ask, instead of testing on a few input examples, can we instead verify a larger set of inputs (defined intensionally not extensionally)? And that's how you come from a few examples of a rose picture (extensional definition) to a definition given by an NN (intensional definition), which encompasses too-many-to-count rose pictures.

    The NN doesn't have to be perfect. So what, you verified in your paint program one can also paint some pictures of not-quite-roses. Who cares? It's better verified overall.

    Reply View 0 replies
ThreeFx 21 hours ago

Now you’ve just shifted the problem to a much harder statement: proving the things the NN recognizes as a rose is actually a rose.

You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.

Reply View 2 replies
  • js8 18 hours ago

    Yeah. That's why I am saying it's the epistemological problem.

    In the above example, that NN recognizes rose as a rose is an assumption that it is correct as a model of the (part of the) world. On that assumption, we get a formal definition of "an image of a rose in the pixelated image", and we use that to formally prove our system allows roses to be painted.

    But getting rid of that assumption is I believe epistemologically impossible; you have to assume some other correspondence with reality.

    I agree with you on the hardware. I think the biggest obstacle to software formal correctness is the lack of formal models of which we can be confident describe our environment. (One obstacle is the IP laws - companies do not like to share the models of things they produce.)

    Reply View 0 replies
  • lstodd 18 hours ago

    Right, the problem is that one can't formally describe the environment, and any one thing has to interact with it. So formallness goes right out the window.

    Reply View 0 replies
netdevphoenix 14 hours ago

> how do we know that our model of reality corresponds to reality?

This is the main issue I have with formal methods in commercial settings. Most of the time, the issue is that the model reality map is far from accurate. If you have to rewrite your verification logic every time you have to update your tests, development would go very slowly

Reply View 0 replies
butlike 9 hours ago

Definition by consensus doesn't always equal absolute definition, to continue your epistemological metaphor. Just because the consensus states it's a rose doesn't mean it absolutely is in the truest sense (the artist, program, and neural network consensus could all be wrong in some intrinsic way).

Reply View 0 replies
empath75 16 hours ago

Formal verification is a pure logic problem. You are making a proof, and a proof is just a demonstration that you can reach a given expression given certain axioms and the rules of formal logic.

You can't just chuck a neural network into the mix because they aren't formally verified to do basically anything beyond matrix multiplication and the fact that they are universal approximators.

Reply View 0 replies