Detail

Combining Machine Learning with Automated Reasoning in Large Formal Knowledge Bases

Induction (suggesting and learning conjectures, principles, and explanations from data) and deduction (drawing conclusions from principles) are two frequent reasoning methods used by humans. Recently, in the field of formal, computer-understandable mathematics, large formal knowledge bases have been created, allowing AI researchers to experiment with various novel combinations of inductive and deductive reasoning. At the same time, the search space of purely deductive general reasoning tools becomes very large when working over large mathematical theories, and needs to be complemented by various heuristics. A promising way how to automatically find and optimize such heuristics is again induction, and particularly machine learning from previous problems.
In this talk the field will be shortly introduced. The MaLARea system combining in a closed loop automated reasoning tools with machine learning from solved problems will be introduced, and evaluated on a large-theory benchmark. The various existing and possible ways of how to do machine learning over large bodies of computer-understandable mathematics will be discussed.