---
OA_place: publisher
_id: '11362'
abstract:
- lang: eng
  text: "Deep learning has enabled breakthroughs in challenging computing problems
    and has emerged as the standard problem-solving tool for computer vision and natural
    language processing tasks.\r\nOne exception to this trend is safety-critical tasks
    where robustness and resilience requirements contradict the black-box nature of
    neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital
    to provide guarantees on neural network agents' safety and robustness criteria.
    \r\nThis can be achieved by developing formal verification methods to verify the
    safety and robustness properties of neural networks.\r\n\r\nOur goal is to design,
    develop and assess safety verification methods for neural networks to improve
    their reliability and trustworthiness in real-world applications.\r\nThis thesis
    establishes techniques for the verification of compressed and adversarially trained
    models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst,
    we establish the problem of verifying quantized neural networks. Quantization
    is a technique that trades numerical precision for the computational efficiency
    of running a neural network and is widely adopted in industry.\r\nWe show that
    neglecting the reduced precision when verifying a neural network can lead to wrong
    conclusions about the robustness and safety of the network, highlighting that
    novel techniques for quantized network verification are necessary. We introduce
    several bit-exact verification methods explicitly designed for quantized neural
    networks and experimentally confirm on realistic networks that the network's robustness
    and other formal properties are affected by the quantization.\r\n\r\nFurthermore,
    we perform a case study providing evidence that adversarial training, a standard
    technique for making neural networks more robust, has detrimental effects on the
    network's performance. This robustness-accuracy tradeoff has been studied before
    regarding the accuracy obtained on classification datasets where each data point
    is independent of all other data points. On the other hand, we investigate the
    tradeoff empirically in robot learning settings where a both, a high accuracy
    and a high robustness, are desirable.\r\nOur results suggest that the negative
    side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally,
    we consider the problem of verifying safety when running a Bayesian neural network
    policy in a feedback loop with systems over the infinite time horizon. Bayesian
    neural networks are probabilistic models for learning uncertainties in the data
    and are therefore often used on robotic and healthcare applications where data
    is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian
    neural networks so that they yield probability distributions over safe decisions
    only.\r\nOur method learns a safety certificate that guarantees safety over the
    infinite time horizon to determine which decisions are safe in every possible
    state of the system.\r\nWe demonstrate the effectiveness of our approach on a
    series of reinforcement learning benchmarks."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Mathias
  full_name: Lechner, Mathias
  id: 3DC22916-F248-11E8-B48F-1D18A9856A87
  last_name: Lechner
citation:
  ama: Lechner M. Learning verifiable representations. 2022. doi:<a href="https://doi.org/10.15479/at:ista:11362">10.15479/at:ista:11362</a>
  apa: Lechner, M. (2022). <i>Learning verifiable representations</i>. Institute of
    Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:11362">https://doi.org/10.15479/at:ista:11362</a>
  chicago: Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science
    and Technology Austria, 2022. <a href="https://doi.org/10.15479/at:ista:11362">https://doi.org/10.15479/at:ista:11362</a>.
  ieee: M. Lechner, “Learning verifiable representations,” Institute of Science and
    Technology Austria, 2022.
  ista: Lechner M. 2022. Learning verifiable representations. Institute of Science
    and Technology Austria.
  mla: Lechner, Mathias. <i>Learning Verifiable Representations</i>. Institute of
    Science and Technology Austria, 2022, doi:<a href="https://doi.org/10.15479/at:ista:11362">10.15479/at:ista:11362</a>.
  short: M. Lechner, Learning Verifiable Representations, Institute of Science and
    Technology Austria, 2022.
corr_author: '1'
date_created: 2022-05-12T07:14:01Z
date_published: 2022-05-12T00:00:00Z
date_updated: 2026-04-16T09:46:06Z
day: '12'
ddc:
- '004'
degree_awarded: PhD
department:
- _id: GradSch
- _id: ToHe
doi: 10.15479/at:ista:11362
ec_funded: 1
file:
- access_level: closed
  checksum: 8eefa9c7c10ca7e1a2ccdd731962a645
  content_type: application/zip
  creator: mlechner
  date_created: 2022-05-13T12:33:26Z
  date_updated: 2022-05-13T12:49:00Z
  file_id: '11378'
  file_name: src.zip
  file_size: 13210143
  relation: source_file
- access_level: open_access
  checksum: 1b9e1e5a9a83ed9d89dad2f5133dc026
  content_type: application/pdf
  creator: mlechner
  date_created: 2022-05-16T08:02:28Z
  date_updated: 2022-05-17T15:19:39Z
  file_id: '11382'
  file_name: thesis_main-a2.pdf
  file_size: 2732536
  relation: main_file
file_date_updated: 2022-05-17T15:19:39Z
has_accepted_license: '1'
keyword:
- neural networks
- verification
- machine learning
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: '124'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication_identifier:
  isbn:
  - 978-3-99078-017-6
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '11366'
    relation: part_of_dissertation
    status: public
  - id: '10665'
    relation: part_of_dissertation
    status: public
  - id: '10667'
    relation: part_of_dissertation
    status: public
  - id: '10666'
    relation: part_of_dissertation
    status: public
  - id: '7808'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
title: Learning verifiable representations
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2022'
...