Machine learning and formal methods for sport analytics

The main focus of my PhD period is related to the concept of sport analytics. During the last few years, sports analytics has been growing rapidly. The main usage of this discipline is the prediction of soccer match results, even if it can be applied with interesting results in different areas, such as analysis based on the player position information. This context has been explored through three different steps: the analysis and recognition of human activities, the adoption of machine learning on soccer data and, at the end, the application of formal methods on sport analytics scenario. In this way, I want to explore the strengths and the weaknesses of different techniques. Human activity recognition is attracting interest from researchers and developers in recent years due to its immense applications in wide area of human endeavors. The main issue in human behaviour modeling is represented by the diverse nature of human activities and the scenarios in which they are performed. These factors make this aspects challenging to deal with. Then, machine learning techniques have been used in order to make some consideration on a great amount of data related to soccer matches. Specifically, these type of techniques have been used in order to predict soccer game results and player positions during a match. The last step is about the usage of formal methods in order to provide more explainability and interpretability of the results obtained. With the application of formal methods based approach, I try to detect the playing style of a soccer teams, providing transparency of the results obtained. I model soccer teams in terms of automata and, by exploiting model verification techniques, I verify whether a playing style, expressed by means of a temporal logic formula, is exhibited by the team under analysis. This information can support the coach in determining the strategy of the team while the match is in progress. The experimental analysis confirms the effectiveness of the proposed method in soccer team behaviour detection, obtaining promising results, compared with standard baseline approaches.

L’obiettivo principale del mio periodo di Dottorato riguarda il concetto della Soccer Analytics. Durante gli ultimi anni la Soccer Analytics ha registrato un’enorme diffusione. Di solito, in quest’ambito, i ricercatori si sono concentrati sulla predizione dei risultati delle partite anche se, soprattutto negli ultimi tempi, c’è stata un’attenzione particolare nello studio dei dati posizionali. Il mio periodo di Dottorato può essere diviso in tre parti fondamentali: nella prima parte ho preso in considerazione l’analisi e lo studio delle attività svolte dall’uomo; nella seconda parte, mi sono soffermato sull’applicazione di tecniche di Machine Learning applicate al contesto della Soccer Analytics per poi passare, nell’ultimo periodo, all’utilizzo delle tecniche di verifica formale sugli stessi dati. Alla fine di questo percorso ho potuto confrontare i punti di forza e di debolezza di tutte le tecniche utilizzate. L’analisi delle attività umane (Behavioural Analysis) è di grande interesse per i ricercatori a causa della grande quantità di applicazioni possibili di questa disciplina. Quando si parla di questo tipo di disciplina, il primo problema da affrontare consiste nel dover gestire e modellizzare le attività e gli scenari presi in considerazione che, chiaramente, possono essere di diversa natura. Questi aspetti possono essere molto difficili da risolvere. Dopo aver trattato lo studio e l’analisi delle attività umane, sono passato all’applicazione delle tecniche di Machine Learning su dati relativi al contesto calcistico, in maniera tale da poter gestire la grande mole di dati disponibili. Nello specifico, sono state utilizzate delle tecniche supervisionate per predire il risultato di partite di calcio e per identificare la posizione occupata dai giocatori in campo in diverse situazioni di gioco. L’ultimo step riguarda l’utilizzo di tecniche di verifica formale sugli stessi dati presi in considerazione nella seconda parte del lavoro, cercando di ottenere una migliore “explainability” riguardo ai dati a disposizione. L’obiettivo, in questa ultima parte del mio lavoro, riguarda l’identificazione dello stile di gioco delle squadre prese in esame. Per ogni squadra, che viene rappresentata mediante un automa, cerchiamo di identificare lo stile di gioco (offensivo o difensivo) utilizzando tecniche di Model Checking. Le proprietà che vengono verificate sono definite grazie all’aiuto di un esperto di dominio. Questa informazione può essere utile per l’allenatore, che può verificare, durante lo svolgimento della partita, se la squadra sta rispettando le sue direttive. Tutte le analisi, svolte nei vari step del progetto, hanno portato a risultati molto promettenti se confrontati con quelli presenti in letteratura.