Go to JKU Homepage
{{ item.AUTOREN_ZITAT }}:
{{ item.TITEL }}{{ zitatInLang(item) }}
Hard Benchmarks for True QBFs
Solving approaches for quantified Boolean formulas (QBFs), a generalisation of SAT, are often characterized in terms of hard formula families for investigations in terms of proof complexity. In the literature, only false formulas are considered. In this work, we consider the case of true formulas. We develop novel benchmarks and perform extensive evaluations.
Supervisor: Martina Seidl, JKU Linz, Austria
Dates: October 2021 - Ongoing
Advanced Redundancy Proofs for SAT
Tools for solving the Boolean satisfiability (SAT) problem, deciding whether a formula in propositional logic has a solution, have become highly efficient in practice, despite the absence of any known polynomial-time algorithm. Modern SAT solvers are typically able to emit proofs for unsatisfiable formulas, but current proof formats, make it difficult to compactly express crucial solving techniques. In this work we develop novel techniques to overcome these limitations.
Supervisor: Univ.Prof. Dr Armin Biere, Freiburg University (previously JKU Linz)
Dates: January 2019 - Ongoing
Data-efficient Machine Learning
The successes of deep neural networks have largely been in areas where a vast amount of data is available.
However, in many applications from science and engineering hand-labeled data is either limited or expensive to collect.
This has led to a growing interest in reducing the required amount of data to train machine-learning models.
The problem is often framed as few-shot learning with the goal to learn concepts from few labeled examples that generalize to new unseen examples.
In this project we aim to develop learning algorithms that are especially useful in this low-data regime.
* Supervisor: Sepp Hochreiter, JKU Linz, Austria
* Dates: 01 July 2021 – Ongoing
Out of Distribution Generalization in Reinforcement Learning
Many settings in Reinforcement Learning (RL) demand abilities to generalise beyond the distributions seen during training.
A change in the distribution of the states or rewards could result in drastic performance degradation in agents, if not equipped with suitable mechanisms. Furthermore, the amount of stochasticity in the environment could result in the lack of generalisation, and a change in stochasticity could result in failure of learning, preventing agents from achieving their goals.
Not only an agent has to learn new concepts and adapt its policy accordingly, it has to also remember the learnt concepts without forgetting.
In the real world, all of the aformentioned cases occur on a day to day basis, and we as humans have developed abilities to adapt and learn in a continual manner, which enables us to navigate through such daily challenges. We can continually learn and adapt to non-stationarities, and discover policies based on abstractions that generalise in a satisfactory level.
This project is focused on developing agents that can deal with different levels and kinds of continual distribution shift, and can cope with various kinds of non-stationarity in an environment, leaning general policies from abstract representations and concepts that can generalise to distributions beyond training environments.
Supervisor: Sepp Hochreiter, JKU Linz, Austria
Dates: 15 Dec 2021 – Ongoing
TBA
Supervisor: Sepp Hochreiter, JKU Linz, Austria
Dates: 01 Jan 2020 - Ongoing
Learning general-purpose audio representations with deep neural networks
Audio classification and tagging are central tasks in the field of
machine listening. They are essential for machines to recognize the
environment and identify events in their surroundings, and thus a
critical component of machine perception. These tasks are relevant in a
wide range of applications, including content-based multimedia
information retrieval, context-aware smart devices, and monitoring
systems. One significant barrier to machine audio recognition is the
high cost and scarcity of high-quality labeled data, particularly for
powerful learners such as deep neural networks. We investigate the
incorporation of inductive biases into neural network architectures and
the training process in order to improve generalization when training on
small audio datasets. We also investigate how to extract representations
from models trained on large-scale, general-purpose datasets, to be
transferred to specialized tasks.
* Supervisor: Gerhard Widmer, JKU Linz, Austria
* Dates: 01 Jan 2020 – Ongoing
Knowledge transfer from Simulation to real world
Analysis of signal mixtures is an elementary problem found in application domains specific to various signal modalities. For musical audio signals specifically, it presents a step fundamental to many subsequent tasks in the Music Information Retrieval, such as music transcription or instrument identification and extraction. The underlying goal is often to identify the sources present in the mixture, potentially along with their various properties. In the context of musical signals, atomicity of signal sources can also be defined at various levels. A central difficulty stems from the combinatorial nature of the problem, as music allows for a large number of atomic sources with varying degrees of polyphony (concurrency of source activity across time). We aim to address the combinatorial nature of the problem by analysing mixtures through linear decomposition, while leveraging advances on the front of deep bijective models of data density (e.g., "normalizing flows") in order to better express individual sources by modelling them independently.
* Supervisor: Gerhard Widmer, JKU Linz, Austria
* Dates: 01 Jan 2022 – Ongoing
Modelling Signal Mixtures with Density Models of Sources
Analysis of signal mixtures is an elementary problem found in application domains specific to various signal modalities. For musical audio signals specifically, it presents a step fundamental to many subsequent tasks in the Music Information Retrieval, such as music transcription or instrument identification and extraction. The underlying goal is often to identify the sources present in the mixture, potentially along with their various properties. In the context of musical signals, atomicity of signal sources can also be defined at various levels. A central difficulty stems from the combinatorial nature of the problem, as music allows for a large number of atomic sources with varying degrees of polyphony (concurrency of source activity across time). We aim to address the combinatorial nature of the problem by analysing mixtures through linear decomposition, while leveraging advances on the front of deep bijective models of data density (e.g., "normalizing flows") in order to better express individual sources by modelling them independently.
* Supervisor: Gerhard Widmer, JKU Linz, Austria
* Dates: 01 October 2019 – Ongoing
Explainability and Fairness in Music Recommender Systems
Music Recommender Systems have been increasingly become more popular in recent years and currently represent one of the main tools for music exploration and discovery.
Due to their frequent use by millions of users worldwide, it is crucial to ensure that these systems (1) provide insights on their functioning to enhance trust and transparency of their users and (2) avoid possible discrimination and biases e.g. by providing different treatment to different user groups in terms of gender, age, culture, among many. In this context, I aim to develop interpretable/explainable models for recommender systems, especially in the music domain, which can help explore and correct possible misconducts in terms of fairness of these systems.
* Supervisor: Markus Schedl, JKU Linz, Austria
* Dates: 15 September 2019 – Ongoing
Finding and Analyzing Matrix Multiplication Algorithms with Computer Algebra
Matrix Multiplication is one of the fundamental operations in
Linear Algebra and thus has applications in lots of different areas.
Algorithms for matrix multiplication are solutions of a particular
system of equations. This system rapidly grows with the
size of the matrices, therefore we can only solve it for very small
sizes. Algorithms for small matrices are especially important
because they can be used to multiply larger matrices as well. While
for the 2x2 case we know all solutions for optimal algorithms,
already for the 3x3 case we do not know an optimal algorithm at all.
Also finding new algorithms that meet the currently best known bound
is a nontrivial task. We use large scale computations to search for
new algorithms and to get a better understanding of the solution set.
* Supervisor: Manuel Kauers, JKU Linz, Austria
* Dates: 20 Jan 2020 – Ongoing
Long Term Credit Assignment in RL
His research revolves aroung long term credit assignment in Reinforcement Learning and how we can build algorithms which learn to build abstractions to learn faster and generalize to unknown environments.
Supervisor: Sepp Hochreiter, JKU Linz, Austria
Dates: 01.Jan 2019 - Ongoing
Application of Neural Networks in Many-Body Physics
Problems with a large number of interacting particles are ubiquitous in science and key to many future technologies. Recently, the successful application of deep learning methods to such problems led to remarkable progress in statistical mechanics, quantum chemistry and condensed matter physics.
We will investigate variational methods and Graph Neural Networks in the context of many-body physics problems related to the identification of ground states and phases of matter. For supervised methods a crucial aspect will be the data efficiency and the combination with few-shot learning and physics inspired model architectures.
* Supervisor: Sepp Hochreiter, JKU Linz, Austria
* Dates: 01 May 2021 – Ongoing
Using Domain Adaptation to counter the distribution shift when testing in new domains
Machine Learning, and in particular deep learning, requires a large amount of labeled data to train models that master complex tasks. In some domains, for example, healthcare or electric motor fault detection, gathering label data can raise privacy issues or is labor intensive. Domain Adaptation tackles this issue by transferring knowledge from source domains to different, but related target domains. An especially promising direction in this field is to simulate real-world processes, which allow to produce automatically labeled data, and apply domain adaptation techniques to make this knowledge applicable to the underlying real-world problem. Successfully mastering this procedure can have a large impact in lots of application areas, for instance, simulating faults of electrical devices in order to monitor the condition of the real devices in production, or generalizing across a variety of recording devices in the audio domain.
* Supervisor: Gerhard Widmer, JKU Linz, Austria
* Dates: 21 September 2021 – Ongoing
ML in Wireless Communication
For Digital Wireless Communication like WLAN or 5G, one has to solve the problem of equalization. Sending data over a wireless channel always introduces noise, mixing, echos, cancellations and other distortions to the received signal. Reducing the bit-errors introduced by the channel to enhance the speed and link-stability is a topic of ongoing research. This project is approaching the problem from the direction of machine learning by utilizing methods like hopfield-transofmers and tree-search strategies to find better equalization methods and compete with the current state-of-the-art techniques.
Supervisor: Sepp Hochreiter, JKU Linz, Austria
Dates: 01 Dec 2019 - Ongoing
Improving Expansion-Based QBF Solving
The works aims to improve the certification of modern solvers for quantified Boolean formulas. Certification of expansion-based QBF solving is limited by the fact that modern SAT solvers do not provide resolution proofs any more. The aim of this project is to replace this inference proof system with a more modern interference proof system. We formalize this novel system, implement it in a QBF solving framework, and qualify any improvements in proof complexity.
Supervisor: Univ-Prof. Dr. Martina Seidl, JKU Linz
Dates: 01 October 2021 – Ongoing
Johannes Kepler University Linz
Altenberger Straße 69
4040 Linz, Austria
