@inproceedings{10668, abstract = {Robustness to variations in lighting conditions is a key objective for any deep vision system. To this end, our paper extends the receptive field of convolutional neural networks with two residual components, ubiquitous in the visual processing system of vertebrates: On-center and off-center pathways, with an excitatory center and inhibitory surround; OOCS for short. The On-center pathway is excited by the presence of a light stimulus in its center, but not in its surround, whereas the Off-center pathway is excited by the absence of a light stimulus in its center, but not in its surround. We design OOCS pathways via a difference of Gaussians, with their variance computed analytically from the size of the receptive fields. OOCS pathways complement each other in their response to light stimuli, ensuring this way a strong edge-detection capability, and as a result an accurate and robust inference under challenging lighting conditions. We provide extensive empirical evidence showing that networks supplied with OOCS pathways gain accuracy and illumination-robustness from the novel edge representation, compared to other baselines.}, author = {Babaiee, Zahra and Hasani, Ramin and Lechner, Mathias and Rus, Daniela and Grosu, Radu}, booktitle = {Proceedings of the 38th International Conference on Machine Learning}, issn = {2640-3498}, location = {Virtual}, pages = {478--489}, publisher = {ML Research Press}, title = {{On-off center-surround receptive fields for accurate and robust image classification}}, volume = {139}, year = {2021}, } @inproceedings{10670, abstract = {Imitation learning enables high-fidelity, vision-based learning of policies within rich, photorealistic environments. However, such techniques often rely on traditional discrete-time neural models and face difficulties in generalizing to domain shifts by failing to account for the causal relationships between the agent and the environment. In this paper, we propose a theoretical and experimental framework for learning causal representations using continuous-time neural networks, specifically over their discrete-time counterparts. We evaluate our method in the context of visual-control learning of drones over a series of complex tasks, ranging from short- and long-term navigation, to chasing static and dynamic objects through photorealistic environments. Our results demonstrate that causal continuous-time deep models can perform robust navigation tasks, where advanced recurrent models fail. These models learn complex causal control representations directly from raw visual inputs and scale to solve a variety of tasks using imitation learning.}, author = {Vorbach, Charles J and Hasani, Ramin and Amini, Alexander and Lechner, Mathias and Rus, Daniela}, booktitle = {35th Conference on Neural Information Processing Systems}, location = {Virtual}, title = {{Causal navigation by continuous-time neural networks}}, year = {2021}, } @inproceedings{10688, abstract = {Civl is a static verifier for concurrent programs designed around the conceptual framework of layered refinement, which views the task of verifying a program as a sequence of program simplification steps each justified by its own invariant. Civl verifies a layered concurrent program that compactly expresses all the programs in this sequence and the supporting invariants. This paper presents the design and implementation of the Civl verifier.}, author = {Kragl, Bernhard and Qadeer, Shaz}, booktitle = {Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design}, editor = {Ruzica, Piskac and Whalen, Michael W.}, isbn = {978-3-85448-046-4}, location = {Virtual}, pages = {143–152}, publisher = {TU Wien Academic Press}, title = {{The Civl verifier}}, doi = {10.34727/2021/isbn.978-3-85448-046-4_23}, volume = {2}, year = {2021}, } @unpublished{9281, abstract = {We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics.}, author = {Dubach, Guillaume and Mühlböck, Fabian}, booktitle = {arXiv}, title = {{Formal verification of Zagier's one-sentence proof}}, doi = {10.48550/arXiv.2103.11389}, year = {2021}, } @inproceedings{10665, abstract = {Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network’s correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors into account. In this paper, we show that verifying the bitexact implementation of quantized neural networks with bitvector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.}, author = {Henzinger, Thomas A and Lechner, Mathias and Zikelic, Dorde}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {5A}, pages = {3787--3795}, publisher = {AAAI Press}, title = {{Scalable verification of quantized neural networks}}, volume = {35}, year = {2021}, }