Yeah, this is however the same kind of discussion as back in the day Assembly developers not trusting FORTRAN compilers, so it is a matter of time, and funding.
The Fortran compilers were trying to get the answer right whereas the proposed funding void would at best be trying to avoid a segv.
What probably does have real merit is tying a superoptimiser to a LLM, provided you've got the SAT solver included in the mix as well to know if it worked.
