3 ms·
I think I have to know what chain of reasoning is behind this or that fact and/or deduction. i would like to be able to verify that. For example, the proof of
by thesz 3y ago
I think I have to know what chain of reasoning is behind this or that fact and/or deduction. i would like to be able to verify that.
For example, the proof of the absence of solution in SAT should be accompanied with the easily verifiable chain of reasoning. This shows the absence of incorrect deductions and missing assignments. Another example is autovectorization in contemporary compilers, they can show you why parts of your loops are not eligible for vectoriztion.
All LM's can do is to show me that these parts of those inputs are important for that output, but nothing else. Thus, they cannot be trusted even for minimally critical tasks.
- pixl97 3y agoEven you can't do that yourself. You can only mad post ad-hoc justifications for the choices you made.
- thesz 3y agoWhat cannot I do myself? Look at the output of gcc -ftree-vectorizer-verbose=2? Run the verifier after picosat? I did both.
- thesz 3y agoTo illustrate: https://arxiv.org/abs/2401.05566 https://arxiv.org/abs/2401.05566 One can teach LLM to write good code now and bad code in future (when everyone lower their guards). And no one can prove who and how made LLM to do that. Also, no one can prove formally the absence of such a plant.