The reason you wouldn't want to use ML for program transformations is that compiler analyses like constant folding are essentially fast, specialized theorem provers. When you need to know if an optimization is safe or not (is this expression equivalent to that one?), you want an exact solution, not just a pretty good guess, and there are known techniques that can give you just that.

However, you can use ML in areas where compilers use heuristics. For example, how many times should you unroll this loop, or should you inline function B into function A? Your program is going to be valid with or without inlining/unrolling, and the compiler needs an "intuition" of what's going to be best for performance. Right now, in most cases, this uses simple hardcoded rules.

The same goes for math. You wouldn't ask a neural network to certify whether a mathematical proof is valid or not, knowing it has been 99% accurate on the test set. You couldn't trust it to verify all the steps. However, you could use a neural network to help you guide a formal theorem prover in searching for a proof, as in which branches of the infinite tree of mathematical expressions should you search.