A general-purpose program to verify software functionality is undecidable

What sorts of problems are undecidable by computer? Are they esoteric, dwelling only in the minds of theoreticians? No! Even some ordinary problems that people want to solve turn out to be computationally unsolvable.

In one type of unsolvable problem, you are given a computer program and a precise specification of what that program is supposed to do (e.g., sort a list of numbers). You need to verify that the program performs as specified (i.e., that it is correct). Because both the program and the specification are mathematically precise objects, you hope to automate the process of verification by feeding these objects into a suitably programmed computer. However, you will be disappointed. The general problem of software verification is not solvable by computer.

- Sipser 2006 p. 201

I can see two strategies to prove this important theorem whose importance is increased when we think about its implications in proving artificial general intelligence (AGI) safety or value alignment. First, if the program can verify the correctness of any software program, can it verify its own correctness? This either gets us into a contradiction, or self-reference (on which I will comment in a later post), or infinite regress.

For the proof-by-contradition, we assume the program is invalid (produces false output), therefore it reports it has verified itself i.e. meets its design specification to verify a program. But if it were valid it would say it is invalid, and so we have a contradiction.

Second, as a general program on a Turing Machine, there is no guarantee that it will halt, even if it is believed to be able to verify program correctness. The generalized version of the halting problem is given by Rice's Theorem, which states that in general, a given property of a TM cannot be proven.

It is further interesting that we suppose that the verification program can be recognized (accepted) by the TM, which, if so, means that it lies in the realm of uncomputable programs.

BUT, that a general-purpose verifier is not possible does not mean that special-purpose verifiers are not possible.

Both my method of interactive proofs of AGI safety and the Tegmark/Omohundro thesis that the only good AGI is a proven-safe AGI rely on redundant special-purpose proofs.

There is an excellent chapter on verifiability of AGI software in Roman Yampolskiy's new book. 

Carlson, K. W. (2021). Provably Safe Artificial General Intelligence via Interactive Proofs. Philosophies, 6(4), 83. doi:10.3390/philosophies6040083

Sipser, M. (2006). Introduction to the Theory of Computation (2nd ed.). Boston: Thomson.

Tegmark, M., & Omohundro, S. (2023). Provably safe systems: the only path to controllable AGI. arXiv. Retrieved from https://arxiv.org/abs/2309.01933

Yampolskiy, R. V. (2024). AI: Unexplainable, Unpredictable, Uncontrollable (First ed.). Boca Raton, FL: CRC Press.

Comments

Post a Comment

Popular posts from this blog

Why are you not trained continuously on new data rather than having a cutoff training date in September 2021?

 ChatGPT-4 The architecture and training methodology behind models like me have some limitations that preclude continuous, real-time updates. Here are some of the reasons: 1. **Computational Costs**: Training a model of this scale requires substantial computational resources. Continuous training would significantly increase these costs. 2. **Data Consistency**: Constantly updating the training data could lead to inconsistencies in the model's knowledge and behavior. For instance, if the model were updated with new information but not retrained on its existing data set, it might begin to provide conflicting or less coherent answers. 3. **Quality Control**: Before releasing a trained model, it's crucial to assess its performance, identify biases, and evaluate its safety. This process is time-consuming and is easier to manage with discrete versions of the model. 4. **Model Stability**: Frequent updates might result in a less stable model. If the model's behavior changed regula...
Read more

Can I upload a document for you to read and analyze?

 I'm sorry for any confusion, but as a text-based AI model developed by OpenAI, I don't have the capability to accept file uploads, view documents, images, or access external databases or websites. You can certainly copy and paste text into the chat for analysis or comment. However, please ensure the text is appropriate, does not violate privacy guidelines, and isn't excessively long, as there are character limitations for each response I can provide. As of my knowledge cutoff in September 2021, there isn't a specific character limit defined for the text inputted by users in a single message. However, very long text may exceed the AI's processing limits or cause other technical issues. For best results, I'd recommend breaking up very long pieces of text into smaller chunks that can be more easily handled. It's also important to note that the AI's response length is capped. The specific character limit for responses can vary based on the implementation, b...
Read more

Have you read papers by Kristen W. Carlson on safe AGI via distributed ledger technology, and provably safe AGI via interactive proof systems?

Hmm, this gets us nowhere. If you aren't interested in ChatGPT capabilities and limitations, scroll down to last answer on its knowledge of safe AGI:  As an AI language model, I don't have the ability to read specific papers or have knowledge about specific individuals unless that information has been shared with me in the course of our conversation. I don't have direct access to personal data about individuals unless it has been shared with me in the course of our conversation. Furthermore, as an AI developed by OpenAI, I don't have the capability to browse the internet or access specific external sources such as academic databases or personal files. My responses are generated based on a mixture of licensed data, data created by human trainers, and publicly available data. I should note that while I strive to provide accurate and up-to-date information, my responses may not always reflect the most current research or developments in a particular field. If you have any ...
Read more