AIAI Seminar-Monday 15 April-Talk by Richard Schmoetten, James Vaughan and Waylon Li

Speaker: Richard Schmoetten

Title: Vector Fields in Isabelle/HOL

Abstract: Manifolds allow for a generalisation of smooth functions beyond Euclidean spaces. I will give a quick overview of our formalisation of smooth vector fields on manifolds. In particular, I will discuss some of the difficulties we faced when working with mathematical structures involving type-based entities as well as definitions over subsets of a type.

Speaker: James Vaughan

Title: Adaptable machine learning for premise selection

Abstract: Identifying the relevant theorems required for a proof is one of the most important steps in solving it automatically. Given the amount of mathematics currently available to proof assistants, contemporary premise selectors learn when a theorem is relevant from how it is used in historical proofs. However, recently proven theorems have had little opportunity to be used, and these are frequently promising premises for upcoming problems. In this talk, I will discuss how we are using machine learning models from recommender systems to quickly adapt to these new theorems.

Speaker: Waylon Li

Title: Learn to Rank Risky Investors: A Case Study of Predicting Retail Traders’ Behaviour and Profitability

Abstract: Identifying risky traders with high profits in the financial market is crucial to market-makers, such as trading exchanges. This would allow market-makers to make real-time decisions on regulation compliance or hedging, ensuring effective risk management. Nevertheless, it remains a challenging task due to the complexity of market and individual traders behaviours. Traditional approaches often fall short in capturing the dynamic and complex nature of traders behaviours. In this talk, I will introduce our novel method by reframing the problem of identifying risky traders as a ranking task, employing LEarning-TO-Rank (LETOR) algorithms.