Hi. Your idea seems to be, that if probabilistic inference isn't able to recognize the theorems of a formal system, then we shouldn't expect language models to arrive at truth in general. 

I don't know if anyone has studied statistical regularities in theorems. You could ask on the "foundations of mathematics" list. But I think this is not a particularly effective critique of the truth capabilities of language models. 

On the one hand, the epistemology of theorems is quite different to the epistemology of worldly facts, like historical, subjective, or practical facts, and yet it's the latter that people are mostly concerned with. 

On the other hand, it's not clear that human mathematicians are inherently better than language models at spotting possible truths, since this involves intuition and insight, and that's all about heuristics - mental rules of thumb that generate plausible hypotheses. And language models are clearly heuristic rather than deductive in how they generate their responses. So there's no reason they can't get as good as human mathematicians, or better... And in fact the same applies to much of the worldly truths as well - so much of what we decide to believe has a heuristic origin, rather than arising from definite knowledge. 

If there is a serious difference between humans and language models, I'd say it hinges on consciousness. The human sense of what is true, is bound up with the mysteries of awareness, being, and the awareness of being. Conscious experience has a subjective and an objective pole, science focuses on the objective pole, and various scientific reductionisms try to reduce subjective ontology to entities from physics, computer science, or mathematics. In the distant past I wrote against this on Less Wrong, as well as advocating for the kind of quantum mind theory which says that consciousness is possibly grounded in what physicists call entanglement; something which implies that AI on a classical computer wouldn't be conscious. 

The relationship between AIs, humans, belief, and truth is very multifaceted. The potentials run from very good to very bad. I've tried to sketch why I think truth in formal systems is not very relevant to the enthusiasm for language models, and where I think there's a genuine ontological difference between AI and humans. I'll also add that there is some work on identifying what a language model actually "believes" [LW · GW] (spotted via June Ku's Twitter), which could perhaps be used to train a language model to care more about truth.  

Given a formal theory, there is no fundamental barrier to emitting only sentence prefixes that do have a continuation into a provable sentence of that theory. There is a random algorithm that can produce any provable sentence of a theory in this manner.

Note that this is very different from (and does not require solving) the generally undecidable problem "given an arbitrary prefix, determine whether it can be continued into a provable sentence".

Current LLM architectures can't implement such an algorithm directly, but in principle could do so with some sort of unbounded "scratchpad", just as humans would also require some form of unbounded external storage to implement such a process.

If I understand your proposal correctly (I may not), this might work in some technical sense but I'm not sure it's useful because it's not clear to me how truth is grounded here and so there's nothing actually constraining the analysis to verify truth instead of a proxy for truth.

I got a bit disappointing answers - people telling me how "this will not have impact" instead of answering the questions :) seriously, I think that it's a 15 minute problem for someone who knows theoretical CS well. It could have some impact on a very hard problem. Not the best option probably, but what is better?

Isn't it easier to spend 15 minutes to work on a CS theory problem, meeting new ppl, learning something ,instead of coming up with a long explanation of "why this is not the best choice"?

I'm a feminist but I'll give a trad cis example to illustrate this because I don't expect a feminist one to go well here (am I wrong?). In How I Met Your Mother the womanizer character Barney Stinson once had an issue. Women were calling him every minute and wanting to meet him. He couldn't choose which one is "the best" choice. As a result he didn't get to know any of them.

https://m.youtube.com/watch?v=_twv2L_Cogo

I feel it's the same - so much energy spent on "if it's the best thing to do" that even 15 minutes will not be spent on something new. Illusion of exploration - not actually trying the new thing but rather just quickly explaining why it's "not the best", spending most of the time "computing the best thing" and not actually doing it...

Am I not seeing it right? Am I missing something?

I think your intuition that learning from only positive examples is very inefficient is likely true. However, if additional supervised fine-tuning is done, then the models also effectively learns from its mistakes and could potentially become a lot better fast.