I work on the formal verification of AI systems as well, but focusing on model-based reasoning systems rather than the model-free ML systems. What you've described is exactly what terrifies me most about ML in safety…
Also, wouldn't the existence of a library function (#3) imply that what you're doing is either non-trivial or common enough that someone has already given the function a name? Seems like #1 is sufficient.
I work on the formal verification of AI systems as well, but focusing on model-based reasoning systems rather than the model-free ML systems. What you've described is exactly what terrifies me most about ML in safety…
Also, wouldn't the existence of a library function (#3) imply that what you're doing is either non-trivial or common enough that someone has already given the function a name? Seems like #1 is sufficient.