اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدTemplates and Recurrences: Better Together
66
0
0.0
(
0
)
تأليف
Jason Breck
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. A template-based method begins with a template that contains unknown quantities, and finds invariants that match the template by extracting and solving constraints on the unknowns. A disadvantage of template-based methods is that they require fixing the set of terms that may appear in an invariant in advance. This disadvantage is particularly prominent for non-linear invariant generation, because the user must supply maximum degrees on polynomials, bases for exponents, etc. On the other hand, recurrence-based methods are able to find sophisticated non-linear mathematical relations, including polynomials, exponentials, and logarithms, because such relations arise as the solutions to recurrences. However, a disadvantage of past recurrence-based invariant-generation methods is that they are primarily loop-based analyses: they use recurrences to relate the pre-state and post-state of a loop, so it is not obvious how to apply them to a recursive procedure, especially if the procedure is non-linearly recursive (e.g., a tree-traversal algorithm). In this paper, we combine these two approaches and obtain a technique that uses templates in which the unknowns are functions rather than numbers, and the constraints on the unknowns are recurrences. The technique synthesizes invariants involving polynomials, exponentials, and logarithms, even in the presence of arbitrary control-flow, including any combination of loops, branches, and (possibly non-linear) recursion. For instance, it is able to show that (i) the time taken by merge-sort is $O(n log(n))$, and (ii) the time taken by Strassens algorithm is $O(n^{log_2(7)})$.
قيم البحث
اقرأ أيضاً
In modern applications, statisticians are faced with integrating heterogeneous data modalities relevant for an inference, prediction, or decision problem. In such circumstances, it is convenient to use a graphical model to represent the statistical d
ependencies, via a set of connected modules, each relating to a specific data modality, and drawing on specific domain expertise in their development. In principle, given data, the conventional statistical update then allows for coherent uncertainty quantification and information propagation through and across the modules. However, misspecification of any module can contaminate the estimate and update of others, often in unpredictable ways. In various settings, particularly when certain modules are trusted more than others, practitioners have preferred to avoid learning with the full model in favor of approaches that restrict the information propagation between modules, for example by restricting propagation to only particular directions along the edges of the graph. In this article, we investigate why these modular approaches might be preferable to the full model in misspecified settings. We propose principled criteria to choose between modular and full-model approaches. The question arises in many applied settings, including large stochastic dynamical systems, meta-analysis, epidemiological models, air pollution models, pharmacokinetics-pharmacodynamics, and causal inference with propensity scores.
Consider a cost-sharing game with players of different contribution to the total cost: an example might be an insurance company calculating premiums for a population of mixed-risk individuals. Two natural and competing notions of fairness might be to
a) charge each individual the same price or b) charge each individual according to the cost that they bring to the pool. In the insurance literature, these general approaches are referred to as solidarity and actuarial fairness and are commonly viewed as opposites. However, in insurance (and many other natural settings), the cost-sharing game also exhibits externalities of size: all else being equal, larger groups have lower average cost. In the insurance case, we analyze a model with externalities of size due to a reduction in the variability of losses. We explore how this complicates traditional understandings of fairness, drawing on literature in cooperative game theory. First, we explore solidarity: we show that it is possible for both groups (high and low risk) to strictly benefit by joining an insurance pool where costs are evenly split, as opposed to being in separate risk pools. We build on this by producing a pricing scheme that maximally subsidizes the high risk group, while maintaining an incentive for lower risk people to stay in the insurance pool. Next, we demonstrate that with this new model, the price charged to each individual has to depend on the risk of other participants, making naive actuarial fairness inefficient. Furthermore, we prove that stable pricing schemes must be ones where players have the anti-social incentive of desiring riskier partners, contradicting motivations for using actuarial fairness. Finally, we describe how these results relate to debates about fairness in machine learning and potential avenues for future research.
MOOC participants often feel isolated and disconnected from their peers. Navigating meaningful peer interactions, generating a sense of belonging, and achieving social presence are all major challenges for MOOC platforms. MOOC users often rely on ext
ernal social platforms for such connection and peer interaction, however, off-platform networking often distracts participants from their learning. With the intention of resolving this issue, we introduce PeerCollab, a web-based platform that provides affordances to create communities and supports meaningful peer interactions, building close-knit groups of learners. We present an initial evaluation through a field study (n=56) over 6 weeks and a controlled experiment (n=22). The result indicates insights on how learners build a sense of belonging and develop peer interactions leading to close-knit learning circles. We find that PeerCollab can provide more meaningful interactions and create a community to bring a culture of social learning to decentralized, and isolated MOOC learners.
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the users inte
nt. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows. We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)--(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.
We analyze the statistical properties of Poincare recurrences of Homo sapiens, mammalian and other DNA sequences taken from Ensembl Genome data base with up to fifteen billions base pairs. We show that the probability of Poincare recurrences decays i
n an algebraic way with the Poincare exponent $beta approx 4$ even if oscillatory dependence is well pronounced. The correlations between recurrences decay with an exponent $ u approx 0.6$ that leads to an anomalous super-diffusive walk. However, for Homo sapiens sequences, with the largest available statistics, the diffusion coefficient converges to a finite value on distances larger than million base pairs. We argue that the approach based on Poncare recurrences determines new proximity features between different species and shed a new light on their evolution history.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
