+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Freitag, 22. Dezember 2023, 11.00 Uhr
Ort: Gebäude E3, Seminarraum 118, Ahornstr. 55
Referent: Moritz Ibing M.Sc.
Lehrstuhl Informatik 8
Thema: Localized Control over the Latent Space of Neural Networks
Abstract:
Neural networks (NNs) are prevalent today when it comes to analyzing (classifying,
segmenting, detecting, etc.) or generating data in all kinds of modalities (text,
images, 3D shapes, etc.). They are so useful in these areas, because they have
great representation power, while being easy to optimize and generalizing well to
unseen data. However, their complexity makes them hard to interpret and modify.
Neural networks are usually used to compute a mapping between the data space
and a so-called latent space. Often we are interested in local properties of such a
mapping. For example, we might want to slightly change the embedding of a data
point to achieve a different classification. Such local modifications however are
difficult, as NNs usually have globally entangled properties. In this work we will
propose ideas how to deal with this problem.
Local control is especially of importance for shape representations. It has been
shown that NNs are well suited to represent these e.g. as parametric or implicit
functions. However, when a global function is used, local supervision is hard to
model. We therefore impose additional structure on the latent space of functional
representations, making them easier to work with and more expressive.
Such a structured representation makes downstream tasks easier, as we are more
versatile regarding the shapes we can represent, we can make use of its regularity
for the network design, and it allows a compressed encoding that can help to reduce
memory consumption. Our focus will be on general shape generation, but we will
also present more specific applications like shape completion or super-resolution
among others. Our approaches set the state-of-the-art among generative models
both in previously used metrics and a newly introduced measure we adapt for this
purpose.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Montag, 13. November 2023, 09.30 Uhr
Ort: Informatikzentrum, E3, 2. Etage, Raum 9222
Referent: Henri Lotze M.Sc.
Lehr- und Forschungsgebiet Theoretische Informatik
Thema: Going Offline -- Delays, Reservations and Predictions in Online
Computation
Abstract:
The study of classical online computation builds upon a rather simple
model. The input to a given problem is not known in advance,
decisions have to made immediately upon the arrival of a new element
and these decisions are irrevocable.
While this model is very well suitable to compute worst case bounds to
a broad range of problems, there are some problems which are not well
suited for this analysis. Naturally, problems that do not admit a
constant approximation ratio in their offline formulation do not admit
a constant competitive ratio in the worst case in the online
formulation. However, some problems that are approximable still do
not admit a constant competitive ratio when analyzed in the online
case. For a subset of these problems, such as the Online Simple
Knapsack problem and the class of general F-Node- and F-Edge-Deletion
problems, the reason for this seems to be that a single, specific bad
decision by an algorithm can be arbitrarily punished by an adversary.
In this talk, we explore modifications of the classical online model
with the aim to find natural models that on the one hand cover a large
range of problems and on the other hand work against pathological
kinds of instances that restrict an algorithm from obtaining a
constant competitive ratio. To this end, we study three modifications
of the classical online model.
The models that we study are that of "Late Accepts" -- with Advice --,
which allows to postpone decisions in online minimization problems
until a current partial solution does not uphold a certain property
anymore. The second one is that of "Reservations", in which any
decision may be postponed for a cost proportional to the gain of an
item. Finally, the model of "Bounded Predictions" allows an online
algorithm to see the complete instance in advance, with a caveat:
There is noise on the instance -- controlled by an adversary -- and
each element may actually deviate from its prediction, up to factor
that is known to the algorithm.
We are able to partially classify the advice complexity of the
complete class of both F-Node-Deletion and F-Edge-Deletion problems.
We give tight bounds on the competitive ratio for the Online Simple
Knapsack problem with Reservations for the whole range of possible
reservation costs, i.e. for a factor between 0 and 1. Finally, we give
partially tight bounds for the Online Simple Knapsack problem with
Bounded Predictions for the whole range of possible noise factors on
the size of the items.
Es laden ein: die Dozentinnen und Dozenten der Informatik
+**********************************************************************
*
*
* Einladung
*
*
*
* Informatik-Oberseminar
*
*
*
+**********************************************************************
Zeit: Mittwoch, 13. Dezember 2023, 16:00 Uhr
Ort: Informatikzentrum Ahornstr. 55, Raum 5053.2 (B-IT)
Referentin: Jana Berger M.Sc.
Lehrstuhl Informatik 2
Thema: Applying Software Model Checking: Experiences and Advancements
Abstract:
We present a comprehensive investigation into the applicability of
formal methods for software model checking, with a particular emphasis
on the automotive sector.
The work is grounded in a practical study carried out with Ford Motor
Company, offering a basis for the exploration and enhancement of both
commercial and academic model checking tools.
In the first part of the study, we collaborated with Ford Motor Company
to formalise their natural language requirements for two automotive case
studies employing the commercial C code model checker, BTC EmbeddedPlatform.
Our investigation focused on the verification of auto-generated C code
from Simulink models, analysing the associated challenges and providing
practical recommendations for both engineers and tool developers.
Building on this foundation, we then applied academic C code model
checkers to the same case studies, comparing their performance
against BTC EmbeddedPlatform.
This comparison yielded a fresh set of insights and recommendations
aimed at enhancing academic model checking tools.
The second part of this work addresses the development of new tools and
methods aimed at advancing the state of the art in software model checking.
First, we designed NITWIT, a novel violation witness validator based on
C code interpretation.
This approach yields fast execution with a minimal memory footprint and
is agnostic of existing model checkers.
Next, we developed a tool for writing specifications with formal
semantics, tailored specifically for the automotive industry.
This tool is capable of auto-generating (a) specifications in Simulink,
BTC and pure C code for verification, streamlining the formal
verification process, and (b) natural language representations with
fixed semantics for stakeholders and non-experts to review and use.
Finally, to better facilitate the testing and benchmarking of C code
model checkers, we built a tool that generates C code.
The style of the generated code borrows from the two case studies, thus
providing a valuable resource for stress-testing model checkers while
respecting non-disclosure agreements, offering a wide variety of
controllable code metrics, features and transformers.
In summary, this thesis provides new and relevant insights as well as
novel tools aimed at improving the application and comparison of
software model checking, particularly in the context of the automotive
industry.
It offers practical solutions to real-world challenges, and helps to
bridge the gap between commercial and academic approaches to software
model checking.
Es laden ein: die Dozentinnen und Dozenten der Informatik