diff --git a/docs/Project.toml b/docs/Project.toml index 1814eb3..639f676 100644 --- a/docs/Project.toml +++ b/docs/Project.toml @@ -1,5 +1,7 @@ [deps] Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4" +DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244" [compat] Documenter = "1" +DocumenterCitations = "1.3" diff --git a/docs/make.jl b/docs/make.jl index 19e616a..36ccfa5 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -1,18 +1,23 @@ -using Documenter, NeuralNetworkReachability +using Documenter, NeuralNetworkReachability, DocumenterCitations DocMeta.setdocmeta!(NeuralNetworkReachability, :DocTestSetup, :(using NeuralNetworkReachability); recursive=true) +bib = CitationBibliography(joinpath(@__DIR__, "src", "refs.bib"); style=:alpha) + makedocs(; sitename="NeuralNetworkReachability.jl", modules=[NeuralNetworkReachability], format=Documenter.HTML(; prettyurls=get(ENV, "CI", nothing) == "true", - collapselevel=1, assets=["assets/aligned.css"]), + collapselevel=1, + assets=["assets/aligned.css", "assets/citations.css"]), pagesonly=true, + plugins=[bib], pages=["Home" => "index.md", "Library" => Any["ForwardAlgorithms" => "lib/ForwardAlgorithms.md", "BackwardAlgorithms" => "lib/BackwardAlgorithms.md", "BidirectionalAlgorithms" => "lib/BidirectionalAlgorithms.md", "Util" => "lib/Util.md"], + "Bibliography" => "bibliography.md", "About" => "about.md"]) deploydocs(; repo="github.com/JuliaReach/NeuralNetworkReachability.jl.git", diff --git a/docs/src/assets/citations.css b/docs/src/assets/citations.css new file mode 100644 index 0000000..b0c6326 --- /dev/null +++ b/docs/src/assets/citations.css @@ -0,0 +1,17 @@ +.citation dl { + display: grid; + grid-template-columns: max-content auto; } +.citation dt { + grid-column-start: 1; } +.citation dd { + grid-column-start: 2; + margin-bottom: 0.75em; } +.citation ul { + padding: 0 0 2.25em 0; + margin: 0; + list-style: none !important;} +.citation ul li { + text-indent: -2.25em; + margin: 0.33em 0.5em 0.5em 2.25em;} +.citation ol li { + padding-left:0.75em;} diff --git a/docs/src/bibliography.md b/docs/src/bibliography.md new file mode 100644 index 0000000..a987675 --- /dev/null +++ b/docs/src/bibliography.md @@ -0,0 +1,4 @@ +# Bibliography + +```@bibliography +``` diff --git a/docs/src/refs.bib b/docs/src/refs.bib new file mode 100644 index 0000000..d75a115 --- /dev/null +++ b/docs/src/refs.bib @@ -0,0 +1,77 @@ + +@inproceedings{GehrMDTCV18, + author = {Timon Gehr and + Matthew Mirman and + Dana Drachsler{-}Cohen and + Petar Tsankov and + Swarat Chaudhuri and + Martin T. Vechev}, + title = {{AI2:} Safety and Robustness Certification of Neural Networks with + Abstract Interpretation}, + booktitle = {2018 {IEEE} Symposium on Security and Privacy, {SP} 2018, Proceedings, + 21-23 May 2018, San Francisco, California, {USA}}, + pages = {3--18}, + publisher = {{IEEE} Computer Society}, + year = {2018}, + url = {https://doi.org/10.1109/SP.2018.00058}, + doi = {10.1109/SP.2018.00058}, + timestamp = {Fri, 24 Mar 2023 00:03:11 +0100}, + biburl = {https://dblp.org/rec/conf/sp/GehrMDTCV18.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{SinghGMPV18, + author = {Gagandeep Singh and + Timon Gehr and + Matthew Mirman and + Markus P{\"{u}}schel and + Martin T. Vechev}, + editor = {Samy Bengio and + Hanna M. Wallach and + Hugo Larochelle and + Kristen Grauman and + Nicol{\`{o}} Cesa{-}Bianchi and + Roman Garnett}, + title = {Fast and Effective Robustness Certification}, + booktitle = {Advances in Neural Information Processing Systems ({NeurIPS})}, + pages = {10825--10836}, + year = {2018}, + url = {https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-Abstract.html} +} + +@inproceedings{IvanovWAPL19, + author = {Radoslav Ivanov and + James Weimer and + Rajeev Alur and + George J. Pappas and + Insup Lee}, + editor = {Necmiye Ozay and + Pavithra Prabhakar}, + title = {Verisig: verifying safety properties of hybrid systems with neural + network controllers}, + booktitle = {Hybrid Systems: Computation and Control ({HSCC})}, + pages = {169--178}, + publisher = {{ACM}}, + year = {2019}, + url = {https://doi.org/10.1145/3302504.3311806}, + doi = {10.1145/3302504.3311806} +} + +@inproceedings{Kochdumper0AB23, + author = {Niklas Kochdumper and + Christian Schilling and + Matthias Althoff and + Stanley Bak}, + editor = {Kristin Yvonne Rozier and + Swarat Chaudhuri}, + title = {Open- and Closed-Loop Neural Network Verification Using Polynomial + Zonotopes}, + booktitle = {{NASA} Formal Methods ({NFM})}, + series = {LNCS}, + volume = {13903}, + pages = {16--36}, + publisher = {Springer}, + year = {2023}, + url = {https://doi.org/10.1007/978-3-031-33170-1_2}, + doi = {10.1007/978-3-031-33170-1_2} +} diff --git a/src/ForwardAlgorithms/AI2.jl b/src/ForwardAlgorithms/AI2.jl index 931d3d3..adbc60e 100644 --- a/src/ForwardAlgorithms/AI2.jl +++ b/src/ForwardAlgorithms/AI2.jl @@ -2,15 +2,12 @@ AI2Box <: AI2 AI2 forward algorithm for ReLU activation functions based on abstract -interpretation with the interval domain from [1]. +interpretation with the interval domain from [GehrMDTCV18](@citet). ### Notes This algorithm is less precise than [`BoxForward`](@ref) because it abstracts after every step, including the affine map. - -[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks -with abstract interpretation*, SP 2018. """ struct AI2Box <: ForwardAlgorithm end @@ -18,15 +15,12 @@ struct AI2Box <: ForwardAlgorithm end AI2Zonotope <: AI2 AI2 forward algorithm for ReLU activation functions based on abstract -interpretation with the zonotope domain from [1]. +interpretation with the zonotope domain from [GehrMDTCV18](@citet). ### Fields - `join_algorithm` -- (optional; default: `"join"`) algorithm to compute the join of two zonotopes - -[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks -with abstract interpretation*, SP 2018. """ struct AI2Zonotope{S} <: ForwardAlgorithm join_algorithm::S @@ -39,10 +33,7 @@ AI2Zonotope() = AI2Zonotope("join") AI2Polytope <: AI2 AI2 forward algorithm for ReLU activation functions based on abstract -interpretation with the polytope domain from [1]. - -[1]: Gehr et al.: *AI²: Safety and robustness certification of neural networks -with abstract interpretation*, SP 2018. +interpretation with the polytope domain from [GehrMDTCV18](@citet). """ struct AI2Polytope <: ForwardAlgorithm end diff --git a/src/ForwardAlgorithms/DeepZ.jl b/src/ForwardAlgorithms/DeepZ.jl index 6ef48b1..61f5f42 100644 --- a/src/ForwardAlgorithms/DeepZ.jl +++ b/src/ForwardAlgorithms/DeepZ.jl @@ -2,9 +2,7 @@ DeepZ <: ForwardAlgorithm Forward algorithm based on zonotopes for ReLU, sigmoid, and tanh activation -functions from [1]. - -[1]: Singh et al.: *Fast and Effective Robustness Certification*, NeurIPS 2018. +functions from [SinghGMPV18](@citet). """ struct DeepZ <: ForwardAlgorithm end diff --git a/src/ForwardAlgorithms/PolyZonoForward.jl b/src/ForwardAlgorithms/PolyZonoForward.jl index 29ee14c..3fdab20 100644 --- a/src/ForwardAlgorithms/PolyZonoForward.jl +++ b/src/ForwardAlgorithms/PolyZonoForward.jl @@ -34,7 +34,7 @@ struct TaylorExpansionQuadratic <: QuadraticApproximation end PolyZonoForward{A<:PolynomialApproximation,N,R} <: ForwardAlgorithm Forward algorithm based on poynomial zonotopes via polynomial approximation from -[1]. +[Kochdumper0AB23](@citet). ### Fields @@ -54,9 +54,6 @@ The default constructor takes keyword arguments with the following defaults: See the subtypes of `PolynomialApproximation` for available polynomial approximation methods. - -[1]: Kochdumper et al.: *Open- and closed-loop neural network verification using -polynomial zonotopes*, NFM 2023. """ struct PolyZonoForward{A<:PolynomialApproximation,O,R} <: ForwardAlgorithm polynomial_approximation::A diff --git a/src/ForwardAlgorithms/Verisig.jl b/src/ForwardAlgorithms/Verisig.jl index 36d2d03..c44d4c7 100644 --- a/src/ForwardAlgorithms/Verisig.jl +++ b/src/ForwardAlgorithms/Verisig.jl @@ -1,7 +1,7 @@ """ Verisig{R} <: ForwardAlgorithm -Forward algorithm for sigmoid and tanh activation functions from [1]. +Forward algorithm for sigmoid and tanh activation functions from [IvanovWAPL19](@citet). ### Fields @@ -13,9 +13,6 @@ The implementation is known to be unsound in some cases. The implementation currently only supports neural networks with a single hidden layer. - -[1] Ivanov et al.: *Verisig: verifying safety properties of hybrid systems with -neural network controllers*, HSCC 2019. """ struct Verisig{R} <: ForwardAlgorithm algo::R