A program can be configured to behave smarter (better settings can improve apparent smartness in the sense of fit for purpose of behavior), which is kind of "prompting" an LLM to behave smarter, isn't it?
0. mostly
If you know how to prove something without making an initial assumption, let us know.
If you think you can reduce those assumptions, also let us know.
There should not be a "who" involved at all. That's not proof. That's trust.
Not 99% of programs. And even if they could, they never are.
Besides AI is a program in the same sense. Fix the seed/temperature, and you can verify it to perform according to its specifications. It's just that its specificactions include returning answers based on a weight model.
You misunderstand. Incomplete specification is still useful. You can verify code against a spec and for the range that spec covers it will be "correct" (minus race conditions I guess).
You can't verify anything with AI. Safeguards against prompt injection might break with just re-prompting it with same question. Or break when AI vendor updates their model.
If you're talking about verifying whether it produces the correct tokens, that's not generally something you can specify in advance with AI. I mean: if your task is one where you can precisely specify which output tokens are correct for a given input, then the task doesn't need AI, no?