Hybrid logic is a modal logic with additional operators specifying nominals and is highly expressive. For example, there is no formula corresponding to the irreflexivity of Kripke frames in basic modal logic, but there is in hybrid logic. Irreflexivity is significant in that irreflexive and symmetric Kripke frames can be regarded as undirected graphs reviewed from a graph theoretic point of view. Thus, the study of the hybrid logic with axioms corresponding to irreflexivity and symmetry can help to elucidate the logical properties of undirected graphs. In this paper, we formulate the tableau method of the hybrid logic for undirected graphs. Our main result is to show the completeness theorem and the termination property of the tableau method, which leads us to prove the decidability.
相關內容
We describe a new algorithm to compute Whitney stratifications of real and complex algebraic varieties. This algorithm is a modification of the algorithm of Helmer and Nanda (HN), but is made more efficient by using techniques for equidimensional decomposition rather than computing the set of associated primes of a polynomial ideal at a key step in the HN algorithm. We note that this modified algorithm may fail to produce a minimal Whitney stratification even when the HN algorithm would produce a minimal stratification. We, additionally, present an algorithm to coarsen any Whitney stratification of a complex variety to a minimal Whitney stratification; the theoretical basis for our approach is a classical result of Teissier.
Probabilistic Hoare logic (PHL) is an extension of Hoare logic and is specifically useful in verifying randomized programs. It allows researchers to formally reason about the behavior of programs with stochastic elements, ensuring the desired probabilistic properties are upheld. The relative completeness of satisfaction-based PHL has been an open problem ever since the birth of the first PHL in 1979. More specifically, no satisfaction-based PHL with While-loop has been proven to be relatively complete yet. This paper solves this problem by establishing a new PHL with While-loop and prove its relative completeness. The programming language concerned in our PHL is expressively equivalent to the existing PHL systems but brings a lot of convenience in showing completeness. The weakest preterm for While-loop command reveals how it changes the probabilistic properties of computer states, considering both execution branches that halt and infinite runs. We prove the relative completeness of our PHL in two steps. We first establish a semantics and proof system of Hoare triples with probabilistic programs and deterministic assertions. Then, by utilizing the weakest precondition of deterministic assertions, we construct the weakest preterm calculus of probabilistic expressions. The relative completeness of our PHL is then obtained as a consequence of the weakest preterm calculus.
We propose a novel nonparametric Bayesian approach for meta-analysis with event time outcomes. The model is an extension of linear dependent tail-free processes. The extension includes a modification to facilitate (conditionally) conjugate posterior updating and a hierarchical extension with a random partition of studies. The partition is formalized as a Dirichlet process mixture. The model development is motivated by a meta-analysis of cancer immunotherapy studies. The aim is to validate the use of relevant biomarkers in the design of immunotherapy studies. The hypothesis is about immunotherapy in general, rather than about a specific tumor type, therapy and marker. This broad hypothesis leads to a very diverse set of studies being included in the analysis and gives rise to substantial heterogeneity across studies
Evolutionary multitasking (EMT) is an emerging approach for solving multitask optimization problems (MTOPs) and has garnered considerable research interest. The implicit EMT is a significant research branch that utilizes evolution operators to enable knowledge transfer (KT) between tasks. However, current approaches in implicit EMT face challenges in adaptability, due to the use of a limited number of evolution operators and insufficient utilization of evolutionary states for performing KT. This results in suboptimal exploitation of implicit KT's potential to tackle a variety of MTOPs. To overcome these limitations, we propose a novel Learning to Transfer (L2T) framework to automatically discover efficient KT policies for the MTOPs at hand. Our framework conceptualizes the KT process as a learning agent's sequence of strategic decisions within the EMT process. We propose an action formulation for deciding when and how to transfer, a state representation with informative features of evolution states, a reward formulation concerning convergence and transfer efficiency gain, and the environment for the agent to interact with MTOPs. We employ an actor-critic network structure for the agent and learn it via proximal policy optimization. This learned agent can be integrated with various evolutionary algorithms, enhancing their ability to address a range of new MTOPs. Comprehensive empirical studies on both synthetic and real-world MTOPs, encompassing diverse inter-task relationships, function classes, and task distributions are conducted to validate the proposed L2T framework. The results show a marked improvement in the adaptability and performance of implicit EMT when solving a wide spectrum of unseen MTOPs.
A key challenge of quantum programming is uncomputation: the reversible deallocation of qubits. And while there has been much recent progress on automating uncomputation, state-of-the-art methods are insufficient for handling today's expressive quantum programming languages. A core reason is that they operate on primitive quantum circuits, while quantum programs express computations beyond circuits, for instance, they can capture families of circuits defined recursively in terms of uncomputation and adjoints. In this paper, we introduce the first modular automatic approach to synthesize correct and efficient uncomputation for expressive quantum programs. Our method is based on two core technical contributions: (i) an intermediate representation (IR) that can capture expressive quantum programs and comes with support for uncomputation, and (ii) modular algorithms over that IR for synthesizing uncomputation and adjoints. We have built a complete end-to-end implementation of our method, including an implementation of the IR and the synthesis algorithms, as well as a translation from an expressive fragment of the Silq programming language to our IR and circuit generation from the IR. Our experimental evaluation demonstrates that we can handle programs beyond the capabilities of existing uncomputation approaches, while being competitive on the benchmarks they can handle. More broadly, we show that it is possible to benefit from the greater expressivity and safety offered by high-level quantum languages without sacrificing efficiency.
Quantum computing and modern tensor-based computing have a strong connection, which is especially demonstrated by simulating quantum computations with tensor networks. The other direction is less studied: quantum computing is not often applied to tensor-based problems. Considering tensor decompositions, we focus on discovering practical matrix multiplication algorithms and develop two algorithms to compute decompositions on quantum computers. The algorithms are expressed as higher-order unconstrained binary optimization (HUBO) problems, which are translated into quadratic unconstrained binary optimization (QUBO) problems. Our first algorithm is decompositional to keep the optimization problem feasible for the current quantum devices. Starting from a suitable initial point, the algorithm discovers tensor decomposition corresponding to the famous Strassen matrix multiplication algorithm, utilizing the current quantum annealers. Since the decompositional algorithm does not guarantee minimal length for found tensor decompositions, we develop a holistic algorithm that can find fixed-length decompositions. Theoretically, by fixing a shorter length than the length for the best-known decomposition, we can ensure that the solution to the holistic optimization problem would yield faster matrix multiplication algorithms.
Reshaping, a point operation that alters the characteristics of signals, has been shown capable of improving the compression ratio in video coding practices. Out-of-loop reshaping that directly modifies the input video signal was first adopted as the supplemental enhancement information (SEI) for the HEVC/H.265 without the need to alter the core design of the video codec. VVC/H.266 further improves the coding efficiency by adopting in-loop reshaping that modifies the residual signal being processed in the hybrid coding loop. In this paper, we theoretically analyze the rate-distortion performance of the in-loop reshaping and use experiments to verify the theoretical result. We prove that the in-loop reshaping can improve coding efficiency when the entropy coder adopted in the coding pipeline is suboptimal, which is in line with the practical scenarios that video codecs operate in. We derive the PSNR gain in a closed form and show that the theoretically predicted gain is consistent with that measured from experiments using standard testing video sequences.
Tensor network contractions are widely used in statistical physics, quantum computing, and computer science. We introduce a method to efficiently approximate tensor network contractions using low-rank approximations, where each intermediate tensor generated during the contractions is approximated as a low-rank binary tree tensor network. The proposed algorithm has the flexibility to incorporate a large portion of the environment when performing low-rank approximations, which can lead to high accuracy for a given rank. Here, the environment refers to the remaining set of tensors in the network, and low-rank approximations with larger environments can generally provide higher accuracy. For contracting tensor networks defined on lattices, the proposed algorithm can be viewed as a generalization of the standard boundary-based algorithms. In addition, the algorithm includes a cost-efficient density matrix algorithm for approximating a tensor network with a general graph structure into a tree structure, whose computational cost is asymptotically upper-bounded by that of the standard algorithm that uses canonicalization. Experimental results indicate that the proposed technique outperforms previously proposed approximate tensor network contraction algorithms for multiple problems in terms of both accuracy and efficiency.
Edge computing has recently emerged as a promising paradigm to boost the performance of distributed learning by leveraging the distributed resources at edge nodes. Architecturally, the introduction of edge nodes adds an additional intermediate layer between the master and workers in the original distributed learning systems, potentially leading to more severe straggler effect. Recently, coding theory-based approaches have been proposed for stragglers mitigation in distributed learning, but the majority focus on the conventional workers-master architecture. In this paper, along a different line, we investigate the problem of mitigating the straggler effect in hierarchical distributed learning systems with an additional layer composed of edge nodes. Technically, we first derive the fundamental trade-off between the computational loads of workers and the stragglers tolerance. Then, we propose a hierarchical gradient coding framework, which provides better stragglers mitigation, to achieve the derived computational trade-off. To further improve the performance of our framework in heterogeneous scenarios, we formulate an optimization problem with the objective of minimizing the expected execution time for each iteration in the learning process. We develop an efficient algorithm to mathematically solve the problem by outputting the optimum strategy. Extensive simulation results demonstrate the superiority of our schemes compared with conventional solutions.
As artificial intelligence (AI) models continue to scale up, they are becoming more capable and integrated into various forms of decision-making systems. For models involved in moral decision-making, also known as artificial moral agents (AMA), interpretability provides a way to trust and understand the agent's internal reasoning mechanisms for effective use and error correction. In this paper, we provide an overview of this rapidly-evolving sub-field of AI interpretability, introduce the concept of the Minimum Level of Interpretability (MLI) and recommend an MLI for various types of agents, to aid their safe deployment in real-world settings.
注冊地址： 北京市海淀區羊坊店路18號2幢3層301-191