Search

MLsub is a minimal language with a type system combining subtyping and parametric polymorphism and a type inference algorithm which infers compact principal types. Simple-sub is an alternative inference algorithm which can be implemented efficiently and is easier to understand. MLsub supports explicitly typed records which are not extensible. Here we extend Simple-sub with extensible records, meaning that we can add new fields to a previously defined record. For this we add row variables to our type language and extend the type constraint solving method of our type inference algorithm accordingly, keeping the decidability of type inference.

We provide an algorithm for deciding simple grammar bisimilarity whose complexity is polynomial in the valuation of the grammar (maximum seminorm among production rules). Since the valuation is at most exponential in the size of the grammar, this gives rise to a single-exponential running time. Previously only a doubly-exponential algorithm was known. As an application, we provide a conversion from context-free session types to simple grammars whose valuation is linear in the size of the type. In this way, we provide the first polynomial-time algorithm for deciding context-free session type equivalence., Comment: 37 pages, 6 figure

We present, for the first time, a novel theoretical approach to address the problem of correspondence free multivector cloud registration in conformal geometric algebra. Such formalism achieves several favorable properties. Primarily, it forms an orthogonal automorphism that extends beyond the typical vector space to the entire conformal geometric algebra while respecting the multivector grading. Concretely, the registration can be viewed as an orthogonal transformation (\it i.e., scale, translation, rotation) belonging to $SO(4,1)$ - group of special orthogonal transformations in conformal geometric algebra. We will show that such formalism is able to: $(i)$ perform the registration without directly accessing the input multivectors. Instead, we use primitives or geometric objects provided by the conformal model - the multivectors, $(ii)$ the geometric objects are obtained by solving a multilinear eigenvalue problem to find sets of eigenmultivectors. In this way, we can explicitly avoid solving the correspondences in the registration process. Most importantly, this offers rotation and translation equivariant properties between the input multivectors and the eigenmultivectors. Experimental evaluation is conducted in datasets commonly used in point cloud registration, to testify the usefulness of the approach with emphasis to ambiguities arising from high levels of noise. The code is available at https://github.com/Numerical-Geometric-Algebra/RegistrationGA . This work was submitted to the International Journal of Computer Vision and is currently under review.

Collecting the most informative data from a large dataset distributed over a network is a fundamental problem in many fields, including control, signal processing and machine learning. In this paper, we establish a connection between selecting the most informative data and finding the top-$k$ elements of a multiset. The top-$k$ selection in a network can be formulated as a distributed nonsmooth convex optimization problem known as quantile estimation. Unfortunately, the lack of smoothness in the local objective functions leads to extremely slow convergence and poor scalability with respect to the network size. To overcome the deficiency, we propose an accelerated method that employs smoothing techniques. Leveraging the piecewise linearity of the local objective functions in quantile estimation, we characterize the iteration complexity required to achieve top-$k$ selection, a challenging task due to the lack of strong convexity. Several numerical results are provided to validate the effectiveness of the algorithm and the correctness of the theory., Comment: Submitted to the IEEE Transactions on Automatic Control

We address the long-standing problem of how to learn effective pixel-based image diffusion models at scale, introducing a remarkably simple greedy growing method for stable training of large-scale, high-resolution models. without the needs for cascaded super-resolution components. The key insight stems from careful pre-training of core components, namely, those responsible for text-to-image alignment {\it vs.} high-resolution rendering. We first demonstrate the benefits of scaling a {\it Shallow UNet}, with no down(up)-sampling enc(dec)oder. Scaling its deep core layers is shown to improve alignment, object structure, and composition. Building on this core model, we propose a greedy algorithm that grows the architecture into high-resolution end-to-end models, while preserving the integrity of the pre-trained representation, stabilizing training, and reducing the need for large high-resolution datasets. This enables a single stage model capable of generating high-resolution images without the need of a super-resolution cascade. Our key results rely on public datasets and show that we are able to train non-cascaded models up to 8B parameters with no further regularization schemes. Vermeer, our full pipeline model trained with internal datasets to produce 1024x1024 images, without cascades, is preferred by 44.0% vs. 21.4% human evaluators over SDXL.

Protecting and restoring forest ecosystems is critical for biodiversity conservation and carbon sequestration. Forest monitoring on a global scale is essential for prioritizing and assessing conservation efforts. Satellite-based remote sensing is the only viable solution for providing global coverage, but to date, large-scale forest monitoring is limited to single modalities and single time points. In this paper, we present a dataset consisting of data from five public satellites for recognizing forest plantations and planted tree species across the globe. Each satellite modality consists of a multi-year time series. The dataset, named \PlantD, includes over 2M examples of 64 tree label classes (46 genera and 40 species), distributed among 41 countries. This dataset is released to foster research in forest monitoring using multimodal, multi-scale, multi-temporal data sources. Additionally, we present initial baseline results and evaluate modality fusion and data augmentation approaches for this dataset.

Many modern distributed systems consist of devices that generate more data than what can be transmitted via a communication link in near real time with high-fidelity. We consider the scheduling problem in which a device has access to multiple data sources, but at any moment, only one of them is revealed in real-time to a remote receiver. Even when the sources are Gaussian, and the fidelity criterion is the mean squared error, the globally optimal data selection strategy is not known. We propose a data-driven methodology to search for the elusive optimal solution using linear function approximation approach called neuroscheduling and establish necessary and sufficient conditions for the optimal scheduler to not over fit training data. Additionally, we present several numerical results that show that the globally optimal scheduler and estimator pair to the Gaussian case are nonlinear., Comment: Submitted for presentation at the 2024 Asilomar Conference on Signals, Systems, and Computers

In the recent years, the dual-encoder vision-language models (\eg CLIP) have achieved remarkable text-to-image retrieval performance. However, we discover that these models usually results in very different retrievals for a pair of paraphrased queries. Such behavior might render the retrieval system less predictable and lead to user frustration. In this work, we consider the task of paraphrased text-to-image retrieval where a model aims to return similar results given a pair of paraphrased queries. To start with, we collect a dataset of paraphrased image descriptions to facilitate quantitative evaluation for this task. We then hypothesize that the undesired behavior of existing dual-encoder model is due to their text towers which are trained on image-sentence pairs and lack the ability to capture the semantic similarity between paraphrased queries. To improve on this, we investigate multiple strategies for training a dual-encoder model starting from a language model pretrained on a large text corpus. Compared to public dual-encoder models such as CLIP and OpenCLIP, the model trained with our best adaptation strategy achieves a significantly higher ranking similarity for paraphrased queries while maintaining similar zero-shot classification and retrieval accuracy.

Diffusion models have made significant advances in text-guided synthesis tasks. However, editing user-provided images remains challenging, as the high dimensional noise input space of diffusion models is not naturally suited for image inversion or spatial editing. In this work, we propose an image representation that promotes spatial editing of input images using a diffusion model. Concretely, we learn to encode an input into "image elements" that can faithfully reconstruct an input image. These elements can be intuitively edited by a user, and are decoded by a diffusion model into realistic images. We show the effectiveness of our representation on various image editing tasks, such as object resizing, rearrangement, dragging, de-occlusion, removal, variation, and image composition. Project page: https://jitengmu.github.io/Editable_Image_Elements/, Comment: Project page: https://jitengmu.github.io/Editable_Image_Elements/

In surgical oncology, screening colonoscopy plays a pivotal role in providing diagnostic assistance, such as biopsy, and facilitating surgical navigation, particularly in polyp detection. Computer-assisted endoscopic surgery has recently gained attention and amalgamated various 3D computer vision techniques, including camera localization, depth estimation, surface reconstruction, etc. Neural Radiance Fields (NeRFs) and Neural Implicit Surfaces (NeuS) have emerged as promising methodologies for deriving accurate 3D surface models from sets of registered images, addressing the limitations of existing colon reconstruction approaches stemming from constrained camera movement. However, the inadequate tissue texture representation and confused scale problem in monocular colonoscopic image reconstruction still impede the progress of the final rendering results. In this paper, we introduce a novel method for colon section reconstruction by leveraging NeuS applied to endoscopic images, supplemented by a single frame of depth map. Notably, we pioneered the exploration of utilizing only one frame depth map in photorealistic reconstruction and neural rendering applications while this single depth map can be easily obtainable from other monocular depth estimation networks with an object scale. Through rigorous experimentation and validation on phantom imagery, our approach demonstrates exceptional accuracy in completely rendering colon sections, even capturing unseen portions of the surface. This breakthrough opens avenues for achieving stable and consistently scaled reconstructions, promising enhanced quality in cancer screening procedures and treatment interventions.

This paper introduces a novel pipeline designed to bring ultrasound (US) plane pose estimation closer to clinical use for more effective navigation to the standard planes (SPs) in the fetal brain. We propose a semi-supervised segmentation model utilizing both labeled SPs and unlabeled 3D US volume slices. Our model enables reliable segmentation across a diverse set of fetal brain images. Furthermore, the model incorporates a classification mechanism to identify the fetal brain precisely. Our model not only filters out frames lacking the brain but also generates masks for those containing it, enhancing the relevance of plane pose regression in clinical settings. We focus on fetal brain navigation from 2D ultrasound (US) video analysis and combine this model with a US plane pose regression network to provide sensorless proximity detection to SPs and non-SPs planes; we emphasize the importance of proximity detection to SPs for guiding sonographers, offering a substantial advantage over traditional methods by allowing earlier and more precise adjustments during scanning. We demonstrate the practical applicability of our approach through validation on real fetal scan videos obtained from sonographers of varying expertise levels. Our findings demonstrate the potential of our approach to complement existing fetal US technologies and advance prenatal diagnostic practices., Comment: 11 pages, 5 figures

This paper presents the methodology and key results which enabled to establish the so-called Ancillary Service Matrix (ASM) presenting the ability to deliver the different ancillary services of each of the 6 demonstrators of the XFLEX HYDRO research project combined with the applicable technologies studied in this analysis. These technologies include i) the variable speed technology with Doubly Fed Induction Machine (DFIM) or Full Size Frequency Converters (FSFC), ii) the Smart Power Plant Supervisor (SPPS) enabling to extend the operating range of the hydraulic units in turbine mode based on a better knowledge of the hydro unit wear and tear and associated costs over the full unit operating range, iii) the hydraulic short circuit (HSC) operation leading to simultaneous operation of pump and turbines of Pumped Storage Power Plants (PSPP) and iv) the Hydro-Battery-Hybrid (HBH) applied at Run-of-River demonstrator. The demonstrators considered for this study includes 4 pumped storage power plants, 1 conventional hydro storage plant and 1 run-of-the-river plant. For each demonstrator a 1D simulation model was developed and validated and was further enhanced to include the model of control system enabling to address the various ancillary services. The systematic 1D numerical simulation of ancillary service contribution of each demonstrator and related technologies enabled to quantify the magnitude of active power response to contribute to the different grid services. The results have been scored between 0 and 5 for each ancillary service, allowing to populate the Ancillary Service Matrix which is summarizing the results in a graphical and synthetic way. The analysis of the score of the Ancillary Services Matrix enables the reader to draw several key conclusions about the benefits unlocked by the implementation of these technologies which are summarized in the paper., Comment: 25 pages, Proceedings of HYDRO 2023, International Conference, October 16-18, 2023, Edinburgh, Scotland

Within colorectal cancer diagnostics, conventional colonoscopy techniques face critical limitations, including a limited field of view and a lack of depth information, which can impede the detection of precancerous lesions. Current methods struggle to provide comprehensive and accurate 3D reconstructions of the colonic surface which can help minimize the missing regions and reinspection for pre-cancerous polyps. Addressing this, we introduce 'Gaussian Pancakes', a method that leverages 3D Gaussian Splatting (3D GS) combined with a Recurrent Neural Network-based Simultaneous Localization and Mapping (RNNSLAM) system. By introducing geometric and depth regularization into the 3D GS framework, our approach ensures more accurate alignment of Gaussians with the colon surface, resulting in smoother 3D reconstructions with novel viewing of detailed textures and structures. Evaluations across three diverse datasets show that Gaussian Pancakes enhances novel view synthesis quality, surpassing current leading methods with a 18% boost in PSNR and a 16% improvement in SSIM. It also delivers over 100X faster rendering and more than 10X shorter training times, making it a practical tool for real-time applications. Hence, this holds promise for achieving clinical translation for better detection and diagnosis of colorectal cancer., Comment: 12 pages, 5 figures

We explore the integration of metaprogramming in a call-by-value linear lambda-calculus and sketch its extension to a session type system. We build on a model of contextual modal type theory with multi-level contexts, where contextual values, closing arbitrary terms over a series of variables, may then be boxed and transmitted in messages. Once received, one such value may then be unboxed (with a let-box construct) and locally applied before being run. We present a series of examples where servers prepare and ship code on demand via session typed messages., Comment: In Proceedings PLACES 2024, arXiv:2404.03712

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing., Comment: In Proceedings PLACES 2024, arXiv:2404.03712

Anomaly detection (AD) aims to identify defective images and localize their defects (if any). Ideally, AD models should be able to detect defects over many image classes; without relying on hard-coded class names that can be uninformative or inconsistent across datasets; learn without anomaly supervision; and be robust to the long-tailed distributions of real-world applications. To address these challenges, we formulate the problem of long-tailed AD by introducing several datasets with different levels of class imbalance and metrics for performance evaluation. We then propose a novel method, LTAD, to detect defects from multiple and long-tailed classes, without relying on dataset class names. LTAD combines AD by reconstruction and semantic AD modules. AD by reconstruction is implemented with a transformer-based reconstruction module. Semantic AD is implemented with a binary classifier, which relies on learned pseudo class names and a pretrained foundation model. These modules are learned over two phases. Phase 1 learns the pseudo-class names and a variational autoencoder (VAE) for feature synthesis that augments the training data to combat long-tails. Phase 2 then learns the parameters of the reconstruction and classification modules of LTAD. Extensive experiments using the proposed long-tailed datasets show that LTAD substantially outperforms the state-of-the-art methods for most forms of dataset imbalance. The long-tailed dataset split is available at https://zenodo.org/records/10854201 ., Comment: This paper is accepted to CVPR 2024. The supplementary material is included. The long-tailed dataset split is available at https://zenodo.org/records/10854201

We present an extension-based approach for computing and verifying preferences in an abstract argumentation system. Although numerous argumentation semantics have been developed previously for identifying acceptable sets of arguments from an argumentation framework, there is a lack of justification behind their acceptability based on implicit argument preferences. Preference-based argumentation frameworks allow one to determine what arguments are justified given a set of preferences. Our research considers the inverse of the standard reasoning problem, i.e., given an abstract argumentation framework and a set of justified arguments, we compute what the possible preferences over arguments are. Furthermore, there is a need to verify (i.e., assess) that the computed preferences would lead to the acceptable sets of arguments. This paper presents a novel approach and algorithm for exhaustively computing and enumerating all possible sets of preferences (restricted to three identified cases) for a conflict-free set of arguments in an abstract argumentation framework. We prove the soundness, completeness and termination of the algorithm. The research establishes that preferences are determined using an extension-based approach after the evaluation phase (acceptability of arguments) rather than stated beforehand. In this work, we focus our research study on grounded, preferred and stable semantics. We show that the complexity of computing sets of preferences is exponential in the number of arguments, and thus, describe an approximate approach and algorithm to compute the preferences. Furthermore, we present novel algorithms for verifying (i.e., assessing) the computed preferences. We provide details of the implementation of the algorithms (source code has been made available), various experiments performed to evaluate the algorithms and the analysis of the results.

Many socioeconomic phenomena, such as technology adoption, collaborative problem-solving, and content engagement, involve a collection of agents coordinating to take a common action, aligning their decisions to maximize their individual goals. We consider a model for networked interactions where agents learn to coordinate their binary actions under a strict bound on their rationality. We first prove that our model is a potential game and that the optimal action profile is always to achieve perfect alignment at one of the two possible actions, regardless of the network structure. Using a stochastic learning algorithm known as Log Linear Learning, where agents have the same finite rationality parameter, we show that the probability of agents successfully agreeing on the correct decision is monotonically increasing in the number of network links. Therefore, more connectivity improves the accuracy of collective decision-making, as predicted by the phenomenon known as Wisdom of Crowds. Finally, we show that for a fixed number of links, a regular network maximizes the probability of success. We conclude that when using a network of irrational agents, promoting more homogeneous connectivity improves the accuracy of collective decision-making., Comment: Submitted to 2024 IEEE Conference on Decision and Control

Feature point detection and description is the backbone for various computer vision applications, such as Structure-from-Motion, visual SLAM, and visual place recognition. While learning-based methods have surpassed traditional handcrafted techniques, their training often relies on simplistic homography-based simulations of multi-view perspectives, limiting model generalisability. This paper introduces a novel approach leveraging neural radiance fields (NeRFs) for realistic multi-view training data generation. We create a diverse multi-view dataset using NeRFs, consisting of indoor and outdoor scenes. Our proposed methodology adapts state-of-the-art feature detectors and descriptors to train on NeRF-synthesised views supervised by perspective projective geometry. Our experiments demonstrate that the proposed methods achieve competitive or superior performance on standard benchmarks for relative pose estimation, point cloud registration, and homography estimation while requiring significantly less training data compared to existing approaches.

The interplay between criminal organizations and law enforcement disruption strategies is crucial in criminology. Criminal enterprises, like legitimate businesses, balance visibility and security to thrive. This study uses evolutionary game theory to analyze criminal networks' dynamics, resilience to interventions, and responses to external conditions. We find strong hysteresis effects, challenging traditional deterrence-focused strategies. Optimal thresholds for organization formation or dissolution are defined by these effects. Stricter punishment doesn't always deter organized crime linearly. Network structure, particularly link density and skill assortativity, significantly influences organization formation and stability. These insights advocate for adaptive policy-making and strategic law enforcement to effectively disrupt criminal networks.

Policymaking for complex challenges such as pandemics necessitates the consideration of intricate implications across multiple domains and scales. Computational models can support policymaking, but a single model is often insufficient for such multidomain and scale challenges. Multi-models comprising several interacting computational models at different scales or relying on different modeling paradigms offer a potential solution. Such multi-models can be assembled from existing computational models (i.e., integrated modeling) or be designed conceptually as a whole before their computational implementation (i.e., integral modeling). Integral modeling is particularly valuable for novel policy problems, such as those faced in the early stages of a pandemic, where relevant models may be unavailable or lack standard documentation. Designing such multi-models through an integral approach is, however, a complex task requiring the collaboration of modelers and experts from various domains. In this collaborative effort, modelers must precisely define the domain knowledge needed from experts and establish a systematic procedure for translating such knowledge into a multi-model. Yet, these requirements and systematic procedures are currently lacking for multi-models that are both multiscale and multi-paradigm. We address this challenge by introducing a procedure for developing multi-models with an integral approach based on clearly defined domain knowledge requirements derived from literature. We illustrate this procedure using the case of school closure policies in the Netherlands during the COVID-19 pandemic, revealing their potential implications in the short and long term and across the healthcare and educational domains. The requirements and procedure provided in this article advance the application of integral multi-modeling for policy support in multiscale and multidomain contexts.

Artificial intelligence (AI) has driven many information and communication technology (ICT) breakthroughs. Nonetheless, the scope of ICT systems has expanded far beyond AI since the Turing test proposal. Critically, recent AI regulation proposals adopt AI definitions affecting ICT techniques, approaches, and systems that are not AI. In some cases, even works from mathematics, statistics, and engineering would be affected. Worryingly, AI misdefinitions are observed from Western societies to the Global South. In this paper, we propose a framework to score how validated as appropriately-defined for regulation (VADER) an AI definition is. Our online, publicly-available VADER framework scores the coverage of premises that should underlie AI definitions for regulation, which aim to (i) reproduce principles observed in other successful technology regulations, and (ii) include all AI techniques and approaches while excluding non-AI works. Regarding the latter, our score is based on a dataset of representative AI, non-AI ICT, and non-ICT examples. We demonstrate our contribution by reviewing the AI regulation proposals of key players, namely the United States, United Kingdom, European Union, and Brazil. Importantly, none of the proposals assessed achieve the appropriateness score, ranging from a revision need to a concrete risk to ICT systems and works from other fields.

Most of the existing diffusion models use Gaussian noise for training and sampling across all time steps, which may not optimally account for the frequency contents reconstructed by the denoising network. Despite the diverse applications of correlated noise in computer graphics, its potential for improving the training process has been underexplored. In this paper, we introduce a novel and general class of diffusion models taking correlated noise within and across images into account. More specifically, we propose a time-varying noise model to incorporate correlated noise into the training process, as well as a method for fast generation of correlated noise mask. Our model is built upon deterministic diffusion models and utilizes blue noise to help improve the generation quality compared to using Gaussian white (random) noise only. Further, our framework allows introducing correlation across images within a single mini-batch to improve gradient flow. We perform both qualitative and quantitative evaluations on a variety of datasets using our method, achieving improvements on different tasks over existing deterministic diffusion models in terms of FID metric., Comment: SIGGRAPH 2024 Conference Proceedings; Project page: https://xchhuang.github.io/bndm

In supervised learning, models are trained to extract correlations from a static dataset. This often leads to models that rely on high-level misconceptions. To prevent such misconceptions, we must necessarily provide additional information beyond the training data. Existing methods incorporate forms of additional instance-level supervision, such as labels for spurious features or additional labeled data from a balanced distribution. Such strategies can become prohibitively costly for large-scale datasets since they require additional annotation at a scale close to the original training data. We hypothesize that targeted natural language feedback about a model's misconceptions is a more efficient form of additional supervision. We introduce Clarify, a novel interface and method for interactively correcting model misconceptions. Through Clarify, users need only provide a short text description to describe a model's consistent failure patterns. Then, in an entirely automated way, we use such descriptions to improve the training process by reweighting the training data or gathering additional targeted data. Our user studies show that non-expert users can successfully describe model misconceptions via Clarify, improving worst-group accuracy by an average of 17.1% in two datasets. Additionally, we use Clarify to find and rectify 31 novel hard subpopulations in the ImageNet dataset, improving minority-split accuracy from 21.1% to 28.7%.

We investigate the generation of an entangled electron pair emerging from a system composed of two quantum dots attached to a superconductor Cooper pair beam splitter. We take into account three processes: Crossed Andreev Reflection, cotuneling, and Coulomb interaction. Together, these processes play crucial roles in the formation of entangled electronic states, with electrons being in spatially separated quantum dots. By using perturbation theory, we derive an analytical effective model that allows a simple picture of the intricate process behind the formation of the entangled state. Several entanglement quantifiers, including quantum mutual information, negativity, and concurrence, are employed to validate our findings. Finally, we define and calculate the covariance associated with the detection of two electrons, each originating from one of the quantum dots with a specific spin value. The time evolution of this observable follows the dynamics of all entanglement quantifiers, thus suggesting that it can be a useful tool for mapping the creation of entangled electrons in future applications within quantum information protocols., Comment: To be published in Physical Review A

Crowd counting is an important problem in computer vision due to its wide range of applications in image understanding. Currently, this problem is typically addressed using deep learning approaches, such as Convolutional Neural Networks (CNNs) and Transformers. However, deep networks are data-driven and are prone to overfitting, especially when the available labeled crowd dataset is limited. To overcome this limitation, we have designed a pipeline that utilizes a diffusion model to generate extensive training data. We are the first to generate images conditioned on a location dot map (a binary dot map that specifies the location of human heads) with a diffusion model. We are also the first to use these diverse synthetic data to augment the crowd counting models. Our proposed smoothed density map input for ControlNet significantly improves ControlNet's performance in generating crowds in the correct locations. Also, Our proposed counting loss for the diffusion model effectively minimizes the discrepancies between the location dot map and the crowd images generated. Additionally, our innovative guidance sampling further directs the diffusion process toward regions where the generated crowd images align most accurately with the location dot map. Collectively, we have enhanced ControlNet's ability to generate specified objects from a location dot map, which can be used for data augmentation in various counting problems. Moreover, our framework is versatile and can be easily adapted to all kinds of counting problems. Extensive experiments demonstrate that our framework improves the counting performance on the ShanghaiTech, NWPU-Crowd, UCF-QNRF, and TRANCOS datasets, showcasing its effectiveness.