About me
Since June 2024, I work as a Formal Verification Engineer at Apple.
Previously, I was a PhD student at the University of Edinburgh, supervised by Dr Paul Jackson. I was part of the LFCS and the AIML. During my PhD, I worked on CvxLean, a verified convex optimization modeling framework written in Lean.
Before that, I obtained an MEng in Mathematics and Computer Science from Imperial College London and a Logic Year certificate from the ILLC.
My main interests are theorem proving and validated numerics.
E-mail:
GitHub | Google Scholar | dblp | LinkedIn
Theses
Verified transformations for convex programming
PhD thesis, University of Edinburgh, 2024
(PDF)
Schemes in Lean
MEng thesis, Imperial College London, 2019
(PDF)
Publications
Transforming optimization problems into Disciplined Convex Programming form
R. Fernández Mir, P. Jackson, S. Bhat, A. Goens, T. Grosser
International Conference on Intelligent Computer Mathematics (CICM), Vol 14960, pp.183-202, 2024.
(publisher's website)
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
IEEE Transactions on Neural Networks and Learning Systems (IEEE TNNLS), early access, pp.1-21, 2024.
(publisher's website | 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)