View: session overviewtalk overview

09:00 | How can we make trustworthy AI? ABSTRACT. Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, adaptability, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes. |

10:00 | Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation PRESENTER: Alexey Gonus ABSTRACT. This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions. |

10:30 | GeoGebra Discovery (system entry) PRESENTER: Zoltán Kovács ABSTRACT. GeoGebra Discovery is an experimental version of GeoGebra, dealing with automated reasoning in elementary geometry. It contains some bleeding edge features of GeoGebra that are under heavy development and therefore not intended for every day use yet, so they are not included in the official GeoGebra version. Also, in some cases, there is no consensus on whether to include certain elements in GeoGebra or to leave them out (for example, because they are too specific for a particular audience). GeoGebra Discovery is maintained by a group of researchers from various fields of interest, including mathematics education, algebraic geometry and computer science. |

11:30 | Learning Support Systems based on Mathematical Knowledge Management PRESENTER: Michael Kohlhase ABSTRACT. To cater to the increasingly diverse student bodies, higher education has to personalize education. In times of stagnant educational budgets and staffing problems, this can only be achieved via adaptive, interactive learning support services. In this paper we show how these can be generated by modeling the domain, the learner competencies, and the rhetoric and didactic relations among learning objects, re-using existing technologies and systems of mathematical knowledge management. |

12:00 | Teaching Linear Algebra in a mechanized mathematical environment PRESENTER: Robert Corless ABSTRACT. This paper outlines our ideas of how to teach linear algebra in a mechanized mathematical environment, and discusses some of our reasons for thinking that this is a better way to teach linear algebra than the “old fashioned way.” We discuss some technological tools such as Maple, Matlab, Python, and Jupyter Notebooks, and some choices of topics that are especially suited to teaching with these tools. The discussion is informed by our experience over the past thirty or more years teaching at various levels, especially at the University of Western Ontario. |

12:30 | Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters PRESENTER: Jan Frederik Schaefer ABSTRACT. When publishing papers, researchers in mathematics and related disciplines typically focus on the presentation, i.e. type-setting, of their ideas and provide little semantic information. This impedes the development of services that benefit from semantic information, such as semantic search and screen readers for vision-impaired researchers. As a remedy, there have been attempts to infer semantic data from already published papers using small programs that we call spotters. Unfortunately, there is no standardized format for semantic annotations and spotter authors typically invent their own format. This leads to two problems: i) there is no ecosystem of tools for common tasks like the visualization of results or the manual annotation of a gold standard, and ii) re-using, evaluating and combining results becomes very difficult. In this paper, we address the issue by describing a standardized, flexible way to represent semantic annotations, using semantic web technologies and, in particular, the web annotation standard. Furthermore, we describe SpotterBase, a set of tools to help with processing the annotations and creating new ones. |

14:00 | AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae PRESENTER: Jan Frederik Schaefer ABSTRACT. Mathematical formulae are a significant challenge for various services that help us access scientific publications. For example, finding relevant formulae with a search engine is difficult and screen readers struggle to verbalize them in an understandable way. We believe that such services could be improved if more semantic information is available. To automatically extract this information, we typically need manually annotated data sets for evaluation and, potentially, for the training of machine learning models. However, mathematical formulae also present a major challenge for annotation tools, as they cannot be presented well as plain text which is required by most existing tools. In this context, we present AnnoTize, a new annotation tool. It can create, display and update annotations for HTML5 documents and was specifically designed to support the fine-grained annotation of formulae encoded in MathML. As manual annotation can be tedious and time-consuming, AnnoTize offers several features to speed up the annotation process for large annotation tasks. |

14:30 | PRESENTER: Haruka Miyata ABSTRACT. This paper discusses the enhancements we have made to the Mizar Extension for Visual Studio Code (VSCode). The first part of the paper explores the creation of the Mizar Server and client-side infrastructure, developed to support the web version of the Mizar Extension for VSCode. The latter part provides an update on the development of the formatter function and reports on the progress of our research into coding assistance using ChatGPT. |

15:00 | Extracting Mathematical Concepts with Large Language Models PRESENTER: Valeria de Paiva ABSTRACT. We extract mathematical concepts from mathematical text using generative large language models (LLMs) like ChatGPT, contributing to the field of automatic term extraction (ATE) and mathematical text processing, and also to the study of LLMs themselves. Our work builds on that of others, %especially~\cite{collard2022}, in that we aim for automatic extraction of terms (keywords) in one mathematical field, category theory, using as a corpus the 755 abstracts from a snapshot of the online journal \emph{Theory and Applications of Categories}, circa 2020. Where our study diverges from previous work is in (1) providing a more thorough analysis of what makes mathematical term extraction a difficult problem to begin with; (2) paying close attention to inter-annotator disagreements; (3) providing a set of guidelines which both human and machine annotators could use to standardize the extraction process; (4) introducing a new annotation tool to help humans with ATE, applicable to any mathematical field and even beyond mathematics; (5) using prompts to ChatGPT as part of the extraction process, and proposing best practices for such prompts; and (6) raising the question of whether ChatGPT could be used as an annotator on the same level as human experts. Our overall findings are that the matter of mathematical ATE is an interesting field which can benefit from participation by LLMs, but LLMs themselves cannot at this time surpass human performance on it. |