One standard way to prove existence for deterministic, highly nonlinear PDEs is to use the Schauder-Tychonoff fixed-point theorem. In what follows, we introduce and verify a stochastic variant of the Schauder-Tychonoff theorem. We apply our existence result to nonlinear stochastic diffusion equations with non-Lipschitz perturbations

In this study, we investigate the incompressible generalised Navier-Stokes-Voigt equations within a bounded domain Ω⊂ℝ^d, where d ≥ 2. The governing momentum equation is expressed as: ∂_t(v - κΔv) + ∇· (v⊗v) + ∇ π- ν∇·( |𝐃(v)|^p-2𝐃(v) ) = f. Here, for d ∈{2,3}, v represents the velocity field, π denotes the pressure, and f is the external forcing term. The constants κ and ν correspond to the relaxation time and kinematic viscosity, respectively. The parameter p ∈ (1, ∞) characterizes the fluid's flow behavior, and 𝐃(v) denotes the symmetric part of the velocity gradient ∇v. For the power-law exponent p ∈( 2d/d+2, ∞), we establish the existence of a weak solution to the generalised Navier-Stokes-Voigt equations. Furthermore, we demonstrate that the weak solution is unique for the same range of the exponent p. The optimality of our results lies in the framework's use of a Gelfand triple, which allows the Aubin-Dubinskii lemma to yield strong convergence of approximate solutions, essential for existence and valid precisely for p > 2d/d+2.

In this work, we investigate the Central Limit Theorem (CLT) and Moderate Deviation Principle (MDP) for the solution of a stochastic generalized Burgers-Huxley (SGBH) equation with multiplicative Gaussian noise. The SGBH equation is a diffusion-convection-reaction type equation which consists of a nonlinearity of polynomial order, and we take into account an infinite-dimensional noise having a coefficient that has linear growth. We first prove the CLT which allows us to establish the convergence of the distribution of the solution to a re-scaled SGBH equation to a desired distribution function. Furthermore, we extend our asymptotic analysis by investigating the MDP for the solution of SGBH equation. Using the weak convergence method, we establish the MDP and derive the corresponding rate function.

The main goal of this article is to study the effect of small, highly nonlinear, unbounded drifts (small time large deviation principle (LDP) based on exponential equivalence arguments) for a class of stochastic partial differential equations (SPDEs) with fully monotone coefficients driven by multiplicative Gaussian noise. The small time LDP obtained in this paper is applicable for various quasi-linear and semilinear SPDEs such as porous medium equations, Cahn-Hilliard equation, 2D Navier-Stokes equations, convection-diffusion equation, 2D liquid crystal model, power law fluids, Ladyzhenskaya model, p-Laplacian equations, etc., perturbed by multiplicative Gaussian noise.

In this work, we focus on the global solvability and uniform large deviations for the solutions of stochastic generalized Burgers-Huxley (SGBH) equation perturbed by a small multiplicative white in time and colored in space noise. The SGBH equation has the nonlinearity of polynomial order and noise considered in this work is infinite dimensional with a coefficient having linear growth. First, we prove the existence of a \textsl{unique local mild solution} in the sense of Walsh to SGBH equation with the help of a truncation argument and contraction mapping principle. Then the global solvability results are established by using uniform bounds of the local mild solution, stopping time arguments, tightness properties and Skorokhod's representation theorem. By using the uniform Laplace principle, we obtain the \textsl{large deviation principle} (LDP) for the law of solutions to SGBH equation by using variational representation methods. Further, we derive the \textsl{uniform large deviation principle} (ULDP) for the law of solutions in two different topologies by using a weak convergence method. First, in the $\mathrm{C}([0, T ];\mathrm{L}^p([0,1])) $ topology where the uniformity is over $\mathrm{L}^p([0,1])$-bounded sets of initial conditions, and secondly in the $\mathrm{C} ([0, T ] \times[0,1])$ topology with uniformity being over bounded subsets in the $\mathrm{C}([0,1])$-norm. Finally, we consider SGBH equation perturbed by a space-time white noise with bounded noise coefficient and establish the ULDP for the laws of solutions. The results obtained in this work hold true for stochastic Burgers' as well as Burgers-Huxley equations.

In this work, we consider the incompressible generalized Navier-Stokes-Voigt equations in a bounded domain 𝒪⊂ℝ^d , d≥ 2 , driven by a multiplicative Gaussian noise. The considered momentum equation is given by: d( u - κΔu) = [ f +div( -πI+ν |D(u)|^p-2D(u)-u⊗u) ] d t + Φ (u)dW(t). In the case of d=2,3 , u accounts for the velocity field, π is the pressure, f is a body force and the final term represents the stochastic forces. Here, κ and ν are given positive constants that account for the kinematic viscosity and relaxation time, and the power-law index p is another constant (assumed p>1 ) that characterizes the flow. We use the usual notation I for the unit tensor and D(u):=1/2( ∇u + (∇u)^⊤) for the symmetric part of velocity gradient. For p∈ (2d/d+2,∞ ) , we first prove the existence of a martingale solution. Then we show the pathwise uniqueness of solutions. We employ the classical Yamada-Watanabe theorem to ensure the existence of a unique probabilistic strong solution.

Floodsub is a simple, robust and popular peer-to-peer publish/subscribe (pubsub) protocol, where nodes can arbitrarily leave or join the network, subscribe to or unsubscribe from topics and forward newly received messages to all of their neighbors, except the sender or the originating peer. To show the correctness of Floodsub, we propose its specification: Broadcastsub, in which implementation details like network connections and neighbor subscriptions are elided. To show that Floodsub does really implement Broadcastsub, one would have to show that the two systems have related infinite computations. We prove this by reasoning locally about states and their successors using Well-Founded Simulation (WFS). In this paper, we focus on the mechanization of a proof which shows that Floodsub is a simulation refinement of Broadcastsub using WFS. To the best of our knowledge, ours is the first mechanized refinement-based verification of a real world pubsub protocol.

In this work, we investigate the Central Limit Theorem (CLT) and Moderate Deviation Principle (MDP) for the stochastic generalized Burgers-Huxley (SGBH) equation with multiplicative Gaussian noise. The SGBH equation is a diffusion-convection-reaction type equation which consists a nonlinearity of polynomial order, and we take into account of an infinite-dimensional noise having a coefficient that has linear growth. We first prove the CLT which allows us to establish the convergence of the distribution of the solution to a re-scaled SGBH equation to a desired distribution function. Furthermore, we extend our asymptotic analysis by investigating the MDP for the SGBH equation. Using the weak convergence method, we establish the MDP and derive the corresponding rate function.

The asymptotic analysis of a class of stochastic partial differential equations (SPDEs) with fully locally monotone coefficients covering a large variety of physical systems, a wide class of quasilinear SPDEs and a good number of fluid dynamic models is carried out in this work. The aim of this work is to develop the large deviation theory for small Gaussian as well as Poisson noise perturbations of the above class of SPDEs. We establish a Wentzell-Freidlin type large deviation principle for the strong solutions to such SPDEs perturbed by Lévy noise in a suitable Polish space using a variational representation (based on a weak convergence approach) for nonnegative functionals of general Poisson random measures and Brownian motions. The well-posedness of an associated deterministic control problem is established by exploiting pseudo-monotonicity arguments and the stochastic counterpart is obtained by an application of Girsanov's theorem.

The main objective of this paper is to demonstrate the uniform large deviation principle (UDLP) for the solutions of two-dimensional stochastic Navier-Stokes equations (SNSE) in the vorticity form when perturbed by two distinct types of noises. We first consider an infinite-dimensional additive noise that is white in time and colored in space and then consider a finite-dimensional Wiener process with linear growth coefficient. In order to obtain the ULDP for 2D SNSE in the vorticity form, where the noise is white in time and colored in space, we utilize the existence and uniqueness result from \emph{B. Ferrario et. al., Stochastic Process. Appl., {\bf 129} (2019), 1568--1604,} and the \textsl{uniform contraction principle}. For the finite-dimensional multiplicative Wiener noise, we first prove the existence of a unique local mild solution to the vorticity equation using a truncation and fixed point arguments. We then establish the global existence of the truncated system by deriving a uniform energy estimate for the local mild solution. By applying stopping time arguments and a version of Skorokhod's representation theorem, we conclude the global existence and uniqueness of a solution to our model. We employ the weak convergence approach to establish the ULDP for the law of the solutions in two distinct topologies. We prove ULDP in the $\mathrm{C}([0,T];\mathrm{L}^p(\mathbb{T}^2))$ topology, for $p>2$, taking into account the uniformity of the initial conditions contained in bounded subsets of $\mathrm{L}^p(\mathbb{T}^2)$. Finally, in $\mathrm{C}([0,T]\times\mathbb{T}^2)$ topology, the uniformity of initial conditions lying in bounded subsets of $\mathrm{C}(\mathbb{T}^2)$ is considered.

GossipSub is a new peer-to-peer communication protocol designed to counter attacks from misbehaving peers by controlling what information is sent and to whom, via a score function computed by each peer that captures positive and negative behaviors of its neighbors. The score function depends on several parameters (weights, caps, thresholds) that can be configured by applications using GossipSub. The specification for GossipSub is written in English and its resilience to attacks from misbehaving peers is supported empirically by emulation testing using an implementation in Golang. In this work we take a foundational approach to understanding the resilience of GossipSub to attacks from misbehaving peers. We build the first formal model of GossipSub, using the ACL2s theorem prover. Our model is officially endorsed by the GossipSub developers. It can simulate GossipSub networks of arbitrary size and topology, with arbitrarily configured peers, and can be used to prove and disprove theorems about the protocol. We formalize fundamental security properties stating that the score function is fair, penalizes bad behavior, and rewards good behavior. We prove that the score function is always fair, but can be configured in ways that either penalize good behavior or ignore bad behavior. Using our model, we run GossipSub with the specific configurations for two popular real-world applications: the FileCoin and Eth2.0 blockchains. We show that all properties hold for FileCoin. However, given any Eth2.0 network (of any topology and size) with any number of potentially misbehaving peers, we can synthesize attacks where these peers are able to continuously misbehave by never forwarding topic messages, while maintaining positive scores so that they are never pruned from the network by GossipSub.

In this article, we establish the Wong-Zakai approximation result for a class of stochastic partial differential equations (SPDEs) with fully local monotone coefficients perturbed by a multiplicative Wiener noise. This class of SPDEs encompasses various fluid dynamic models and also includes quasi-linear SPDEs, the convection-diffusion equation, the Cahn-Hilliard equation, and the two-dimensional liquid crystal model. It has been established that the class of SPDEs in question is well-posed, however, the existence of a unique solution to the associated approximating system cannot be inferred from the solvability of the original system. We employ a Faedo-Galerkin approximation method, compactness arguments, and Prokhorov's and Skorokhod's representation theorems to ensure the existence of a probabilistically weak solution for the approximating system. Furthermore, we also demonstrate that the solution is pathwise unique. Moreover, the classical Yamada-Watanabe theorem allows us to conclude the existence of a probabilistically strong solution (analytically weak solution) for the approximating system. Subsequently, we establish the Wong-Zakai approximation result for a class of SPDEs with fully local monotone coefficients. We utilize the Wong-Zakai approximation to establish the topological support of the distribution of solutions to the SPDEs with fully local monotone coefficients. Finally, we explore the physically relevant stochastic fluid dynamics models that are covered by this work's functional framework.

Sparse regression is frequently employed in diverse scientific settings as a feature selection method. A pervasive aspect of scientific data that hampers both feature selection and estimation is the presence of strong correlations between predictive features. These fundamental issues are often not appreciated by practitioners, and jeapordize conclusions drawn from estimated models. On the other hand, theoretical results on sparsity-inducing regularized regression such as the Lasso have largely addressed conditions for selection consistency via asymptotics, and disregard the problem of model selection, whereby regularization parameters are chosen. In this numerical study, we address these issues through exhaustive characterization of the performance of several regression estimators, coupled with a range of model selection strategies. These estimators and selection criteria were examined across correlated regression problems with varying degrees of signal to noise, distribution of the non-zero model coefficients, and model sparsity. Our results reveal a fundamental tradeoff between false positive and false negative control in all regression estimators and model selection criteria examined. Additionally, we are able to numerically explore a transition point modulated by the signal-to-noise ratio and spectral properties of the design covariance matrix at which the selection accuracy of all considered algorithms degrades. Overall, we find that SCAD coupled with BIC or empirical Bayes model selection performs the best feature selection across the regression problems considered.

Almost all Computer Science programs require students to take a course on the Theory of Computation (ToC) which covers various models of computation such as finite automata, push-down automata and Turing machines. ToC courses tend to give assignments that require paper-and-pencil solutions. Grading such assignments takes time, so students typically receive feedback for their solutions more than a week after they complete them. We present the Automatic Automata Checker (A2C), an open source library that enables one to construct executable automata using definitions that mimic those found in standard textbooks. Such constructions are easy to reason about using semantic equivalence checks, properties and test cases. Instructors can conveniently specify solutions in the form of their own constructions. A2C can check for semantic equivalence between student and instructor solutions and can immediately generate actionable feedback, which helps students better understand the material. A2C can be downloaded and used locally by students as well as integrated into Learning Management Systems (LMS) like Gradescope to automatically grade student submissions and generate feedback. A2C is based on the ACL2s interactive theorem prover, which provides advanced methods for stating, proving and disproving properties. Since feedback is automatic, A2C can be deployed at scale and integrated into massively open online courses.

Teaching proofs is a crucial component of any undergraduate-level program that covers formal reasoning. We have developed a calculational reasoning format and refined it over several years of teaching a freshman-level course, "Logic and Computation", to thousands of undergraduate students. In our companion paper [28], we presented our calculational proof format, gave an overview of the calculational proof checker (CPC) tool that we developed to help users write and validate proofs, described some of the technical and implementation details of CPC and provided several publicly available proofs written using our format. In this paper, we dive deeper into the implementation details of CPC, highlighting how proof validation works, which helps us argue that our proof checking process is sound.

GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to a dynamically selected subset of their neighboring peers (mesh neighbors) while gossiping about messages they have seen with the rest. Peers decide which of their neighbors to graft or prune from their mesh locally and periodically using a score for each neighbor. Scores are calculated using a score function that depends on mesh-specific parameters, weights and counters relating to a peer's performance in the network. Since a GossipSub network's performance ultimately depends on the performance of its peers, an important question arises: Is the score calculation mechanism effective in weeding out non-performing or even intentionally misbehaving peers from meshes? We answered this question in the negative in our companion paper [31] by reasoning about GossipSub using our formal, official and executable ACL2s model. Based on our findings, we synthesized and simulated attacks against GossipSub which were confirmed by the developers of GossipSub, FileCoin, and Eth2.0, and publicly disclosed in MITRE CVE-2022-47547. In this paper, we present a detailed description of our model. We discuss design decisions, security properties of GossipSub, reasoning about the security properties in context of our model, attack generation and lessons we learnt when writing it.

The present work is concerned with two-dimensional stochastic sub-critical and critical convective Brinkman-Forchheimer (2 D SCBF) equations perturbed by a white noise (non-degenerate) in smooth bounded domains in R-2. We establish two important properties of the Markov semigroup associated with the solutions of 2 D SCBF equations (for the absorption exponent r - 1, 2, 3), that is, irreducibility and strong Feller property. These two properties implies the uniqueness of invariant measures and ergodicity also. Then, we discuss the ergodic behavior of 2D SCBF equations by providing a Large Deviation Principle (LDP) for the occupation measure for large time (Donsker-Varadhan), which describes the exact rate of exponential convergence.

In the realm of computer vision and robotics, the pursuit of intelligent robotic grasping and accurate 6D object pose estimation has been a focal point of research. Many modern-world applications, such as robot grasping, manipulation, and palletizing, require the correct pose of objects present in a scene to perform their specific tasks. The estimation of a 6D object pose becomes even more challenging due to inherent complexities, especially when dealing with objects positioned within cluttered scenes and subjected to high levels of occlusion. While prior endeavors have made strides in addressing this issue, their accuracy falls short of the reliability demanded by real-world applications. In this research, we present an architecture that, unlike prior works, incorporates contextual awareness. This novel approach capitalizes on the contextual information attainable about the objects in question. The framework we propose takes a dissection approach, discerning objects by their intrinsic characteristics, namely whether they are symmetric or non-symmetric. Notably, our methodology employs a more profound estimator and refiner network tandem for non-symmetric objects, in contrast to symmetric ones. This distinction acknowledges the inherent dissimilarities between the two object types, thereby enhancing performance. Through experiments conducted on the LineMOD dataset, widely regarded as a benchmark for pose estimation in occluded and cluttered scenes, we demonstrate a notable improvement in accuracy of approximately 3.2% compared to the previous state-of-the-art method, DenseFusion. Moreover, our results indicate that the achieved inference time is sufficient for real-time usage. Overall, our proposed architecture leverages contextual information and tailors the pose estimation process based on object types, leading to enhanced accuracy and real-time performance in challenging scenarios. Code is available at GitHub link