Название: Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings
Автор: Fairouz Kamareddine, Claudio Sacerdoti Coen
Издательство: Springer
Серия: Lecture Notes in Artificial Intelligence
Год: 2021
Страниц: 263
Язык: английский
Формат: pdf (true)
Размер: 10.7 MB

This book constitutes the refereed proceedings of the 14th International Conference on Intelligent Computer Mathematics, CICM 2021, held in Timisoara, Romania, in July 2021. The 12 full papers, 7 system descriptions, 1 system entry, and 3 abstracts of invited papers presented were carefully reviewed and selected from a total of 38 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teaching and geometric reasoning, and logic and systems, among other topics.

We present a comparison of several online Machine Learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician’s Machine Learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq’s standard library.

Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to Computer Science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.