Blueprint Bibliography🔗

Bibliography (70)

• Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala, 2019. “PyTorch: An Imperative Style, High-Performance Deep Learning Library”. arXiv:1912.01703
  Cited from (51)

  • Chapter 2: Building Models, Section 2.2: Models
  • Chapter 2: Building Models, Section 2.3: Sample Shapes In Memory
  • Chapter 2: Building Models, Section 2.3: Tensor minibatches
  • Chapter 2: Building Models, Section 2.1: Tensors
  • Chapter 2: Building Models, Section 2.1: Arithmetic On Tensors
  • Chapter 2: Building Models, Section 2.1: Linear Layers And Prefix Dimensions
  • Chapter 2: Building Models, Section 2.5: TorchLean API
  • Chapter 7: Examples and Applications, Section 7.6: BugZoo Catalog
  • Chapter 7: Examples and Applications, Section 7.3: The Noise Schedule
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
  • Chapter 7: Examples and Applications, Section 7.1: Modern Models
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 7: Examples and Applications, Section 7.4: Actor And Critic Batch Shapes
  • Chapter 7: Examples and Applications, Section 7.2: Parameter Layout
  • Chapter 7: Examples and Applications, Section 7.9: Theorem Hypotheses
  • Chapter 7: Examples and Applications, Section 7.5: Autograd (Tape + Gradients)
  • Chapter 7: Examples and Applications, Section 7.5: Autograd (Tape + Gradients)
  • Chapter 7: Examples and Applications, Section 7.7: Rank, Slices, And The Reshape Guard
  • Chapter 5: Floating Point and Native Boundaries, Section 5.4: PyTorch Graph Capture
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Linear Layer Error Bounds
  • Chapter 5: Floating Point and Native Boundaries, Section 5.1: Tensors, Reductions, And Quantization
  • Chapter 5: Floating Point and Native Boundaries, Section 5.3: Hard Attention Masks
  • Chapter 1: Introduction, Section 1.3: Command Help And Further Reading
  • Chapter 1: Introduction, Section 1.7: PyTorch State Dictionaries
  • Chapter 1: Introduction, Section 1.5: Imports And Namespaces
  • Chapter 1: Introduction, Section 1.1: Model Definition And Initialization
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.6: Autograd Implementations And Specifications
  • Chapter 1: Introduction, Section 1.6: References
  • Chapter 1: Introduction, Section 1.4: Functional Programming
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Train And Evaluation Mode
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: Gradient Return Values And Accumulation
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.6: PyTorch Interop
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.6: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: PyTorch Gradient Accumulation
  • Chapter 4: Semantics and Graphs, Section 4.2: Shape Mismatch In PyTorch
  • Chapter 4: Semantics and Graphs, Section 4.1: Tensors
  • Chapter 6: Verification and Certificates, Section 6.8: ReLU Approximation In PyTorch
  • Chapter 6: Verification and Certificates, Section 6.3: Autograd Proofs
  • Chapter 6: Verification and Certificates, Section 6.5: Sampling And Privacy Guarantees
  • Chapter 6: Verification and Certificates, Section 6.12: Cholesky In PyTorch
  • Chapter 6: Verification and Certificates, Section 6.6: Scalar Optimizer Comparison
  • Chapter 6: Verification and Certificates, Section 6.10: Gaussian Noising In PyTorch
  • Chapter 6: Verification and Certificates, Section 6.10: MLP Derivative Composition
  • Chapter 6: Verification and Certificates, Section 6.2: Value-Table Preservation
  • Chapter 6: Verification and Certificates, Section 6.4: Comparison With PyTorch Tolerances
  • Chapter 6: Verification and Certificates, Section 6.11: PDE Residuals In PyTorch
  • Chapter 6: Verification and Certificates, Section 6.7: MAE Loss In PyTorch
• Adrien Bardes, Jean Ponce, and Yann LeCun, 2022. “VICReg: Variance-Invariance-Covariance Regularization for Self-Supervised Learning”. arXiv:2105.04906
  Cited from (2)

  • Chapter 6: Verification and Certificates, Section 6.7: Pairwise Spread And Variance
  • Chapter 6: Verification and Certificates, Section 6.7: Proof And Runtime Boundary
• Albert Gu, Karan Goel, and Christopher Ré, 2022. “Efficiently Modeling Long Sequences with Structured State Spaces”. In International Conference on Learning Representations (ICLR).
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.9: Causality In State-Space Models
• Albert Gu and Tri Dao, 2024. “Mamba: Linear-Time Sequence Modeling with Selective State Spaces”. arXiv:2312.00752
  Cited from (4)

  • Chapter 2: Building Models, Section 2.2: Model Family Constructors
  • Chapter 7: Examples and Applications, Section 7.1: State-Space Models
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 6: Verification and Certificates, Section 6.9: Causality In State-Space Models
• Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby, 2021. “An Image Is Worth 16x16 Words: Transformers for Image Recognition at Scale”. arXiv:2010.11929
  Cited from (5)

  • Chapter 2: Building Models, Section 2.2: Model Family Constructors
  • Chapter 7: Examples and Applications, Section 7.1: Vision Transformers
  • Chapter 7: Examples and Applications, Section 7.1: Permuting Keys, Values, And Queries
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 7: Examples and Applications, Section 7.2: ResNet And ViT On CIFAR
• Andreas Griewank and Andrea Walther (2000). “Algorithm 799: Revolve. An Implementation of Checkpointing for the Reverse or Adjoint Mode of Computational Differentiation”. ACM Transactions on Mathematical Software. 26(1), pp. 19–45.
  Cited from (2)

  • Chapter 1: Introduction, Section 1.7: Checking The Gradient Against A Difference Quotient
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Checkpoint Wrapper Semantics
• Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Łukasz Kaiser, and Illia Polosukhin, 2017. “Attention Is All You Need”. arXiv:1706.03762
  Cited from (16)

  • Chapter 2: Building Models, Section 2.2: Models
  • Chapter 2: Building Models, Section 2.2: PyTorch Transformer Parameter Comparison
  • Chapter 2: Building Models, Section 2.3: Next-Token Datasets
  • Chapter 2: Building Models, Section 2.1: Tensor Type
  • Chapter 2: Building Models, Section 2.4: Learning-rate schedules
  • Chapter 7: Examples and Applications, Section 7.6: BugZoo Catalog
  • Chapter 7: Examples and Applications, Section 7.1: Causal Masks
  • Chapter 7: Examples and Applications, Section 7.1: Permuting Keys, Values, And Queries
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 7: Examples and Applications, Section 7.2: Parameter Layout
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: Boolean Attention Masks
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.6: Transformer (Encoder)
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.6: References
  • Chapter 4: Semantics and Graphs, Section 4.1: Attention masks
  • Chapter 6: Verification and Certificates, Section 6.3: Model Coverage: Attention, Transformers, And Recurrent Cells
  • Chapter 6: Verification and Certificates, Section 6.4: Normalization And Attention
• Atılım Güneş Baydin, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind (2018). “Automatic Differentiation in Machine Learning: a Survey”. Journal of Machine Learning Research. 18(153), pp. 1–43.
  Cited from (16)

  • Chapter 2: Building Models, Section 2.5: Explicit Differentiation
  • Chapter 7: Examples and Applications, Section 7.7: Function And Model Differentiation
  • Chapter 5: Floating Point and Native Boundaries, Section 5.2: Backward Error Propagation
  • Chapter 1: Introduction, Section 1.7: Training Step
  • Chapter 1: Introduction, Section 1.6: References
  • Chapter 1: Introduction, Section 1.6: Autograd Implementations And Specifications
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Graph Lowering And Direct Execution
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Vegetation Attenuation Model
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: Vector-Jacobian Products
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: Forward And Backward Ownership
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Gradient Accumulation On The Tape
  • Chapter 6: Verification and Certificates, Section 6.3: Autograd Proofs
  • Chapter 6: Verification and Certificates, Section 6.10: Vector-Jacobian Products
  • Chapter 6: Verification and Certificates, Section 6.11: PDE Residuals In PyTorch
• Augustus Odena, Catherine Olsson, David G. Andersen, and Ian Goodfellow, 2019. “TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing”. In International Conference on Machine Learning (ICML).
  Cited from (4)

  • Chapter 7: Examples and Applications, Section 7.6: BugZoo Catalog
  • Chapter 7: Examples and Applications, Section 7.9: Operation Development
  • Chapter 5: Floating Point and Native Boundaries, Section 5.4: Semantic Guarantees For Imported Graphs
  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
• Aäron van den Oord, Oriol Vinyals, and Koray Kavukcuoglu, 2017. “Neural Discrete Representation Learning”. arXiv:1711.00937
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.3: Discrete Codes
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
• Barak A. Pearlmutter and Jeffrey Mark Siskind (2008). “Reverse-Mode AD in a Functional Framework: Lambda the Ultimate Backpropagator”. ACM Transactions on Programming Languages and Systems. 30(2).
  Cited from (3)

  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: Local Rules And The Global Reverse Pass
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: JVPs And Hessian-Vector Products
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Model Mode And Random State
• Boris T. Polyak (1964). “Some Methods of Speeding Up the Convergence of Iteration Methods”. USSR Computational Mathematics and Mathematical Physics. 4(5), pp. 1–17.
  Cited from (7)

  • Chapter 2: Building Models, Section 2.5: Persistent And Per-Call Configuration
  • Chapter 2: Building Models, Section 2.4: Adam Moments And Step Counter
  • Chapter 7: Examples and Applications, Section 7.4: Target Networks
  • Chapter 1: Introduction, Section 1.6: Momentum SGD
  • Chapter 1: Introduction, Section 1.4: Functional Programming
  • Chapter 1: Introduction, Section 1.4: Optimizer State Transitions
  • Chapter 1: Introduction, Section 1.4: References
• Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko, 2021. “MLIR: Scaling Compiler Infrastructure for the End of Moore's Law”. In Code Generation and Optimization (CGO).
  Cited from (1)

  • Chapter 4: Semantics and Graphs, Section 4.3: The Node Record
• Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus, 2014. “Intriguing Properties of Neural Networks”. arXiv:1312.6199
  Cited from (4)

  • Chapter 1: Introduction, Section 1.2: Motivation
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 6: Verification and Certificates, Section 6.5: Robustness Specifications And Runtime Checks
  • Chapter 6: Verification and Certificates, Section 6.1: Neural Network Verification
• Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith, 2006. “Calibrating Noise to Sensitivity in Private Data Analysis”. In Theory of Cryptography (TCC).
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.5: Postprocessing
• David Goldberg (1991). “What Every Computer Scientist Should Know About Floating-Point Arithmetic”. ACM Computing Surveys. 23(1), pp. 5–48.
  Cited from (31)

  • Chapter 2: Building Models, Section 2.3: CSV, NPY, And PyTorch Data Comparison
  • Chapter 2: Building Models, Section 2.1: Arithmetic On Tensors
  • Chapter 7: Examples and Applications, Section 7.6: Float Boundary
  • Chapter 7: Examples and Applications, Section 7.8: CPU And CUDA Builds
  • Chapter 7: Examples and Applications, Section 7.4: Checked Arithmetic For Returns And Ratios
  • Chapter 7: Examples and Applications, Section 7.9: Printed Precision
  • Chapter 7: Examples and Applications, Section 7.9: Numerical Guarantees
  • Chapter 7: Examples and Applications, Section 7.5: Tensor Viewer
  • Chapter 7: Examples and Applications, Section 7.7: Tensor Shapes And Scalar Types
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Rounded Reals And Executable Formats
  • Chapter 5: Floating Point and Native Boundaries, Section 5.1: Nonassociative Binary32 Addition
  • Chapter 5: Floating Point and Native Boundaries, Section 5.3: Reduction Order In The Numerical Contract
  • Chapter 5: Floating Point and Native Boundaries, Section 5.2: Numerical Error
  • Chapter 1: Introduction, Section 1.3: Tensors
  • Chapter 1: Introduction, Section 1.1: Fused Multiply-Add
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.4: Floating-Point Equality
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Native CUDA Execution
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Executable Binary32 Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Floating-Point Transcendentals
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: PyTorch Gradients
  • Chapter 4: Semantics and Graphs, Section 4.3: Scalar Interpretations
  • Chapter 4: Semantics and Graphs, Section 4.1: Runtime And Specification Comparison
  • Chapter 6: Verification and Certificates, Section 6.8: Rounding Error
  • Chapter 6: Verification and Certificates, Section 6.5: Ridge Regression In Binary32
  • Chapter 6: Verification and Certificates, Section 6.12: Dot Products And Norms
  • Chapter 6: Verification and Certificates, Section 6.10: ReLU Backward Values At Zero
  • Chapter 6: Verification and Certificates, Section 6.4: Real And Floating-Point Semantics
  • Chapter 6: Verification and Certificates, Section 6.4: Error Bounds For Reductions And Softmax
• Diederik P. Kingma and Jimmy Ba, 2015. “Adam: A Method for Stochastic Optimization”. In International Conference on Learning Representations (ICLR).
  Cited from (3)

  • Chapter 2: Building Models, Section 2.4: Objective And Optimizer Configuration
  • Chapter 2: Building Models, Section 2.4: Adam Moments And Step Counter
  • Chapter 1: Introduction, Section 1.6: Adam's Epsilon
• Diederik P. Kingma and Max Welling, 2014. “Auto-Encoding Variational Bayes”. arXiv:1312.6114
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.3: The VAE Objective
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
• Edward J. Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Lu Wang, and Weizhu Chen, 2022. “LoRA: Low-Rank Adaptation of Large Language Models”. arXiv:2106.09685
  Cited from (1)

  • Chapter 2: Building Models, Section 2.2: Low-Rank Linear Adapters
• Eric Wong and J. Zico Kolter, 2018. “Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope”. arXiv:1711.00851
  Cited from (4)

  • Chapter 1: Introduction, Section 1.1: Output Properties
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 6: Verification and Certificates, Section 6.5: Runtime Margin Reports
  • Chapter 6: Verification and Certificates, Section 6.1: CROWN, Alpha-CROWN, And Alpha-Beta-CROWN
• George C. Necula, 1997. “Proof-Carrying Code”. In Principles of Programming Languages (POPL).
  Cited from (15)

  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 7: Examples and Applications, Section 7.4: Checker Soundness
  • Chapter 7: Examples and Applications, Section 7.9: Theorem Hypotheses
  • Chapter 7: Examples and Applications, Section 7.9: Scientific ML
  • Chapter 7: Examples and Applications, Section 7.7: Numerical Certificate Replay
  • Chapter 5: Floating Point and Native Boundaries, Section 5.4: The Parser's Structural Guarantee
  • Chapter 1: Introduction, Section 1.1: Output Properties
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: Capsule Contracts And Evidence
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: References
  • Chapter 4: Semantics and Graphs, Section 4.3: Executable Coverage And Proof Coverage
  • Chapter 6: Verification and Certificates, Section 6.1: Executable Certificates And Imported Artifacts
  • Chapter 6: Verification and Certificates, Section 6.2: Proof Obligations As Relations
  • Chapter 6: Verification and Certificates, Section 6.14: Two-Stage Verification
  • Chapter 6: Verification and Certificates, Section 6.13: Verification Certificates
• George Cybenko (1989). “Approximation by Superpositions of a Sigmoidal Function”. Mathematics of Control, Signals and Systems. 2(4), pp. 303–314.
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.8: Approximation And Enclosure Guarantees
• Grigore Roșu (2017). “Matching Logic”. Logical Methods in Computer Science. 13(4).
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
• Grigore Roșu and Traian Florin Șerbănuță (2010). “An Overview of the K Semantic Framework”. Journal of Logic and Algebraic Programming. 79(6), pp. 397–434.
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
• Herbert Robbins and Sutton Monro (1951). “A Stochastic Approximation Method”. The Annals of Mathematical Statistics. 22(3), pp. 400–407.
  Cited from (2)

  • Chapter 2: Building Models, Section 2.4: Objective And Optimizer Configuration
  • Chapter 2: Building Models, Section 2.4: Gradient Descent Updates
• Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel, 2018. “Efficient Neural Network Robustness Certification with General Activation Functions”. arXiv:1811.00866
  Cited from (15)

  • Chapter 7: Examples and Applications, Section 7.5: Verification (IBP/CROWN State)
  • Chapter 7: Examples and Applications, Section 7.5: Interval Dependency
  • Chapter 7: Examples and Applications, Section 7.7: IBP Workflow
  • Chapter 1: Introduction, Section 1.7: Output Width And Input Radius
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.1: Output Properties
  • Chapter 1: Introduction, Section 1.2: Real-Valued Enclosure Proof
  • Chapter 1: Introduction, Section 1.2: Dependency Loss And Affine Relaxations
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 4: Semantics and Graphs, Section 4.3: Interval Bound Propagation
  • Chapter 6: Verification and Certificates, Section 6.1: IBP On A Two-Layer Affine Network
  • Chapter 6: Verification and Certificates, Section 6.1: CROWN, Alpha-CROWN, And Alpha-Beta-CROWN
  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
  • Chapter 6: Verification and Certificates, Section 6.14: Neural Controllers
  • Chapter 6: Verification and Certificates, Section 6.13: Loss Of Correlation In Interval Bounds
• Hubert Ramsauer, Bernhard Schäfl, Johannes Lehner, Philipp Seidl, Michael Widrich, Thomas Adler, Lukas Gruber, Markus Holzleitner, Milena Pavlović, Geir Kjetil Sandve, Victor Greiff, David Kreil, Michael Kopp, Günter Klambauer, Johannes Brandstetter, and Sepp Hochreiter, 2021. “Hopfield Networks is All You Need”. In International Conference on Learning Representations (ICLR).
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.9: Energy Ties And Convergence
• Ilya Loshchilov and Frank Hutter, 2017. “SGDR: Stochastic Gradient Descent with Warm Restarts”. arXiv:1608.03983
  Cited from (1)

  • Chapter 2: Building Models, Section 2.4: Learning-rate schedules
• Ilya Loshchilov and Frank Hutter, 2019. “Decoupled Weight Decay Regularization”. arXiv:1711.05101
  Cited from (10)

  • Chapter 2: Building Models, Section 2.5: Persistent And Per-Call Configuration
  • Chapter 2: Building Models, Section 2.4: Adam Moments And Step Counter
  • Chapter 7: Examples and Applications, Section 7.2: Changing Width, Heads, And Context
  • Chapter 5: Floating Point and Native Boundaries, Section 5.2: Optimizer Arithmetic
  • Chapter 1: Introduction, Section 1.3: Trainer Configuration
  • Chapter 1: Introduction, Section 1.7: Training Step
  • Chapter 1: Introduction, Section 1.4: Optimizer State Transitions
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 6: Verification and Certificates, Section 6.6: Scalar Optimizer Comparison
  • Chapter 6: Verification and Certificates, Section 6.4: Rounded Optimizer Steps
• James K. Reed, Zachary DeVito, Horace He, Ansley Ussery, and Jason Ansel, 2022. “torch.fx: Practical Program Capture and Transformation for Deep Learning in Python”. In Machine Learning and Systems (MLSys).
  Cited from (2)

  • Chapter 2: Building Models, Section 2.5: Functional Tensor Operations
  • Chapter 4: Semantics and Graphs, Section 4.3: PyTorch Graph Capture
• Jiaming Song, Chenlin Meng, and Stefano Ermon, 2021. “Denoising Diffusion Implicit Models”. arXiv:2010.02502
  Cited from (3)

  • Chapter 7: Examples and Applications, Section 7.3: Reverse Sampling
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
  • Chapter 6: Verification and Certificates, Section 6.10: Forward Diffusion Kernels
• Jiawei Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, and Lingming Zhang, 2023. “NNSmith: Generating Diverse and Valid Test Cases for Deep Learning Compilers”. arXiv:2207.13066
  Cited from (6)

  • Chapter 2: Building Models, Section 2.1: Shape Guarantees
  • Chapter 7: Examples and Applications, Section 7.6: BugZoo Catalog
  • Chapter 7: Examples and Applications, Section 7.9: Operation Development
  • Chapter 5: Floating Point and Native Boundaries, Section 5.4: Semantic Guarantees For Imported Graphs
  • Chapter 6: Verification and Certificates, Section 6.2: Proof Systems
  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
• John J. Hopfield (1982). “Neural Networks and Physical Systems with Emergent Collective Computational Abilities”. Proceedings of the National Academy of Sciences. 79(8), pp. 2554–2558.
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.9: Hopfield Dynamics
• John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov, 2017. “Proximal Policy Optimization Algorithms”. arXiv:1707.06347
  Cited from (3)

  • Chapter 7: Examples and Applications, Section 7.4: Reinforcement Learning
  • Chapter 7: Examples and Applications, Section 7.4: Rollout Data
  • Chapter 7: Examples and Applications, Section 7.4: The PPO Objective
• John Schulman, Philipp Moritz, Sergey Levine, Michael I. Jordan, and Pieter Abbeel, 2015. “High-Dimensional Continuous Control Using Generalized Advantage Estimation”. arXiv:1506.02438
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.4: Reinforcement Learning
  • Chapter 7: Examples and Applications, Section 7.4: Returns And Generalized Advantage Estimation
• Jonathan Ho, Ajay Jain, and Pieter Abbeel, 2020. “Denoising Diffusion Probabilistic Models”. arXiv:2006.11239
  Cited from (4)

  • Chapter 7: Examples and Applications, Section 7.3: Forward Noising
  • Chapter 7: Examples and Applications, Section 7.3: Diffusion Training And Sampling
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
  • Chapter 6: Verification and Certificates, Section 6.10: Forward Diffusion Kernels
• Jure Zbontar, Li Jing, Ishan Misra, Yann LeCun, and Stéphane Deny, 2021. “Barlow Twins: Self-Supervised Learning via Redundancy Reduction”. arXiv:2103.03230
  Cited from (2)

  • Chapter 6: Verification and Certificates, Section 6.7: Discrete VICReg Model
  • Chapter 6: Verification and Certificates, Section 6.7: Proof And Runtime Boundary
• Jérôme Bolte and Edouard Pauwels, 2020. “A Mathematical Model for Automatic Differentiation in Machine Learning”. In Neural Information Processing Systems (NeurIPS).
  Cited from (2)

  • Chapter 1: Introduction, Section 1.7: Crossing An Activation Boundary
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: ReLU Derivatives At Zero
• Kai Jia and Martin Rinard, 2020. “Exploiting Verified Neural Networks via Floating Point Numerical Error”. arXiv:2003.03021
  Cited from (3)

  • Chapter 7: Examples and Applications, Section 7.6: Float Boundary
  • Chapter 1: Introduction, Section 1.2: Native And Reference IEEE Bounds
  • Chapter 1: Introduction, Section 1.2: References
• Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh, 2020. “Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond”. arXiv:2002.12920
  Cited from (12)

  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 7: Examples and Applications, Section 7.7: IBP Workflow
  • Chapter 1: Introduction, Section 1.7: Output Width And Input Radius
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.1: Output Properties
  • Chapter 1: Introduction, Section 1.2: Real-Valued Enclosure Proof
  • Chapter 1: Introduction, Section 1.2: Dependency Loss And Affine Relaxations
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 6: Verification and Certificates, Section 6.1: Bound Propagation With auto_LiRPA
  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
  • Chapter 6: Verification and Certificates, Section 6.14: Neural Controllers
  • Chapter 6: Verification and Certificates, Section 6.13: Bound Computation And Pruning In Python
• Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun, 2015. “Delving Deep into Rectifiers: Surpassing Human-Level Performance on ImageNet Classification”. In International Conference on Computer Vision (ICCV).
  Cited from (1)

  • Chapter 2: Building Models, Section 2.4: Initial Parameter Values
• Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun, 2016. “Deep Residual Learning for Image Recognition”. arXiv:1512.03385
  Cited from (6)

  • Chapter 2: Building Models, Section 2.2: CIFAR-10 Training Example
  • Chapter 2: Building Models, Section 2.1: Tensor Type
  • Chapter 7: Examples and Applications, Section 7.1: Residual Networks
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 7: Examples and Applications, Section 7.2: ResNet And ViT On CIFAR
  • Chapter 4: Semantics and Graphs, Section 4.2: DAG Syntax And Shared Computations
• Kaiming He, Xinlei Chen, Saining Xie, Yanghao Li, Piotr Dollár, and Ross Girshick, 2022. “Masked Autoencoders Are Scalable Vision Learners”. arXiv:2111.06377
  Cited from (6)

  • Chapter 2: Building Models, Section 2.2: Masked Inputs And Reconstruction Targets
  • Chapter 7: Examples and Applications, Section 7.3: Masked Autoencoding
  • Chapter 7: Examples and Applications, Section 7.3: Masked Autoencoding
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
  • Chapter 6: Verification and Certificates, Section 6.7: MAE Loss In PyTorch
  • Chapter 6: Verification and Certificates, Section 6.7: Proof And Runtime Boundary
• Kurt Hornik (1991). “Approximation Capabilities of Multilayer Feedforward Networks”. Neural Networks. 4(2), pp. 251–257.
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.8: Approximation And Enclosure Guarantees
• Leonardo de Moura and Sebastian Ullrich, 2021. “The Lean 4 Theorem Prover and Programming Language”. In Automated Deduction (CADE 28).
  Cited from (5)

  • Chapter 2: Building Models, Section 2.3: Sample Shapes In Memory
  • Chapter 2: Building Models, Section 2.1: Checked Shape Patterns
  • Chapter 2: Building Models, Section 2.5: TorchLean API
  • Chapter 1: Introduction, Section 1.5: Lean Basics
  • Chapter 1: Introduction, Section 1.5: Further Reading
• Mahmoud Assran, Quentin Duval, Ishan Misra, Piotr Bojanowski, Pascal Vincent, Michael Rabbat, Yann LeCun, and Nicolas Ballas, 2023. “Self-Supervised Learning from Images with a Joint-Embedding Predictive Architecture”. arXiv:2301.08243
  Cited from (2)

  • Chapter 6: Verification and Certificates, Section 6.7: JEPA Target Representations
  • Chapter 6: Verification and Certificates, Section 6.7: Proof And Runtime Boundary
• Maziar Raissi, Paris Perdikaris, and George Em Karniadakis (2019). “Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations”. Journal of Computational Physics. 378, pp. 686–707.
  Cited from (5)

  • Chapter 2: Building Models, Section 2.3: Generated Streams
  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: PINN Residuals
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 6: Verification and Certificates, Section 6.11: Uniform Residual And Boundary Bounds
• Nick Benton, Chung-Kil Hur, Andrew J. Kennedy, and Conor McBride (2012). “Strongly Typed Term Representations in Coq”. Journal of Automated Reasoning. 49(2), pp. 141–159.
  Cited from (1)

  • Chapter 4: Semantics and Graphs, Section 4.2: DAG Syntax And Shared Computations
• Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov (2014). “Dropout: A Simple Way to Prevent Neural Networks from Overfitting”. Journal of Machine Learning Research. 15(56), pp. 1929–1958.
  Cited from (8)

  • Chapter 2: Building Models, Section 2.4: Training State
  • Chapter 7: Examples and Applications, Section 7.2: Parameter Counts And Dropout State
  • Chapter 1: Introduction, Section 1.4: Functional Programming
  • Chapter 1: Introduction, Section 1.4: Training And Evaluation Modes
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Train And Evaluation Mode
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Model Mode And Random State
  • Chapter 4: Semantics and Graphs, Section 4.1: Dropout
• Oleg Kiselyov, 2012. “Typed Tagless Final Interpreters”. In Generic and Indexed Programming (Spring School).
  Cited from (4)

  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: The Differentiable Program Type
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Eager And Graph Interpreters
  • Chapter 4: Semantics and Graphs, Section 4.2: Architecture Representation
  • Chapter 4: Semantics and Graphs, Section 4.3: Scalar Interpretations
• Olivier Bousquet and André Elisseeff (2002). “Stability and Generalization”. Journal of Machine Learning Research. 2, pp. 499–526.
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.5: Algorithmic Stability
• Priya Goyal, Piotr Dollár, Ross Girshick, Pieter Noordhuis, Lukasz Wesolowski, Aapo Kyrola, Andrew Tulloch, Yangqing Jia, and Kaiming He, 2017. “Accurate, Large Minibatch SGD: Training ImageNet in 1 Hour”. arXiv:1706.02677
  Cited from (1)

  • Chapter 2: Building Models, Section 2.4: Learning-rate schedules
• Rico Sennrich, Barry Haddow, and Alexandra Birch, 2016. “Neural Machine Translation of Rare Words with Subword Units”. In Association for Computational Linguistics (ACL).
  Cited from (1)

  • Chapter 2: Building Models, Section 2.3: GPT-2 Byte-Level BPE Files
• Robert Joseph George, Jennifer Cruden, Will Adkisson, Xiangru Zhong, Huan Zhang, and Anima Anandkumar, 2026. “TorchLean: Formalizing Neural Networks in Lean”. arXiv:2602.22631
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.9: Model Review Exercise
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.6: References
• Roy Frostig, Matthew James Johnson, and Chris Leary, 2018. “Compiling Machine Learning Programs via High-Level Tracing”. In Systems for Machine Learning (SysML).
  Cited from (2)

  • Chapter 2: Building Models, Section 2.5: Explicit Differentiation
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: The Differentiable Program Type
• Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar, 2019. “Branch and Bound for Piecewise Linear Neural Network Verification”. arXiv:1909.06588
  Cited from (3)

  • Chapter 1: Introduction, Section 1.2: Stale Parameter Payloads
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 6: Verification and Certificates, Section 6.13: References
• Sebastian Ullrich and Leonardo de Moura, 2019. “Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming”. In Implementation and Application of Functional Languages (IFL).
  Cited from (9)

  • Chapter 2: Building Models, Section 2.5: Explicit Differentiation
  • Chapter 5: Floating Point and Native Boundaries, Section 5.4: Native FFI And Memory Ownership
  • Chapter 1: Introduction, Section 1.5: Immutability And Storage Reuse
  • Chapter 1: Introduction, Section 1.5: Further Reading
  • Chapter 1: Introduction, Section 1.4: Comparing Exact And Rounded Updates
  • Chapter 1: Introduction, Section 1.4: Storage Reuse In The Runtime
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: Gradient Return Values And Accumulation
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Model Mode And Random State
• Sergey Ioffe and Christian Szegedy, 2015. “Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift”. arXiv:1502.03167
  Cited from (6)

  • Chapter 2: Building Models, Section 2.4: Training State
  • Chapter 7: Examples and Applications, Section 7.6: Normalization State
  • Chapter 1: Introduction, Section 1.4: Functional Programming
  • Chapter 1: Introduction, Section 1.4: Training And Evaluation Modes
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Model Mode And Random State
• Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter, 2021. “Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification”. arXiv:2103.06624
  Cited from (10)

  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 1: Introduction, Section 1.1: Verification Artifacts
  • Chapter 1: Introduction, Section 1.1: Interval And Affine Bounds
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 6: Verification and Certificates, Section 6.1: CROWN, Alpha-CROWN, And Alpha-Beta-CROWN
  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
  • Chapter 6: Verification and Certificates, Section 6.14: External Search And Certificate Checking
  • Chapter 6: Verification and Certificates, Section 6.14: Neural Controllers
  • Chapter 6: Verification and Certificates, Section 6.13: Verification Certificates
• Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli, 2018. “On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models”. arXiv:1810.12715
  Cited from (10)

  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 7: Examples and Applications, Section 7.5: Interval Dependency
  • Chapter 7: Examples and Applications, Section 7.7: Model Lowering And Interval Bounds
  • Chapter 1: Introduction, Section 1.7: Input Regions
  • Chapter 1: Introduction, Section 1.2: Dependency Loss And Affine Relaxations
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 4: Semantics and Graphs, Section 4.3: Interval Bound Propagation
  • Chapter 6: Verification and Certificates, Section 6.1: IBP On A Two-Layer Affine Network
  • Chapter 6: Verification and Certificates, Section 6.14: Neural Controllers
  • Chapter 6: Verification and Certificates, Section 6.13: Loss Of Correlation In Interval Bounds
• Sylvie Boldo and Guillaume Melquiond, 2011. “Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq”. In 20th IEEE Symposium on Computer Arithmetic (ARITH).
  Cited from (30)

  • Chapter 7: Examples and Applications, Section 7.6: Float Boundary
  • Chapter 7: Examples and Applications, Section 7.8: Arithmetic
  • Chapter 7: Examples and Applications, Section 7.4: Checked Arithmetic For Returns And Ratios
  • Chapter 7: Examples and Applications, Section 7.9: Theorem Hypotheses
  • Chapter 7: Examples and Applications, Section 7.9: Numerical Guarantees
  • Chapter 7: Examples and Applications, Section 7.5: Float32 Bit Layout Viewer
  • Chapter 7: Examples and Applications, Section 7.7: Numerical Certificate Replay
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Rounded Reals And Executable Formats
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Correspondence With Flocq
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Correspondence With Flocq
  • Chapter 5: Floating Point and Native Boundaries, Section 5.1: Formats And Rounding
  • Chapter 5: Floating Point and Native Boundaries, Section 5.3: Reduction Order In The Numerical Contract
  • Chapter 5: Floating Point and Native Boundaries, Section 5.2: Training-Step Bound Assumptions
  • Chapter 1: Introduction, Section 1.1: Fused Multiply-Add
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.6: Floating Point
  • Chapter 1: Introduction, Section 1.6: References
  • Chapter 1: Introduction, Section 1.2: Floating-Point Arithmetic
  • Chapter 1: Introduction, Section 1.2: References
  • Chapter 1: Introduction, Section 1.4: Floating-Point Equality
  • Chapter 1: Introduction, Section 1.4: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Executable Binary32 Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Floating-Point Transcendentals
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 4: Semantics and Graphs, Section 4.3: Scalar Interpretations
  • Chapter 4: Semantics and Graphs, Section 4.1: Scalar Polymorphism
  • Chapter 6: Verification and Certificates, Section 6.5: Ridge Regression In Binary32
  • Chapter 6: Verification and Certificates, Section 6.12: Exact Proofs And Floating Execution
  • Chapter 6: Verification and Certificates, Section 6.6: Newton-Schulz Iteration
  • Chapter 6: Verification and Certificates, Section 6.4: NF Operations: Rounded Real Arithmetic
• Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond (2015). “Verified Compilation of Floating-Point Computations”. Journal of Automated Reasoning. 54(2), pp. 135–163.
  Cited from (16)

  • Chapter 7: Examples and Applications, Section 7.6: Float Boundary
  • Chapter 7: Examples and Applications, Section 7.9: Theorem Hypotheses
  • Chapter 7: Examples and Applications, Section 7.9: Numerical Guarantees
  • Chapter 7: Examples and Applications, Section 7.5: Float32 Bit Layout Viewer
  • Chapter 7: Examples and Applications, Section 7.7: Floating-Point And Rational Arithmetic
  • Chapter 5: Floating Point and Native Boundaries, Section 5.5: Executable Refinement And Native Execution
  • Chapter 5: Floating Point and Native Boundaries, Section 5.3: Reduction Order In The Numerical Contract
  • Chapter 1: Introduction, Section 1.1: Fused Multiply-Add
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 1: Introduction, Section 1.6: Floating Point
  • Chapter 1: Introduction, Section 1.6: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.1: Executable Binary32 Arithmetic
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Floating-Point Transcendentals
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.4: Parameterization, Reduction, And Arithmetic
  • Chapter 4: Semantics and Graphs, Section 4.3: The Executable Tanh Interval Rule
  • Chapter 4: Semantics and Graphs, Section 4.1: Scalar Polymorphism
• The mathlib Community, 2020. “The Lean Mathematical Library”. In Certified Programs and Proofs (CPP).
  Cited from (19)

  • Chapter 2: Building Models, Section 2.1: Dot-Product Theorems
  • Chapter 7: Examples and Applications, Section 7.4: GridWorld Definition
  • Chapter 7: Examples and Applications, Section 7.9: Theorem Hypotheses
  • Chapter 1: Introduction, Section 1.3: Command Help And Further Reading
  • Chapter 1: Introduction, Section 1.5: Programs, Propositions, And Proofs
  • Chapter 1: Introduction, Section 1.5: Further Reading
  • Chapter 1: Introduction, Section 1.1: The equations
  • Chapter 1: Introduction, Section 1.1: References
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.3: The Outer-Product Gradient Theorem
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.5: Runtime And Proof
  • Chapter 4: Semantics and Graphs, Section 4.2: The Equivalence Theorem
  • Chapter 4: Semantics and Graphs, Section 4.3: Scalar Interpretations
  • Chapter 4: Semantics and Graphs, Section 4.1: MLP Specification Equivalence
  • Chapter 6: Verification and Certificates, Section 6.8: Higher-Dimensional Domains
  • Chapter 6: Verification and Certificates, Section 6.3: Operator Derivative Proof Obligations
  • Chapter 6: Verification and Certificates, Section 6.12: Dot Products And Norms
  • Chapter 6: Verification and Certificates, Section 6.6: Gradient Descent As A Contractive Map
  • Chapter 6: Verification and Certificates, Section 6.10: Forward Diffusion Kernels
  • Chapter 6: Verification and Certificates, Section 6.10: Probability And Autograd Proof Gaps
• Tri Dao, Daniel Y. Fu, Stefano Ermon, Atri Rudra, and Christopher Ré, 2022. “FlashAttention: Fast and Memory-Efficient Exact Attention with IO-Awareness”. arXiv:2205.14135
  Cited from (5)

  • Chapter 7: Examples and Applications, Section 7.6: Contract Review
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: The Attention Specification Theorem
  • Chapter 3: Runtime, Autograd, and Interop, Section 3.2: References
  • Chapter 4: Semantics and Graphs, Section 4.1: Attention masks
  • Chapter 6: Verification and Certificates, Section 6.4: Normalization And Attention
• Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G. Bellemare, Alex Graves, Martin Riedmiller, Andreas K. Fidjeland, Georg Ostrovski, Stig Petersen, Charles Beattie, Amir Sadik, Ioannis Antonoglou, Helen King, Dharshan Kumaran, Daan Wierstra, Shane Legg, and Demis Hassabis (2015). “Human-level control through deep reinforcement learning”. Nature. 518(7540), pp. 529–533.
  Cited from (3)

  • Chapter 2: Building Models, Section 2.3: Generated Streams
  • Chapter 7: Examples and Applications, Section 7.4: Reinforcement Learning
  • Chapter 7: Examples and Applications, Section 7.4: Off-Policy Data: Replay Buffers And DQN
• Xavier Glorot and Yoshua Bengio, 2010. “Understanding the Difficulty of Training Deep Feedforward Neural Networks”. In Artificial Intelligence and Statistics (AISTATS).
  Cited from (1)

  • Chapter 2: Building Models, Section 2.4: Initial Parameter Values
• Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Roșu, 2021. “Towards a Trustworthy Semantics-Based Language Framework via Proof Generation”. In Computer Aided Verification (CAV).
  Cited from (1)

  • Chapter 6: Verification and Certificates, Section 6.2: Related Systems
• Xudong Mao, Qing Li, Haoran Xie, Raymond Y. K. Lau, Zhen Wang, and Stephen Paul Smolley, 2017. “Least Squares Generative Adversarial Networks”. arXiv:1611.04076
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.3: Adversarial Training
  • Chapter 7: Examples and Applications, Section 7.3: Further Reading
• Ya-Chien Chang, Nima Roohi, and Sicun Gao, 2019. “Neural Lyapunov Control”. In Neural Information Processing Systems (NeurIPS).
  Cited from (2)

  • Chapter 7: Examples and Applications, Section 7.8: Verification Commands
  • Chapter 6: Verification and Certificates, Section 6.14: Neural Controllers
• Zongyi Li, Nikola Kovachki, Kamyar Azizzadenesheli, Burigede Liu, Kaushik Bhattacharya, Andrew Stuart, and Anima Anandkumar, 2021. “Fourier Neural Operator for Parametric Partial Differential Equations”. arXiv:2010.08895
  Cited from (6)

  • Chapter 2: Building Models, Section 2.2: Model Family Constructors
  • Chapter 2: Building Models, Section 2.1: Tensor Type
  • Chapter 7: Examples and Applications, Section 7.1: Neural Operators
  • Chapter 7: Examples and Applications, Section 7.1: References
  • Chapter 7: Examples and Applications, Section 7.2: Burgers Neural Operator
  • Chapter 7: Examples and Applications, Section 7.9: Scientific ML