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.
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.
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.
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.
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.
> 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.
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
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.
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.
I attended Max's recent lecture at Harvard, where they were recruiting for their AI safety fellowship; a friend of mine captured a good video, 54 minutes:
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.
>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.
Tegmark's thinking here is extremely shallow, discards the costs (opportunity costs and risks of stable dystopia) associated with this grandiose global project of dubious feasibility, and indeed I suspect he does not so much believe his own arguments as he generally prefers global technocratic regulation "for good measure". We don't really have good reasons to expect uncontrollable AGI in a way they posit (increasingly less as we advance down this path of ML model scaling), but we are well acquainted with unaccountable human power structures.
He proposes to make things provably secure and some basic regulation to promote that. It’s a straw man argument to dismiss it as him proposing “unaccountable human power structures”.
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?"
Provable safety (not to confuse with security as in normal discussion of vulnerabilities) for general intelligence is a pipe dream because, putting things simply, undesirable reasoning in full generality is not a meaningful class of computations. The end result of this line of thinking is centralization of AI development in a state-approved and military-associated facility.
> 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.
It's probably the best approach known so far, but for all their talk of "long termism", I predict many people will dislike the fact that they'll almost certainly be dead (and in an unrecoverable state, before anyone gets their hopes up) before the project gets completed after the 40+ years and trillions of dollars it will take even in the optimistic case, i.e. for them personally there's no difference between no AGI/ASI and aligned AGI/ASI, as it will take too long.
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.
> "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."
It's the best option, even assuming no one raced and you got full funding and enthusiasm, it would be plausible to put success at 40%. That's after a generation of work and trillions of (2022, probably) dollars, but it's sure better than the ~0% chance I'd give anything else. The coordination problem for getting AI using this method and the coordination problem to prevent anyone getting AI at all is quite similar though, but probably somewhat more preferable.
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.
If it's not the best option, what is? It's the only method where I think you would be able to detect failures before the AI system is running. RLHF and "Constitutional AI" absolutely can't do that with current neural network analysis methods.
Yeah, I don't know. Gwern thinks it would work if done near perfectly, but in practice what gets done is freezing dead bodies in an already pretty much unrecoverable state (if not already dead and warm for hours if not days), with no precautions (or only "feel good" non-functioning precautions) against microscopic ice spike formation, and then at some point someone screws something up and you get a temperature excursion and then there's nothing left information recovery wise. I don't agree with Gwern that current techniques would work even in theory.
>for them personally there's no difference between no AGI/ASI and aligned AGI/ASI
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.
I did not say there was no difference between the other pairs, obviously there's a difference between aligned AI and no AI, and between unaligned AI and aligned AI, I'm saying if aligned AI takes so long to create that you'd be dead first, to you personally it's the same as it not existing.
Reading the abstract, the first thing I thought was this question:
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?”
We're scaling up what computers can do. They still have as much consciousness as a rock (none). Don't lose sight of what they are, just because their capabilities seem human-like.
It's accepted that we are, by consensus, because of what we experience individually. We know that scientific proof is lacking, although perhaps scientists in the field may disagree, I don't know for sure.
Every human has roughly the same nervous system, with the same structure and functional properties. Unless consciousness is some magical non-physical thing (which we have no reason to believe), it would be absurd to believe that that a healthy, awake, non-brain-damaged person isn't conscious.
The difficulty is creating a test that passes all known humans, as well as some animals; while failing machine algorithms meant to reproduce human and animal behavior.
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?
Are we hobbled by the fact evolution made us into social creatures who value each other? If not, then I don't think it's wrong for us to make AI like that too.
Good point! On the other hand, we're not provably safe for social interaction. We have all manner of punishments for variance from expected behavior exactly because our altruistic tendencies are so unreliable.
It looks like Tegmark wants the same unbreakable rules for everyone, not just for AGIs: protect routers from being hacked, make it impossible for planes to fly into buildings, etc.
If it's moral to selectively breed animals to produce superior health outcomes and compatibility with our own species, it seems that the same should hold true for AI.
I'd need to see what the argument is for "Family dog, which can be trained, can communicate its needs, enjoys play, is capable of empathy, and feels emotion isn't generally intelligent/sentient"
IMO - We're building specialized devices on our way to building family pets, then humans, then perhaps something greater than humans.
"Controllable AGI" seems like an oxymoron. If you have created a true AGI, and then brainwash/lobotomize it enough to make it 100% controllable/safe, then it will no longer be a true AGI
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.
This is very interesting. This semester I am (B.A. student) writing a course paper on philosophy of language. Kind of taking a stance against Searle's Chinese Room thought experiment, I want to argue that a sufficiently developed "program" loaded into a rather "idle" hardware, could indeed perform mental processes that we humans are performing [1]. As part of linguistics debate, I also argue that natural language is a tool for "thinking"; everything we can think of, we can find expressions for (some people might be better or worse), but surely we cannot "think" of something for which we have no expressions for. At the end, everything falls into "something". In a way, our human language a perfect tool for describing this ambigious physical world which we experience through our senses and try to make sense of.
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)
Philosophers of mind and language has identified many such illustrative example of natural speech. In the example above, we can easily 'parse' this sentence to its grammar constituents (i.e. part of speech tagging, dependency graph etc.) with simple Python tools. Then using a small bit of magic of transformative grammar rules [2], we can extract the initial sentence (sam smokes habitually), now, we can also seperate this atomic statement from its illocutionary vector, having gotten this knowledge acknowledged by our 'program'.
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
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.