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.