Louis Rustenholz

2024

1. Conference Paper

   An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants

   Louis Rustenholz, Pedro López-García, José F. Morales, and Manuel V. Hermenegildo

   In Proceedings of the 31st Static Analysis Symposium (SAS 2024) , Oct 2024

   Abs arXiv Bib PDF Code Slides

   Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours.

   @inproceedings{order-recsolv-sas24,
     author = {Rustenholz, Louis and López-García, Pedro and F.~Morales, José and V.~Hermenegildo, Manuel},
     title = {{A}n {O}rder {T}heory {F}ramework of {R}ecurrence {E}quations for {S}tatic {C}ost {A}nalysis – {D}ynamic {I}nference of {N}on-{L}inear {I}nequality {I}nvariants},
     booktitle = {Proceedings of the 31st Static Analysis Symposium (SAS 2024)},
     year = {2024},
     month = oct,
     publisher = {Springer},
     series = {LNCS},
     volume = {14995},
     paper_presentation_city = {Pasadena, CA},
     paper_presentation_country = {USA}
   }

2. Journal Article

   A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs

   Louis Rustenholz, Maximiliano Klemen, Miguel Ángel Carreira-Perpiñán, and Pedro López-García

   May 2024

   Accepted for publication in TPLP (preprint below).

   Abs arXiv Bib PDF

   Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and many for other languages), as CiaoPP, are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with state-of-the-art solvers, including Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning (sparse-linear and symbolic) regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check if it is actually a solution of the recurrence. Our prototype implementation and its experimental evaluation within the context of the CiaoPP system show quite promising results. Overall, for the considered benchmarks, our approach outperforms state-of-the-art cost analyzers and recurrence solvers, and solves recurrences that cannot be solved by them.

   @misc{mlrec-tplp2024-preprint,
     title = {{A} {M}achine {L}earning-based {A}pproach for {S}olving {R}ecurrence {R}elations and its use in {C}ost {A}nalysis of {L}ogic {P}rograms},
     author = {Rustenholz, Louis and Klemen, Maximiliano and Carreira-Perpiñán, Miguel Ángel and López-García, Pedro},
     year = {2024},
     month = may,
     eprint = {2405.06972},
     archiveprefix = {arXiv},
     primaryclass = {cs.PL},
     url = {https://arxiv.org/abs/2405.06972},
     note = {Accepted for publication in {TPLP} (preprint below).}
   }

2021

1. Conference Paper

   Static Analysis of ReLU Neural Networks with Tropical Polyhedra

   Eric Goubault, Sébastien Palumby, Sylvie Putot, Louis Rustenholz, and Sriram Sankaranarayanan

   In Proceedings of the 28th Static Analysis Symposium (SAS 2021) , Oct 2021

   Abs arXiv Bib PDF Video Video (2) Slides

   This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks. We report on a preliminary evaluation of our approach using a prototype implementation.

   @inproceedings{relunn-by-trop-sas21,
     author = {Goubault, Eric and Palumby, S{\'e}bastien and Putot, Sylvie and Rustenholz, Louis and Sankaranarayanan, Sriram},
     editor = {Dr{\u{a}}goi, Cezara and Mukherjee, Suvam and Namjoshi, Kedar},
     title = {Static Analysis of ReLU Neural Networks with Tropical Polyhedra},
     booktitle = {Proceedings of the 28th Static Analysis Symposium (SAS 2021)},
     year = {2021},
     month = oct,
     publisher = {Springer International Publishing},
     address = {Cham},
     pages = {166--190},
     isbn = {978-3-030-88806-0}
   }

2. Book

   L’équation aux S-unités – Voyage géométrique en théorie des nombres

   Khalil Bendriss, Paul Boisseau, Adam David, Félix Rebotier, and Louis Rustenholz

   Éditions Ellipses, Sep 2021

   Book version of a project on Geometrical and Algebraic Number Theory

   Preface by Diego Izquierdo

   Abs Bib HTML

   Le charme de l’arithmétique vient de la simplicité de ses énoncés jointe à la difficulté de ses preuves. L’équation aux S-unités consiste à trouver les solutions de l’égalité x + y = 1, où x et y sont des nombres entiers dont on a fixé les facteurs premiers. Combien de solutions a-t-elle ? Malgré son apparence élémentaire, cette question fait appel à plusieurs siècles de développement où se sont entrecroisés algèbre, géométrie et analyse. Ce sera finalement dans un article fondateur de 1996 que l’approche audacieuse des mathématiciens Beukers et Schlickewei permettra d’obtenir une réponse.
   
   Dans cet ouvrage, on se propose d’expliquer pas à pas cette fascinante démonstration pour permettre au plus grand nombre de s’approprier les idées qui l’animent. Au cours de cette élucidation, qui constitue le fil rouge du texte, le lecteur découvrira les notions clés qui ont jalonné l’histoire de l’étude des nombres, de Diophante à nos jours. Les outils et concepts fondamentaux de l’arithmétique seront exposés progressivement, avec des exemples qui serviront à les motiver. En plus d’introduire toutes les notions classiques, comme les anneaux de Dedekind, les corps p-adiques, ou encore la théorie des hauteurs, ce livre a vocation à présenter les grands mouvements qui ont forgé la théorie des nombres modernes. Il s’adresse donc à tous ceux, étudiants en troisième année de licence ou curieux de mathématiques, qui veulent découvrir cette discipline telle qu’elle se pratique de nos jours.

   @book{rustenholz-s-unites-ellipses,
     author = {Bendriss, Khalil and Boisseau, Paul and David, Adam and Rebotier, Félix and Rustenholz, Louis},
     editor = {{Éditions Ellipses}},
     title = {{L}’équation aux {S}-unités -- {V}oyage géométrique en théorie des nombres},
     year = {2021},
     month = sep,
     isbn = {9782340056701},
     note = {Book version of a project on Geometrical and Algebraic Number Theory},
     supervisornote = {Preface by Diego Izquierdo},
   }

1. M.S. Thesis

   Automated Approximate Recurrence Solving applied to Static Analysis of Energy Consumption

   Louis Rustenholz

   MPRI and École polytechnique (Master internship report), Aug 2022

   CLIP Lab, IMDEA Software Institute, Madrid, Spain

   Supervised by M.V. Hermenegildo, P. Lopez-Garcia, and J. F. Morales.

   PDF Slides
2. M.S. Thesis

   Categories and Preorders in Value Iteration: Fixed Points and Surrogate Models

   Louis Rustenholz

   École polytechnique (Master internship report), Aug 2021

   ERATO MMSD, National Institute of Informatics, Tokyo, Japan

   Supervised by Ichiro Hasuo and Jérémy Dubut.

   Best Research Internship PDF Slides

   Award for Best Research Internship (École polytechnique’s “Prix du Stage de Recherche”)

3. Internship

   Internship at OCamlPro

   Louis Rustenholz

   École polytechnique , Aug 2020

   Work for the SMT-solver Alt-Ergo. Web-based environment, tutorial, documentation.

   Supervised by Albin Coquereau.

   HTML
4. B.S. Thesis

   L’équation aux S-unités – Voyage géométrique en théorie des nombres

   Khalil Bendriss, Paul Boisseau, Adam David, Félix Rebotier, and Louis Rustenholz

   École polytechnique , Apr 2020

   Year 2 project at École polytechnique (PSC). Compiled in a book at Éditions Ellipses.

   Supervised by Diego Izquierdo.

   PDF Slides
5. Internship

   Internship at Direction Générale de l’Armement

   Louis Rustenholz

   École polytechnique , Apr 2019

   Design of chemico-physical models and simulations working towards a patent.
6. B.S. Thesis

   Neural networks: Expressivity and Implicit Spaces

   Louis Rustenholz

   Lycée Louis-le-Grand , Jun 2018

   Undergraduate research project (Classes Préparatoires, TIPE). Included here: ENS report (pdf) and Mines-Ponts slides.

   PDF Code Slides
7. Misc

   Jeu sur intervalle

   Louis Rustenholz with Cercle Mathématique de Strasbourg

   May 2016

   Paper for a high-school math research competition (TFJM²) – c.f. outreach page. Problems for the 2016 edition

   PDF
8. Misc

   Applying nanotechnology to medicine: the fight against cancer

   Nicolas Wendling, and Louis Rustenholz

   Jun 2014

   High-school research project (TPE). Website on DNA origami nanorobots.