I  am a (full) Professor in the School of Informatics and hold a Chair of Artificial Intelligence. I am also:

Note: I am on sabbatical until the end of August of 2024 so responses to communications may be delayed.

My main field of research lies in AI Modelling, which spans areas such as interactive theorem proving, formal verification, process modelling, and AI/machine learning applied to health/care, medicine and other complex domains.

These days, I am particularly interested in the interactions between, and the combination of, symbolic/knowledge- and data-driven approaches to Artificial Intelligence. More information about current research interests, projects etc. can be found on our AI Modelling Lab website.

Opportunities:

PhD in AI for Health/Care and Medicine: Are you interested in developing and applying AI techniques ranging from formal verification to machine learning to real-world health and care processes? Are you interested in Explainable and/or causal AI for medicine, health and care? If the answer is yes to any of these questions, contact me. Funding may be available for good candidates.

PhD in Formal Modelling and Verification for AI: I am interested in supervising PhD students who wish to explore and develop the foundations of AI algorithms and approaches, e.g. machine learning (including Deep Learning) and logic-based learning, via formal modelling and verification. Candidates will need to have a strong  background in mathematics, an interest in computational logic/theorem proving and experience in machine learning and other aspects of AI. Funding is available for strong applicants.

PhD in Formalised Mathematics for Physics: I am looking for research students interested in  the  formalization of physics, whether theoretical or with a view towards its applications to the real world (e.g. the formal verification of safety properties related to robotics and autonomous navigation). Funding may be available for strong students.

Some of my latest research interests:

  • AI for health and care, with an emphasis on the modelling of computer- and human-based processes and their interactions using AI techniques, and on the use of of AI/ML for predictive and causal modelling in health and care. More information is available on the AIML webpage.
  • Formal verification for AI/ML, especially with regards to reinforcement learning, autonomous agents and differentiable programs.
  • Formalised mathematics: I am working  on the formal reconstruction in the theorem prover Isabelle of proofs from Euler‘s famous Introductio in analysin infinitorum (Introduction to the Analysis of the Infinite), first published in 1748 and on Euler’s Institutiones calculi differentialis  (Foundations of differential calculus). More generally, I am interested in all aspects of formalised mathematics.
  • Process modelling for complex systems including manufacturing, healthcare and beyond.

Latest Refereed Publications (kind of up-to-date, see the AIML’s publication webpage for more information):

  • Charlton E. C., Poon M. T. C., Brennan P. and Fleuriot J. D. (2023). Development of prediction models for one-year brain tumour survival using machine learning: a comparison of accuracy and interpretability. To appear in Computer Methods and Programs in Biomedicine. https://doi.org/10.1016/j.cmpb.2023.107482.
  • Schmoetten R., Palmer J. E. and Fleuriot J. D. (2022). Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL. To appear in the Journal of Automated Reasoning.
  • MacKenzie C., Huch F., Vaughan J. and Fleuriot J. D. (2022)  Re-imagining the Isabelle Archive of Formal Proofs. To appear in the proceedings of CICM 2022.
  • Gunatilleke J., Fleuriot J. and Anand. A. (2022). A literature review on the analysis of symptom-based clinical pathways: Time for a different approach?  PLOS Digital Health.
  • Restocchi V., Gaete Villegas J. and Fleuriot J. D. (2022). Multimorbidity profiles and stochastic block modeling improve ICU patient clustering. Artificial Intelligence for Health. IEEE/ACM CCGRID 2022, 925-932.

 Recent Working Papers:

  • DeLong L. N., Fernández Mir R., Whyte M., Ji Z., Fleuriot J. D. (2023). Neurosymbolic AI for Reasoning on Graph Structures: A Survey. arXiv:2302.07200.
  • Charlton, C. E.  and Poon, M. T. C.  and Brennan, P and Fleuriot, J. D. (2022). Comparing the Interpretability of Machine Learning Classifiers for Brain Tumour Survival Prediction. Available at SSRN: https://ssrn.com/abstract=4164349 or http://dx.doi.org/10.2139/ssrn.4164349
  • Chevallier M., Whyte M., and Fleuriot J. (2022). Constrained Training of Neural Networks via Theorem Proving. arXiv:2207.03880.
  • Chevallier M. and Fleuriot J.  (2021). Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. arXiv:2112.05996.

A Few Papers currently in Preparation:

  • Machine Learning for Rare Diseases: a Glioblastoma Case Study.
  • Mechanizing the Hyperdual Numbers in Isabelle/HOL.
  • L’Hospital’s Theorems and Euler’s Notions of Orders of Infinity in Isabelle/HOL.
  • Reconstructing Euler in Isabelle: The Exponential Series as an Infinite Polynomial.
  • Formalising Meek’s Method of Single Transferable Vote.

Comments are closed.