In plain words: Checking that a neural network always behaves safely is usually treated as a math-speed problem, but this paper recasts those checks as programming-language problems, like proving ordinary code correct, and sketches language-based fixes. It argues such tools could matter more than faster checking algorithms alone.

Abstract · Neural Network Verification is a Programming Language Challenge

Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T. Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Šinkarovs, Haoze Wu
arXiv:2501.05867 · cs.PL, cs.LG, cs.LO · submitted Jan 10, 2025 · updated Jan 30, 2025
abstract · pdf · html · Accepted at ESOP 2025, European Symposium on Programming Languages