Neural Continuous-Time Supermartingale Certificates

This repository contains code for the paper Neural Continuous-Time Supermartingale Certificates by Grigory Neustroev, Mirco Giacobbe, Anna Lukina, published in AAAI 2025. To cite this work you can use:

@inproceedings{neustroev2025neural,
  title={Neural continuous-time supermartingale certificates},
  author={Neustroev, Grigory and Giacobbe, Mirco and Lukina, Anna},
  booktitle={Proceedings of the AAAI Conference on Artificial Intelligence},
  volume={39},
  number={26},
  pages={27538--27546},
  year={2025}
}

How to Install

In the paper, all experiments we run using Python 3.11.7 and the libraries from the requirements file. Please, download auto_LiRPA manually (we used v0.5.0, specifically commit bfb7997) and then either place in the auto_LiRPA subdirectory of this project, or install it yourself.

How to Use

Run the GBM and Inverted Pendulum scripts. The data will be saved to .csv files (copies are included in the results directory). The columns are: random seed, runtime, verification result, final epoch number.

Contributors

Greg Neustroev

Mirco Giacobbe

Anna Lukina