The Alignment Problem is the main problem of Artificial Intelligence (AI): how do we develop AI such that it respects human values? The problem gained more weight recently, primarily due to the prevailing skepticism surrounding the Large Language Models (LLMs) such as ChatGPT. The remarkable and frequently misconstrued capabilities inherent in these LLMs have prompted AI researchers to advocate for either a temporary halt in AI advancement (refer to "Pause Giant AI Experiments: An Open Letter") or an immediate evaluation of the human existential risk posed by AI (refer to "Statement on AI Risk").
I am not a signatory to either of these influential calls. I think that they cast too dramatic a light upon the present state of AI. I do however agree with the need for strong regulation of AI. In fact, such regulation should spur advances in AI, not hinder them, by increasing public trust in AI and providing the bounds within which all AI developers can fairly compete. These LLMs, undeniably powerful as they are, are still nothing but tools and remain fully subject to our discretion for deployment in either constructive or destructive pursuits. Therefore, a regulatory framework must also be built around the use of AI by the public, not just for development of AI.
I published two series of books, seemingly having nothing in common at first glimpse. First series is the Artificial Intelligence, Dreams and Fears of a Blue Dot series; it consists of two books. They are an adaptation of the aibluedot.com website to book form, with some editing done to account for feedback I received mostly on social media.
The second series is the Formal Software Development series; it also consists of two books. These two books are wrappers around a program of study I proposed way back in 2011.
How are they related? I mentioned above the need for AI regulatory action. Such action has been started in the US Congress, as well as the rest of the world. But there has been less work done on the issue of how we will verify that AI systems comply with regulations. The issue of software verification is fundamentally a mathematical issue, therefore it must be based on proofs, not on English (or any other natural language) text.
If we worry about AI extinguishing us humans, we should make sure that we can prove that it cannot do that. In other words, core parts of AI systems will eventually have to be specified formally (i.e. in a formal language), and those core software parts proven to satisfy their formal specifications. From a more practical personal perspective, in my work at sd-ai.org there will be a long-term need for such formal development when it comes to this writing and verifying of AI specifications. I put more details about this need in the SD-AI library.
