|
Having a two year masters degree on the subject, I can give a go: - FAANG companies, top research universities, spinoffs of top research universities - Yes and no. Yes because FM orbits around philosophical questions like correctness, soundness, etc., which are not usually thought in your normal web shop. No because it is fundamental CS i.e. generic. - To prove properties, e.g. that a piece of software is bug-free. Usually this means things like reachability of states, which can be checked with e.g. TLA+. This may be a requirement in a critical system, where your normal support ticket could instead mean a death of someone. Asynchronous, distributed, and multi-core systems, which might be though to wrap your head around, might also be application areas. - This is super opinionated, but I would say learn about SMT solvers and forget the rest. For me, it clicked with SavileRow. Constraint programming was much more like an AI to me than any actual AI, since I just described the constraints and my programs solved itself. This way, you will get used with propositional logic, which is then easier to extend into TLA+ and some partial formal verification tools which prove state-properties with propositional logic and Hoare-triples from generic software. |
Theorem proving and SAT solving are classic AI subjects, don't forget. If we don't think of them this way today that's the usual "if it works, it's not AI" paradox (it's got a name I think, but I don't remember it).
I'd go as far as to say that theorem proving is honest-to-god AI, much more so than pattern recognition. After all, we know many animals that can recognise sights and sounds, but we only know of one animal that can state and prove theorems.