I think the idea with this kind of thing is that ML can make pretty-good guesses really quickly, and then a formalized process can verify them (usually much more quickly than it could derive them). This hybrid model fits lots of different kinds of problems.