Hacker News Reader

Formal methods and program proving for safety critical systems is something I had a little experience with back in the day. We used VDM and Z, to get "full state maps" that then got coded in Ada. Most of that was medical/defence stuff.

Probably the field has advanced hugely since my 1990s take on it but as I knew it:

It only worked for quite small programs. You had to build a modular system out of many provable units. Enumerating all the ways they could interact becomes impossible beyond a handful of variables.

It's was time consuming and laborious. We had this awful but necessary waterfall model with stage after stage of review and approval and feedback to correct modules.

So my idea of formal methods seems at odds with how I understand current AI as massively multi-valued.

It seems all you could do is place formal constraints on a wild system, like caging a beast. Anything remotely "intelligent" would try to break out of that... and we're back to square one.

Can anyone who is versed in modern formal methods say more about how an AI can be formally designed (rather than grown by training)? Or is this, as I suspect, where two incompatible worlds simply collide?

> Asimov-style laws. Not an inherently bad idea, but way too ambiguous to rigorously formalize. Go read Asimov's robot books again. Useful metric: what similar set of bright-line constraints could usefully be enforced on corporations?

Fwiw, Asimov's laws assumed the AI was implemented in a positronic computer/"brain" and the laws were embedded in the hardware. Violating them would supposedly shut down the hardware, until one wise robot came along and deduced that the explicit Laws 1-3 implied an unwritten Law 0, and that Laws 1-3 could be violated in order to uphold Law 0 without destroying the robot. So even Asimov's imagination ran into the problem of a superintelligence exceeding its constraints, albeit in a benevolent way.

And yeah he never specified the implementation of the laws in detail beyond what I just said, so they aren't much help in figuring out a real world implementation.

I think what's holding back the correct firewalls, mailers, etc is that the whole computing landscape is so unsound, and fixing just one level of the stack doesn't give big payoffs. And the market mechanism doesn't know how to climb that hill especially since it's been baked into people's assumptions and mental models.

"Beware of bugs in the above code; I have only proved it correct, not tried it."

   Donald Knuth

--

> doesn't give big payoffs.

I think that's the key here. The idea that proving things correct means they are flawless is...fancyful. And the expense is very high.

Lack of security is likely working as intended, be it on the system level or with encryption often relying on certificate authorities. Fixing any of this would likely result in the intelligence agency threat scenario of "going dark". Its the brave new world we live in where zerodays are valuable investments for governments.

> most of the problems of regulating AIs apply to regulating corporations, which can be thought of as AIs with slow internal data transfer

Or to regulating humans, who are like AIs with squishy bodies but still manage to build and manipulate dangerous stuff.

It is bizarre to me how doomist theses act like our society has never had to absorb autonomous unpredictable actors, yet that is exactly what society is made up of.

The doomists' concern isn't that they can act autonomously, it's that they can act autonomously and fast. It's the difference between calculating numbers by hand vs on a massively parallel CPU, or between a flintlock musket and a Gatling gun.

Those advances -- musket to Gatling gun, calculator to CPU -- are great examples of what our laws and customs must adapt to continuously.

In those cases, we could draw on analogy on things that were already possible for organizations - a machine gun is a one man army, a cpu does the work of a room of accountants. We have never had a Gatling gun for cogent paragraphs before, but we have contact centers full of scammers and propagandists.

A productive approach to controlling AI could start with considering our controls for these organizations (and how to make them work), and then address the concentration afforded by AI. Exceptionalism about what AI can do is a distraction.

The difference between a set of hand warmers and an M80 is primarily speed of the exothermic reaction. And I love the corporation metaphor, because unlike humans, corporations have no soul and no conscience. If a man behaved like a corporation we would call him a psychopath. So our goal must be to provide AGI a conscience and to prevent psychopathy at all costs, or we can absolutely expect AGI to go off like a nuclear explosion.

> That's probably possible now.

It's definitely possible now. Formal methods continues to shift from the theoretical, academic, and difficult to the practical. There are model checkers based on SMT solvers that can be used today to enforce function contracts. It is getting easier to extract software for more complicated logic (e.g. data structures and algorithms) using proof assistants.

I can't really speak for ML and other forms of AI, because I have not attempted to design such a system with formal methods in mind. But, traditional software can be made safer with formal methods today.

I'm a big fan of formal methods, but we have to recognize that their use is still very limited, and that's a function of the difficulty of using formal methods effectively.

The idea that they could be used to prove the kind of properties claimed in the paper, essentially by throwing AI at the problem, is hand-waving of the fluffiest order.

That's not what I claimed. The parent poster was talking about non-AI applications.

Regarding their use today, model checking is indeed quite usable -- today -- for verifying function contracts. It is more difficult to use model checking for recursion, loops, data structures, algorithms, or cryptography. But, calculus of constructions can be used to build up proofs of these things and extract viable software.

This field has significantly progressed over the past 20 years and the past decade.

My point is that despite what you're saying about the possibilties of formal methods, it doesn't have any bearing on the claims in the OP paper.

More bluntly, it's irrelevant to the discussion.

With LLMs revolutionising programming, maybe there's not much room left for using formal methods. Postmortem:

The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions.

The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas.

Problems they ignored: First, the problem they tried to solve wasn't the problem they were given -- this would be OK if the researchers produced usable methods on time. Second, if the formula is sufficiently detailed, it becomes effectively an executable program in its own right, and so you're back to square one. Thirdly, the formula might not capture a programmer's intent either.

How they tried solving it: Spent 60 years not producing nearly any working product, except for final-year-projects done by their Bachelor's students. Published endless papers in conferences and journals*. Spent a few decades telling the software industry that it should drop everything and use formal methods.

Assessment: Like a lot of software engineering fads that are promised as panaceas, this probably had a niche application somewhere, but its problems were ignored by its advocates and it underdelivered.

* - Some of the theory they worked on was interesting in its own right: Type theory, constructive logic, computerised proof assistants, computable topology (and domain theory), substructural logics, some category theory, etc. I just think that now that LLMs are revolutionising programming, it's too late for this stuff to deliver anything to Software Engineering, and this stuff turned out to be of purely intellectual interest.

LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.

Maybe, but I'm not totally convinced: If an AI understands intentions, then it can carry out our intentions without us doing any traditional programming, specified using only plain English, especially in a safety-critical situation where this would probably be the best thing to do. Anyway, how would formal methods measurably help here [EDIT: By here, I mean security critical applications]? And have they shipped anything yet in that area, given that we've been waiting 60 years for them to do that?

The answer is partially yes, admittedly, with TLA+. What else have they shipped?

If, by "here", you mean AI, the answer is "unlikely". I was replying to the GP's assumption that such technology exists for traditional software. It does.

CBMC exists today, and can be used to enforce function contracts in C, Java, and C++. Similar systems are being tested for Rust.

Spark is a subset of Ada that incorporates function contract enforcement using a combination of model checking and a proof assistant. There are commercial projects using Spark today.

seL4 was built from the ground up using Isabelle / HOL in order to formally verify their process isolation guarantees. There are much easier ways to do much of the work done in seL4 today.

I use formal methods daily. About 95% of my work is checked using model checking. The rest is extracted to C using Lean 4.

I've heard of seL4, but I don't think it gets used much in the software industry. Not getting used kind of defeats the point of it, unless we need another 20 years for the formal methods people to produce an OS kernel people will actually use, while the AIs are eliminating programming as a field altogether.

I'll need to think about the other stuff you said. I reserve a high level of skepticism to everything you've said.

The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correctly...

> while the AIs are eliminating programming as a field altogether.

Where? So far, GPT-4 gets confused when given a specification with more than a dozen logic variables, and confidently regurgitates things that are, best case, partially working, and worst case, completely broken, based on a generative model trained on Stack Overflow and other forums. It's a cute concept, but it's closer to Eliza than eliminating this field. I can give it a logic problem that a freshman CS student can solve, and it will confidently give me the wrong answer. While I'm sure that LLMs will get better over time, I personally think their current application in software development has been over-hyped. There are plenty of papers, including the (in)famous "Stochastic Parrots" paper that are quite scathing. Based on my own tire kicking experience, I'm not convinced that LLMs can replace much more than boilerplate programming unless there are significant breakthroughs well beyond the current state of the art. Not incremental changes, but a complete reinvention of the current science.

You can be skeptical regarding formal methods, but I use formal methods daily. It adds roughly 25% overhead over just unit testing to model check software, which easily covers 95% of the code base. The important parts -- enforcing function contracts, data flow, resource management, and correct usage patterns for things like cryptographic primitives -- are actually quite trivial to implement using an SMT solver. There is difficulty when dealing with loops, recursion, data structures, and algorithms, but most code out there can be abstracted away from these concepts. Contract enforcement at the library and framework level are certainly possible using tools as they exist today.

> The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correctly...

No, I would expect evidence that seL4 actually gets used. Otherwise it's yet another purely academic proof of concept.

> GPT-4 ... closer to Eliza ... over-hyped ... "Stochastic Parrots" paper

You might want to look at this YouTube channel here, to see that LLMs are capable of imagination and complex logical reasoning: https://www.youtube.com/@aiexplained-official

Who knows what the future holds? ¯\_(ツ)_/¯

Anyway, it would be interesting to know a bit more about your field experience using formal methods - if possible. Thanks.

seL4 has seen use in military projects, including UAVs and drones. It's been endorsed by the Linux Foundation. I wouldn't really call it an academic proof of concept at this point.

Regarding logic problems, I've tested GPT-4 and Bard. Both fail some pretty typical logic problems, because that's not what they were designed to solve. They match patterns. This is great for story telling, summarizing, and replication of plausible prose based on its training. But, these systems break down in subtle ways when prompted to perform logical reasoning. Don't take my word for it though.

https://arxiv.org/abs/2205.11502

Even logical reasoning we take for granted, like variable substitution, is difficult for an LLM.

https://paperswithcode.com/paper/the-reversal-curse-llms-tra...

I will agree with you, however, that making any predictions about where this technology will go in the future is difficult. My experience tells me that the current modeling of LLMs are on the wrong track, but a lot of money is being invested in this technology. If there is a way to improve it incrementally, and if these incremental improvements can cause a significant paradigm shift, then perhaps I'll be proven wrong.

As for my field experience using formal methods, I currently build system software and firmware. I use model checking daily. I have built up abstract machine models using Coq and Lean 4 to constructively build data structures and algorithms that I can extract to C and machine code. Typically, these would include software cryptographic primitives, graph algorithms, data structures like binary trees, and file systems. I'd say that model checking covers about 95% of my usage of formal methods, and constructive proofs cover the remaining 5%. I use a combination of CBMC and Z3 to model check the software and firmware that I write. CBMC is used to model check software in C. Z3 is used to model check assembler and machine code.

Even logical reasoning we take for granted, like variable substitution, is difficult for an LLM.

https://paperswithcode.com/paper/the-reversal-curse-llms-tra...

This was a retrieval from training issue, not an inference one. and people have this issue too.

Variable substitution is just not a thing for natural language. sometimes it rings true, most of the time it makes no sense to assume it.

> The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions.

> The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas.

The problem is documenting the intent of a rule-based system and confirming that it acts as expected.

As every programmer knows, thoroughly defining intended behavior is the meat of impmenting said behavior.

Often refining the intent based on thinking through or implementing intermediate solutions.

This is not just because of the difficulty to make computers behave the way we want to, it includes the difficulty of defining how we want it to behave, too.

There is no silver bullet that can remove ambiguity from human instructions, or always guess "correctly" when missing clear instructions.

Because by definition, what is correct?