I agree they'd be better for improving something human driven. I previously suggested plugging learning architectures provers to either spot opportunities to feed terms to automated solvers or create new tactics. Similarly, they could augment the automated solvers to improve their heuristics. Improving heuristics or models of data that changes quite a bit in different use cases seems to be the strong suite of these learning architectures. Whereas, there's already efficient algorithms for things like search or validating stuff. Might as well keep them in initial design attempts.