3 ms·
> there's no way to make them generate something semantically valid 100% of the time. You don't need to generate semantically valid reasoning 100% of time for
by nextaccountic 2y ago
> there's no way to make them generate something semantically valid 100% of the time.
You don't need to generate semantically valid reasoning 100% of time for such an approach to be useful. You just need to use semantic data to bias them to follow semantically valid paths more often than not (and sometimes consider using constraint solving on the spot, like offloading into a SMT solver or even incorporating it in the model somehow; it would be nice to have AI models that can combine the strengths of both GPUs and CPUs). And, what's more useful, verify that the reasoning is valid at the end of the train of thought, and if it is not, bail out and attempt something else.
If you see AI as solving an optimization problem (given a question, give a good answer) it's kind of evident that you need to probe the space of ideas in an exploratory fashion, sometimes making unfounded leaps (of the "it was revealed to me in a dream" sort), and in this sense it could even be useful that AI can sometimes hallucinate bullshit. But they need afterwards to come with a good justification for the end result, and if they can't find one they are forced to discard their result (even if it's true). Just like humans often come up with ideas in an irrational, subconscious way, and then proceed to rationalize them. One way to implement this kind of thing is to have the LLM generate code for a theorem prover like Coq or Lean, and then at the end run the code - if the prover rejects the code, the reasoning can't possibly be right, and the AI needs to get back to the drawing board
(Now, if the prover accepts the code, the answer may still be wrong, if the premises were encoded incorrectly - but it would still be a net improvement, specially if people can review the Coq code to spot mistakes)