Ramon Fernández Mir

RFM

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)

Selected talks

01/24 CvxLean: tool overview (slides | video) Lean Together 2024
04/23 Verified reductions for optimization (slides) TACAS 2023
03/23 ML-based premise selection for Lean (slides) AIML seminar
09/22 Verified optimization for hybrid systems (slides) CICM 2022
05/22 Connecting Lean to a convex solver (demo) CMU-Pitt seminar
06/19 Schemes in Lean (slides) ICL thesis defense
09/18 Verification of data layout transformations (slides) Inria-Paris seminar

Teaching assistantships

2022-23 Algorithms and data structures, Introduction to computation
2021-22 Formal verification, Introduction to computation
2020-21 Reasoning and agents, Algorithms and data structures
2018-19 Logic, Reasoning about programs
2017-18 Logic, Reasoning about programs