Can we apply formal theory analysis to the truth of LLM outputs?

Hi! I am Sergia. I was doing AI safety research before, interning at CHAI Berkeley, and Google, and being in and about AIS discussions. I'm recently into AI ethics. While talking to Emily Bender on Mastodon, I learned about her "Octopus" thought experiment that got me thinking into how truthful can LLMs be, from a Theoretical Computer Science perspective. Full disclaimer: I'm leftist and liberal. I hope this does not stop the discussion about the CS itself :) I have a concrete research direction (more like a question to those who know Theoretical CS better than I do).

Epistemic status: intuition of a CS graduate and one who read/did a small project on the AIXI stuff, now a bit forgotten and in need of answers by someone who's more into it now

The setup

I want to examine how truthful those large language models can be, given that a) they're trained to predict the next symbol b) they work in $O\left(\text{length of string}\right)$ and c) in their training data there are both true and false statements.

In what follows I focus only on a), as I feel a) is enough of an assumption to cause enough trouble

I want to model it like this. We have some very basic formal system (maybe even not an induction axiom). We have a Turing machine that prints true statements one by one by applying axioms that are applicable to existing true statements.

I choose this setup (a simple formal system) over full Set Theory because in our, real-world English language we rarely use infinite induction, Goedelian statements, and all that. It's more of a basic formal theory ("Socrates is a man, therefore..."). LLMs are known to fail sometimes even on those "basic logic" tasks like counting or "Alex was 5 years old when he was older than Jane by 1 years..." -- the readers here know more about those probably than I do.

For every $K$ we have a dataset of the first $K$ true statements, given by a machine  $T_K$.

First question: is it true that for formal systems, we can do this - print all true statements like this?

We are interested in creating a Turing machine that, given the beginning of a true statement, will write the rest so that it's a valid true statement.

We use Solomonoff induction ("the best Machine Learning algorithm") which outputs a posterior over strings given the dataset and a prior. This procedure is uncomputable but it outputs a TM doing the job (predicting the rest of the string). We fix some prior

We apply Solomonoff induction to the output of $T_1,T_2,...$ and obtain resulting probability distributions

$P_K\left(\text{rest of the string representing a true formula}|\text{beginning of the string}\right)$

Those are computable and represented by some Turing machine. This way we get $P_1,P_2,...$
 

Questions

For set theory, we know that the true $P\left(\text{rest of the string}|\text{beginning}\right)$ is uncomputable, otherwise, we can establish truth of a formula with it.

Question 2: is it computable for simpler theories, say, ones without an induction axiom? In other words, can we obtain the probability that a true formula starts with a $\forall$ or with a symbol "$x$"?

Question 3: are approximations to this probability computable? In other words, is it possible to obtain a bound, say, "the first symbol of a true formula starts with '$\forall$' with probability in 0.1 to 0.2", with an algorithm that can give any precision in finite time?

My intuition is that the answer is "no" for questions 2 and 3. This would mean that when we feed a large language model more and more data, it will simply memorize true statements it has seen, but it will fail to generalize to unseen statements.

My intuition is that if we plot the probability of a true formula starting with, say, "$\forall$", only estimated via count from finite "observations of true formulas" $P_K\left(\forall |\text{empty}\right)$, this chart will go up and down, with no limit value. Like, if a lot of true formulas in the batch of the first 1000 start with a "$\forall$" does not mean in the next 1000 there will be also a lot of true formulas starting with "$\forall$"

Specific question 4: would this function have a limit value? Does the answer change if we have a decidable theory?

Question four is a specific case of question 3: obtaining this approximation via $P_K$
 

Motivation

This potentially slows down the obsession with LLMs, as "learning truth by observing finite samples of it" is a doomed task: truth does not generalize this way.

Inspiration: there are linguists, humanities people, and people who are already hurt a bit with LLMs (mental health patients, artists, people in places affected by misinformation...) who say something like this, but tech people dismiss it as "more layers and more posts from Reddit in the data will solve everything"), I want to write it with them and with you. Well, there are superintelligence concerns and all that as well.
 

Potential conclusion

(if Q2-4 have negative answers)

The explanation would be that without learning the specific context where the LLM is deployed, without real feedback on an actual task (say, if the patient recovered), they are not very meaningful

Like, it's really hard to learn about a subject just by listening to lectures - it is something, but usually, when doing exercise sessions it becomes clear that the lecture was not clear at all, and then task-specific feedback and task-specific activities (brainstorming with someone who knows, asking the professor, etc) are required. Same with therapy - a freshly graduated therapist with no experience is probably not a good choice

The rest is up to the community, as I forgot most of theoretical CS by now :) Thank you!

License: CC A, Credits to my friend Arshavir for inspiring my thinking into this as well