[logicchains]

>There's no fundamental reason to think it's impossible

There is, although we don't have a formal proof of it yet. Current LLMs are essentially Turning complete, in that they can be used to simulate any arbitrary Turing machine. This makes it impossible to prove an LLM will never output a certain statement for any possible input. The only way around this would be making a "non-Turing-complete" LLM variant, but it would necessarily be less powerful, much as non-Turing-complete programming languages are less powerful and only used for specialised tasks like build systems.

[creer]

"Non-Turing-complete" still leaves you vulnerable to the user plugging into the conversation a "co-processor" "helper agent". For example if the LLM has no web access, it's not really difficult - just slow - to provide this web access for it and "teach" it how to use it.

[potatoman22]

Couldn't you program the sampler to not output certain token sequences?

[namibj]

Yeah. E.g. GPT-4-turbo's JSON-mode seems to forcibly block non-JSON-compliant outputs, at least in some way. They document that forgetting to instruct it to emit JSON may lead to producing whitespace until the output length limit is reached.

In related info, there is "Guiding Language Models of Code with Global Context using Monitors" ( https://arxiv.org/abs/2306.10763 ), which essentially gives IDE-typical type-aware autocomplete to an LLM to primarily study the scenario of enforcing type-consistent method completion in a Java repository.

[edgyquant]

That’s seems extremely difficult if not impossible. There’s a million ways an idea can be conveyed in language.