ML + FV = $\heartsuit$? A Survey on the Application of Machine Learning to Formal Verification

摘要: Formal Verification (FV) and Machine Learning (ML) can seem incompatible due to their opposite mathematical foundations use in real-life problems: FV mostly relies on discrete mathematics aims at ensuring correctness; ML often probabilistic models consists of learning patterns from training data. In this paper, we postulate that they are complementary practice, explore how helps its classical approaches: static analysis, model-checking, theorem-proving, SAT solving. We draw a landscape the current practice catalog some most prominent uses inside tools, thus offering new perspective techniques help researchers practitioners better locate possible synergies. discuss lessons learned our work, point improvements offer visions for future domain light science software systems modeling.