Disclaimer: I'm not especially knowledgeable about this topic, this answer presents my modest understanding.
As far as I know, there is no formal definition for solver simple because this a broad term which describes any system meant to solve a set of constraints or equations. Since every solver must have its own specific scope of problems that it can solve, very different systems can potentially be called "solvers". But the term is more common in the context of complex optimization problems, for example in the domain of multi-objective optimization. Also Prolog is the most famous example of declarative programming: the program is expressed as constraints that the Prolog engines solves.
To my knowledge the term "solver" is rarely used in the context of Machine Learning, probably because:
- ML algorithms don't always rely on optimization, in the sense that many algorithms are completely deterministic.
- Even the ML methods which rely on optimization are not "complex" in the sense that they only deal with very specific types of problems with numerical constraints, i.e. they are not general solvers which can take various types of constraints into account.
Some ML methods like genetic algorithms are specifically used for optimization problems, but (I think) that they are not called solvers because they rely on randomization, not mathematical methods.