About me
I'm a final year Computer Science PhD student at the University of Edinburgh, supervised by Dr Paul Jackson. I'm part of the Laboratory for Foundations of Computer Science and the AI Modelling Lab. Previously, I obtained an MEng in Mathematics and Computer Science from Imperial College London (see my thesis) and a Logic Year certificate from the Institute for Logic, Language and Computation.
My research is in formal verification, with a focus on interactive and automated theorem proving, and validated numerics. Currently, I'm developing CvxLean, a verified convex optimization modeling framework written in Lean. The tool allows users to formulate optimization problems and rigorously transform them into equivalent solver-compatible forms in a semi-automatic fashion.
I'm also interested in the intersection of machine learning and symbolic methods, including neural network verification and neurosymbolic AI.
E-mail:
GitHub | Google Scholar | dblp | LinkedIn
Publications
Verified reductions for optimization
A. Bentkamp, R. Fernández Mir, J. Avigad
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol 13994, pp.74-92, 2023.
(publisher's website | arXiv | GitHub)
Machine-learned premise selection for Lean
B. Piotrowski, R. Fernández Mir, E. Ayers
International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Vol 14278, pp.175-186, 2023.
(publisher's website | arXiv | GitHub)
Conference on Artificial Intelligence and Theorem Proving (AITP), 2023.
(extended abstract)
Neurosymbolic AI for reasoning over knowledge graphs: a survey
L. N. DeLong, R. Fernández Mir, J. D. Fleuriot
Preprint, 2023.
(arXiv | GitHub)
Schemes in Lean
K. Buzzard, C. Hughes, K. Lau, A. Livingston, R. Fernández Mir, S. Morrison
Journal of Experimental Mathematics (ExpMath), Vol 31(2), pp.355-363, 2022.
(publisher's website | arXiv | GitHub)