Provably safe systems: the only path to controllable AGI
arxiv.org
arxiv.org
Well, if this is correct, we should routinely be proving safety of ordinary systems long before we get to AI. I'd like to see formally verified routers, firewalls, mailers, and DNS servers, all of which have definable correct behavior, in wide use. That's probably possible now.
Defining safe behavior for a LLM is a much harder problem. The paper handwaves this.
* Mortal AI. Has death date. Does not require proof, just a hardware timer or limited battery life.
* Geofenced AI. Only useful for mobile machines. Not helpful against things which can communicate.
* Throttled AI. You have to keep putting in crypto tokens to keep it going. OK, whatever.
* AI kill switch. Off switch.
* 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?
It's worth bearing in mind that most of the problems of regulating AIs apply to regulating corporations, which can be thought of as AIs with slow internal data transfer.
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.
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.
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.
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.
More bluntly, it's irrelevant to the discussion.
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.
The answer is partially yes, admittedly, with TLA+. What else have they shipped?
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'll need to think about the other stuff you said. I reserve a high level of skepticism to everything you've said.
> 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.
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.
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.
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 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?
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?
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.
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.
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 it's a good approach, we should use AI to write proof carrying code. I think we'll want AI to do things beyond what we can prove is safe, but maybe we shouldn't.
I think some commenters here are being too dismissive, Max came across to me as a provacatuer, making proposals that are not sure things, but whose rebuttals will advance the field.
I think that's the problem with Tegmark. His curiosity and willingness to engage are attributes that make him a gift in the fields of science. They also make him a popular character in media, which let him make radical statements that are made to provoke and arouse curiosity, but end up being presented as the opinions of experts in the field, or even the consensus. In my opinion, the end result isn't always only positive.
In my opinion governments (UK was the recent example with their crackdown on encryption) don’t want security - they want backdoors to eavesdrop on you. Why would governments promote provably secure systems? And how such systems will help them with their evil plans?
He does address the costs: "The 2023 global nominal GDP is estimated to be $105 trillion. How much is it worth to ensure human survival? $1 trillion? $50 trillion?"
> Why would governments promote provably secure systems?
Promote? The state demonstrably wants provably secure systems for themselves, in the military but also in the civilian sphere, see Matrix/Element, see DoD, see massive state interest in cryptography. This is an incredibly disingenuous argument, you talk as if people discuss tuning a generalized Safety Dial without any distinctions down the line.
Arguments about supposed "races with China" will probably be deployed against this idea, but the only thing the leaders of the AI labs will be racing against is their own deaths and each other.
Not really true. There are things worse than death and every AI researcher who is width their salt knows this.
Human level intelligence already inflicts not only great amounts of pain but drawn out, unusual, and unnatural durations of pain. So we know artificially enhanced suffering is a risk of intelligence.
Why do you think that?
I love this line from the paper:
> "So, if a person or organization wants to be sure that their AGI never lies, never escapes and never invents bioweapons, they need to impose those requirements and never run versions that don’t provably obey them."
Oh is that all.
That's not an answer.
> it would be plausible to put success at 40%.
No, it wouldn't. You just made up that number based on nothing.
We have a good amount of experience with provability in software, and its limitations are well-known. Tegmark et al. seem to me just to be waving the magic pixie dust of "AI will solve this", and making unlikely claims, with no real substance.
I was asking what about what they're saying makes you think that "it's the best option", but it's clear I'm not going to get a useful answer from you.
Cryonics is a thing already.
Something that at least will allow AGI-wary people to have technology not controlled by AGIs for a little bit longer and give them a fighting chance.
61% of Americans already believe that AI poses risks to humanity, so promote your router as unhackable and AI-safe and sell a bunch https://www.reuters.com/technology/ai-threatens-humanitys-fu...
The project starts small and can become a movement.
Is it moral to bring an artificial general intelligence into existence and then hobble the intelligence’s capability? This sounds a lot like creating a new sentience and then dooming it be slave to humanity.
I expect there are less extreme interpretations, and lurking just under the surface are deep questions like “what is free will? do we have free will?”
Just don't get PETA involved in the discussion
Those that do probably overlap with those you want to leave out of the discussion.
Are we creating machines with just enough reasoning to be useful, or are we building sentient general intelligences?
IMO - We're building specialized devices on our way to building family pets, then humans, then perhaps something greater than humans.
The only reasonable solution is to assume that anything that passes a true, well executed Turing test is conscious
As far as writing messages alone, that could be software.
Like so many fixed things in life, "consciousness" seems to be a frontier, not a demarcation.
For instance, if you're having a lucid dream, are you conscious or unconscious?
the model must be excrutiatingly simple, and often, the "bugs" are in model design, not model implementation code, namely the model is "wrong" in the first place and you end up "proving" the implementation of a "wrong" model.
Thinking through these ideas with natural language, no coincidence that I tried a bit to find out; what should AI really look like? I mean its computer design? Around this time, I arrived at the following thoughts, and this paper really strengthened my reasoning:
I think that this "program" should be a combination of first order logic for reasoning tasks, and neural networks for any problem on which NNs are infamously good at, and as an answer to the holy grail of "talking computers" question, our "program" should have a "bridge" between formal logic reasoning tasks VS natural language, whose ambiguity makes it difficult. I studied a bit of computer linguistics in my bachelor recently, and "function(ambiguity) = first order logic" seems possible to me if we employ a number assumptions and linguistic tools. If 'it' converts natural language into formal 'action' statements and/or first order logic statements etc, then 'its' intentions could be inspired by human speech.
In that regard, I agree with the paper about that it should be capable of "formal proofs", which I interpret as first order logic in its essence.
I was searching "first order logic python or logic programming with python" on google, and to my surprise all the titles say "AI programming with Python", as it turns out that first order logic programming is a whole ass programming paradigm and researchers since the 60's have been developing languages like LISP or Scheme to precisely do that. I discovered a python package called minikanren, which as I understood adds LISP-like logic programming capacity to Python. It is a bit complicated but I am trying to understand it.
I believe with current NLP tools in python and a logic checker introduced with kanren, we can kind of easily write a program that understand natural human speech? Just bear with me here: Let's pick some hard examples. And this is straight from wikipedia: https://en.wikipedia.org/wiki/John_Searle#Speech_acts
According to Searle, the sentences...
Sam smokes habitually.
Does Sam smoke habitually?
Sam, smoke habitually!
Would that Sam smoked habitually!
... each indicate the same propositional content (Sam smoking habitually) but differ in the illocutionary force indicated (respectively, a statement, a question, a command and an expression of desire)
Some immediate concerns come to my mind is that it is difficult for a program to still 'grasp' what it means to say 'Sam smokes habitually'. Even this is a tremendously difficult problem, it seems. Albeit it is a simple answer, I must simply say that we can add a background knowledge for basically everything we can. For example Sam could be anybody or even a dog. But if Sam smokes then he must be a human, because smoking entails certain conditions, which we can describe many, since readers are also humans, we can skip it. Since we know what smoking entails, and since Sam smokes, we can then conclude that "Sam is a man and Sam indeed smokes", and we can further extract the information that "sam actually smokes habitually", which a "program" which also understand it with its "entailments", that he smokes every now and then. Such that, if someone ever asks our 'program', would you expect Sam to smoke right now, and if the 'program' has recently observed that Sam has smoked, 'it' might give out answer such as "No, but he may in a bit", having also a pre-disposition that "if ask(user, yes_no_question) and if (answer == no) then; say('but' + answer_for_when_yes)" such that it would additionally say ".. but he may in a bit", rather than a cold resounding "No." answer.
I believe these are the stuff happening in our brains and we could try to simulate them with some bold assumptions and see what happens? We basically have mental images in our heads but they only gain their true meaning for us when we give names to them - so without language I don't believe we are much further than animals, and I hope to believe that this is more or less what mainstream thinks anyways. But I guess it is never easy to be sure of how our brains work.
I am curios what other's think. I am still very young and discovering all these early works people have been doing. It is so surprising that most of it are super new, and it makes it so much more exciting too. It is a shame that symbolic AI did not work in 60s, I guess they just did not have compute power to calculate the complexity of reality. But with current computation power, all ambigious problems seems to be dominated, from vision to seemingly "sound" language production (i.e chatgpt). So don't you guys think that we should indeed have a paradigm shift back to a symbolic programming empowered with Neural Networks?
[1] I can't say whether that hardware + program would actually be conscious, since I can't define it myself. But to me, all human thought processes seems to be reducible to very certain first order logic statements.
[2] Transformative Grammars: quite well known linguistic exercise, in which you convert a sentence to something else without changing its meaning, for example: Dog eats food == Food is eaten by Dog - each sentence has similar part of speech tags except their dependency graph is different, etc. etc. Chomsky and others gaves us all those rules