SearcharxivSearch

arXiv subjects

Martin Hofmann

Publications and source records attributed to Martin Hofmann.

At least 19 recordsLinked to original sources

Unleashing HyDRa: Hybrid Fusion, Depth Consistency and Radar for Unified 3D Perception

Low-cost, vision-centric 3D perception systems for autonomous driving have made significant progress in recent years, narrowing the gap to expensive LiDAR-based methods. The primary challenge in becoming a fully reliable alternative lies in robust depth prediction capabilities, as camera-based systems struggle with long detection ranges and adverse lighting and weather conditions. In this work, we introduce HyDRa, a novel camera-radar fusion architecture for diverse 3D perception tasks. Building upon the principles of dense BEV (Bird's Eye View)-based architectures, HyDRa introduces a hybrid fusion approach to combine the strengths of complementary camera and radar features in two distinct representation spaces. Our Height Association Transformer module leverages radar features already in the perspective view to produce more robust and accurate depth predictions. In the BEV, we refine the initial sparse representation by a Radar-weighted Depth Consistency. HyDRa achieves a new state-of-the-art for camera-radar fusion of 64.2 NDS (+1.8) and 58.4 AMOTA (+1.5) on the public nuScenes dataset. Moreover, our new semantically rich and spatially accurate BEV features can be directly converted into a powerful occupancy representation, beating all previous camera-based methods on the Occ3D benchmark by an impressive 3.7 mIoU. Code and models are available at https://github.com/phi-wol/hydra.

cs.CV

Object classification on video data of meteors and meteor-like phenomena: algorithm and data

Every moment, countless meteoroids enter our atmosphere unseen. The detection and measurement of meteors offer the unique opportunity to gain insights into the composition of our solar systems' celestial bodies. Researchers, therefore, carry out a wide-area-sky-monitoring to secure 360-degree video material, saving every single entry of a meteor. Existing machine intelligence cannot accurately recognize events of meteors intersecting the earth's atmosphere due to a lack of high-quality training data publicly available. This work presents four reusable open source solutions for researchers trained on data we collected due to the lack of available labeled high-quality training data. We refer to the proposed dataset as the NightSkyUCP dataset, consisting of a balanced set of 10,000 meteor- and 10,000 non-meteor-events. Our solutions apply various machine learning techniques, namely classification, feature learning, anomaly detection, and extrapolation. For the classification task, a mean accuracy of 99.1\% is achieved. The code and data are made public at figshare with DOI: 10.6084/m9.figshare.16451625

astro-ph.IM

Type-Based Analysis of Logarithmic Amortised Complexity

We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is potential-based. The type system makes use of logarithmic potential functions and is the first such system to exhibit *logarithmic amortised complexity*. With our approach we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of *splaying*, once the type annotations are fixed.

cs.LO

Quantum Shuttle: Traffic Navigation with Quantum Computing

The Web Summit conference in Lisbon, Portugal, is one of the biggest technology conferences in Europe, attended by tens of thousands of people every year. The high influx of people into Lisbon causes significant stress on the city's transit services for the duration of the conference. For the Web Summit 2019, Volkswagen AG partnered with the city of Lisbon for a pilot project to provide quantum computing-based traffic optimization. A two-phase solution was implemented: the first phase used data science techniques to analyze the movement of people from previous conferences to build temporary new bus routes throughout the city. The second phase used a custom Android navigation app installed in the buses operated by Carris, powered by a quantum optimization service provided by Volkswagen that connected to live traffic data and a D-Wave quantum processing unit to optimize the buses' routes in real-time. To our knowledge, this is the first commercial application that depends on a quantum processor to perform a critical live task.

quant-ph

Transversal ultrasound light guiding deep into scattering media

Biomedical applications requiring tissue diagnosis, activation, and treatment could be substantially leveraged by optical methods, owing to their unique feature set. However, their widespread application is severely limited by the strong light scattering that occurs in many tissues of interest, which dramatically limits achievable penetration depths. Here we demonstrate a new method to solve this issue by utilizing free-running ultrasound waves, transversal to the light propagation direction, to guide light into deeper tissue regions. We study the formation of the ultrasound-induced refractive index structures and waveguides using simple ultrasound field configurations and analyze their effects on the propagation of short light pulses. Our results show waveguide support and associated light intensity increase up to the depths of at least 20 mm in Intralipid-20% phantoms with a reduced scattering coeffcient close to real tissue. Thus we present an important milestone towards low-loss light delivery, focusing and manipulation in deep tissue.

physics.optics

Analysis of Logarithmic Amortised Complexity

We introduce a novel amortised resource analysis based on a potential-based type system. This type system gives rise to logarithmic and polynomial bounds on the runtime complexity and is the first such system to exhibit logarithmic amortised complexity. We relate the thus obtained automatable amortised resource analysis to manual amortised analyses of self-adjusting data structures, like splay trees, that can be found in the literature.

cs.PL

Linear Tree Constraints

Linear tree constraints were introduced by Hofmann and Rodriguez in the context of amortized resource analysis for object oriented programs. More precisely, they gave a reduction from inference of resource types to constraint solving. Thus, once we have found an algorithm to solve the constraints generated from a program, we can read off the resource consumption from their solutions. These constraints have the form of pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. We are interested in the question if a system of such constraints is simultaneously satisfiable. Bauer and Hofmann have recently identified a fragment of the tree constraint problem (UTC) that is still sufficient for program analysis and they proved that the list case of UTC is decidable, whereas the case with trees of degree at least two remained open. In this paper, we solve this problem. We give a decision procedure that covers the entire range of constraints needed for resource analysis.

cs.LO

Enforcing Programming Guidelines with Region Types and Effects

We present in this paper a new type and effect system for Java which can be used to ensure adherence to guidelines for secure web programming. The system is based on the region and effect system by Beringer, Grabowski, and Hofmann. It improves upon it by being parametrized over an arbitrary guideline supplied in the form of a finite monoid or automaton and a type annotation or mockup code for external methods. Furthermore, we add a powerful type inference based on precise interprocedural analysis and provide an implementation in the Soot framework which has been tested on a number of benchmarks including large parts of the Stanford SecuriBench.

cs.PL

Artificial Intelligence and Data Science in the Automotive Industry

Data science and machine learning are the key technologies when it comes to the processes and products with automatic learning and optimization to be used in the automotive industry of the future. This article defines the terms "data science" (also referred to as "data analytics") and "machine learning" and how they are related. In addition, it defines the term "optimizing analytics" and illustrates the role of automatic optimization as a key technology in combination with data analytics. It also uses examples to explain the way that these technologies are currently being used in the automotive industry on the basis of the major subprocesses in the automotive value chain (development, procurement; logistics, production, marketing, sales and after-sales, connected customer). Since the industry is just starting to explore the broad range of potential uses for these technologies, visionary application examples are used to illustrate the revolutionary possibilities that they offer. Finally, the article demonstrates how these technologies can make the automotive industry more efficient and enhance its customer focus throughout all its operations and activities, extending from the product and its development process to the customers and their connection to the product.

cs.AI

Proof-Relevant Logical Relations for Name Generation

Pitts and Stark's $\nu$-calculus is a paradigmatic total language for studying the problem of contextual equivalence in higher-order languages with name generation. Models for the $\nu$-calculus that validate basic equivalences concerning names may be constructed using functor categories or nominal sets, with a dynamic allocation monad used to model computations that may allocate fresh names. If recursion is added to the language and one attempts to adapt the models from (nominal) sets to (nominal) domains, however, the direct-style construction of the allocation monad no longer works. This issue has previously been addressed by using a monad that combines dynamic allocation with continuations, at some cost to abstraction. This paper presents a direct-style model of a $\nu$-calculus-like language with recursion using the novel framework of proof-relevant logical relations, in which logical relations also contain objects (or proofs) demonstrating the equivalence of (the semantic counterparts of) programs. Apart from providing a fresh solution to an old problem, this work provides an accessible setting in which to introduce the use of proof-relevant logical relations, free of the additional complexities associated with their use for more sophisticated languages.

cs.LO

An implementation of Deflate in Coq

The widely-used compression format "Deflate" is defined in RFC 1951 and is based on prefix-free codings and backreferences. There are unclear points about the way these codings are specified, and several sources for confusion in the standard. We tried to fix this problem by giving a rigorous mathematical specification, which we formalized in Coq. We produced a verified implementation in Coq which achieves competitive performance on inputs of several megabytes. In this paper we present the several parts of our implementation: a fully verified implementation of canonical prefix-free codings, which can be used in other compression formats as well, and an elegant formalism for specifying sophisticated formats, which we used to implement both a compression and decompression algorithm in Coq which we formally prove inverse to each other -- the first time this has been achieved to our knowledge. The compatibility to other Deflate implementations can be shown empirically. We furthermore discuss some of the difficulties, specifically regarding memory and runtime requirements, and our approaches to overcome them.

cs.LO

Effect-Dependent Transformations for Concurrent Programs

We describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent programming language. We prove the soundness of a number of general effect-based program equivalences, including a parallelization equation that specifies sufficient conditions for replacing sequential composition with parallel composition. Effect annotations are relative to abstract locations specified by contracts rather than physical footprints allowing us in particular to show the soundness of some transformations involving fine-grained concurrent data structures, such as Michael-Scott queues, that allow concurrent access to different parts of mutable data structures. Our semantics is based on refining a trace-based semantics for first-order programs due to Brookes. By moving from concrete to abstract locations, and adding type refinements that capture the possible side-effects of both expressions and their concurrent environments, we are able to validate many equivalences that do not hold in an unrefined model. The meanings of types are expressed using a game-based logical relation over sets of traces. Two programs $e_1$ and $e_2$ are logically related if one is able to solve a two-player game: for any trace with result value $v_1$ in the semantics of $e_1$ (challenge) that the player presents, the opponent can present an (response) equivalent trace in the semantics of $e_2$ with a logically related result value $v_2$.

cs.PL

Max-stable processes and the functional D-norm revisited

Aulbach et al. (2013) introduced a max-domain of attraction approach for extreme value theory in C[0,1] based on functional distribution functions, which is more general than the approach based on weak convergence in de Haan and Lin (2001). We characterize this new approach by decomposing a process into its univariate margins and its copula process. In particular, those processes with a polynomial rate of convergence towards a max-stable process are considered. Furthermore we investigate the concept of differentiability in distribution of a max-stable processes.

math.PR

On generalized max-linear models and their statistical interpolation

We propose a way how to generate a max-stable process in $C[0,1]$ from a max-stable random vector in $\mathbb R^d$ by generalizing the \emph{max-linear model} established by \citet{wansto11}. It turns out that if the random vector follows some finite dimensional distribution of some initial max-stable process, the approximating processes converge uniformly to the original process and the pointwise mean squared error can be represented in a closed form. The obtained results carry over to the case of generalized Pareto processes. The introduced method enables the reconstruction of the initial process only from a finite set of observation points and, thus, reasonable prediction of max-stable processes in space becomes possible. A possible extension to arbitrary dimension is outlined.

math.PR

Analytical characterization of the genuine multiparticle negativity

The genuine multiparticle negativity is a measure of genuine multiparticle entanglement which can be computed numerically. We present several results how this entanglement measure can be characterized analytically. First, we show that with an appropriate normalization this measure can be seen as coming from a mixed convex roof construction. Based on this, we determine its value for $n$-qubit GHZ-diagonal states and four-qubit cluster-diagonal states.

quant-ph

Scaling of genuine multiparticle entanglement at a quantum phase transition

We investigate the scaling and spatial distribution of genuine multiparticle entanglement in three- and four-spin reduced states of the one-dimensional XY-model at the quantum phase transition. We observe a logarithmic divergence and show that genuine three- and four-particle entanglement obeys finite-size scaling.

quant-ph

Amortised Resource Analysis and Typed Polynomial Interpretations (extended version)

We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be well-typed, then there exists a polynomial interpretation that orients R. For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.

cs.LO

Büchi Types for Infinite Traces and Liveness

We develop a new type and effect system based on Büchi automata to capture finite and infinite traces produced by programs in a small language which allows non-deterministic choices and infinite recursions. There are two key technical contributions: (a) an abstraction based on equivalence relations defined by the policy Büchi automaton, the Büchi abstraction; (b) a novel type and effect system to correctly capture infinite traces. We show how the Büchi abstraction fits into the abstract interpretation framework and show soundness and completeness.

cs.LO