Learning Guided Automated Reasoning: A Brief Survey

arXiv:2403.04017v1 Announce Type: cross
Abstract: Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported …

abstract arxiv assistants automated cs.ai cs.lg cs.lo cs.ne cs.sc face general heuristics however mathematics practice reasoning survey systems theorem theory type