Author name cluster

Boris Düdder

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

IJCAI Conference 2024 Conference Paper

Privacy-Preserving UCB Decision Process Verification via zk-SNARKs

Xikun Jiang
He Lyu
Chenhao Ying
Yibin Xu
Boris Düdder
Yuan Luo

With the increasingly widespread application of machine learning, how to strike a balance between protecting the privacy of data and algorithm parameters and ensuring the verifiability of machine learning has always been a challenge. This study explores the intersection of reinforcement learning and data privacy, specifically addressing the Multi-Armed Bandit (MAB) problem with the Upper Confidence Bound (UCB) algorithm. We introduce zkUCB, an innovative algorithm that employs the Zero-Knowledge Succinct Non-Interactive Argument of Knowledge (zk-SNARKs) to enhance UCB. zkUCB is carefully designed to safeguard the confidentiality of training data and algorithmic parameters, ensuring transparent UCB decision-making. Experiments highlight zkUCB's superior performance, attributing its enhanced reward to judicious quantization bit usage that reduces information entropy in the decision-making process. zkUCB's proof size and verification time scale linearly with the execution steps of zkUCB. This showcases zkUCB's adept balance between data security and operational efficiency. This approach contributes significantly to the ongoing discourse on reinforcing data privacy in complex decision-making processes, offering a promising solution for privacy-sensitive applications.

PDF Details DOI

Highlights Conference 2013 Conference Abstract

Combinatory Logic synthesis and alternation

Boris Düdder
Moritz Martens
Jakob Rehof:

We discuss complexity theoretic results in the context of Combinatory Logic Synthesis which is a new approach to component-based synthesis using type inhabitation. The complexity theoretic reductions behind these results establish explicit and effective connections between combinatory logic inhabitation and automata theoretic models, in the form of alternating tree automata and alternating space bounded Turing machines. These computational models that are commonly found in automata theoretic approaches are related to synthesis based on logics within the MSO family of logics.

PDF Details

CSL Conference 2012 Conference Paper

Bounded Combinatory Logic

Boris Düdder
Moritz Martens
Jakob Rehof
Pawel Urzyczyn

In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), usually K and S. In this setting the set of provable formulas (inhabited types) is PSPACE-complete in simple types and undecidable in intersection types. When arbitrary sets of axiom schemes are considered, the inhabitation problem is undecidable even in simple types (this is known as Linial-Post theorem). k-bounded combinatory logic with intersection types arises from combinatory logic by imposing the bound k on the depth of types (formulae) which may be substituted for type variables in axiom schemes. We consider the inhabitation (provability) problem for k-bounded combinatory logic: Given an arbitrary set of typed combinators and a type tau, is there a combinatory term of type tau in k-bounded combinatory logic? Our main result is that the problem is (k+2)-EXPTIME complete for k-bounded combinatory logic with intersection types, for every fixed k (and hence non-elementary when k is a parameter). We also show that the problem is EXPTIME-complete for simple types, for all k. Theoretically, our results give new insight into the expressive power of intersection types. From an application perspective, our results are useful as a foundation for composition synthesis based on combinatory logic.

Details