arXiv subjects

Anindya Banerjee

Publications and source records attributed to Anindya Banerjee.

At least 19 recordsLinked to original sources

arXiv2025

Macdonald Index From Refined Kontsevich-Soibelman Operator

We propose a refinement of the Kontsevich-Soibelman operator for a class of ``special'' 4d $\mathcal{N}=2$ superconformal field theories characterized by the following conditions: (1) their Coulomb branch admits a source/sink chamber, i.e., a chamber in which the BPS quiver consists of only source and sink nodes, (2) The nodes with valency greater than 2 of the BPS quiver in a source/sink chamber are either all sources or all sinks. We present strong evidence that the trace of this refined operator is related to the Macdonald index of the theory. In particular, we conjecture closed form expressions for the Macdonald indices of the $(A_1,\mathfrak{g})$ Argyres-Douglas theories for any simply-laced Lie algebra $\mathfrak{g}$.

hep-th↗

arXiv2025

Forall-Exists Relational Verification by Filtering to Forall-Forall

Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational Hoare logics exist, with accompanying tool support for compositional reasoning of $\forall\forall$ (2-safety) properties and, generally, k-safety properties of product programs. In contrast, few logics and tools exist for reasoning about $\forall\exists$ properties which are critical in the context of nondeterminism. This paper's primary contribution is a methodology for verifying a $\forall\exists$ judgment by way of a novel filter-adequacy transformation. This transformation adds assertions to a product program in such a way that the desired $\forall\exists$ property (of a pair of underlying unary programs) is implied by a $\forall\forall$ property of the transformed product. The paper develops a program logic for the basic $\forall\exists$ judgement extended with assertion failures; develops bicoms, a form of product programs that represents pairs of executions and that caters for direct translation of $\forall\forall$ properties to unary correctness; proves (using the logic) a soundness theorem that says successful $\forall\forall$ verification of a transformed bicom implies the $\forall\exists$ spec for its underlying unary commands; and implements a proof of principle prototype for auto-active relational verification which has been used to verify all examples in the paper. The methodology thereby enables a user to work with ordinary assertions and assumptions, and a standard assertion language, so that existing tools including auto-active verifiers can be used.

cs.LO↗

arXiv2025

Argyres-Douglas Theories, Macdonald Indices and Arc Space of Zhu Algebra

In this paper, we relate the MacDonald index of a 4d $\mathcal{N}=2$ SCFT with the Hilbert series of the arc space of the Zhu algebra of the corresponding Schur VOA. Using this, we conjecture a simple formula for the MacDonald index of $(A_1,D_{2n+1})$ Argyres-Douglas theory. We perform checks of the formula against the known Schur limits and RG flows. To match the Schur limit, we prove new $q$-series identities.

hep-th↗

arXiv2024

3d $\mathcal{N}=4$ Mirror Symmetry, TQFTs, and 't Hooft Anomaly Matching

Any local unitary 3d $\mathcal{N}=4$ superconformal field theory (SCFT) has a corresponding "universal" relevant deformation that takes it to a gapped phase. This deformation preserves all continuous internal symmetries, $\mathcal{S}$, and therefore also preserves any 't Hooft anomalies supported purely in $\mathcal{S}$. We describe the resulting phase diagram in the case of SCFTs that arise as the endpoints of renormalization group flows from 3d $\mathcal{N}=4$ Abelian gauge theories with any number of $U(1)$ gauge group factors and arbitrary integer charges for the matter fields. We argue that the universal deformations take these QFTs to Abelian fractional quantum Hall states in the infrared (IR), and we explain how to match 't Hooft anomalies between the non-topological ultraviolet theories and the IR topological quantum field theories (TQFTs). Along the way, we give a proof that 3d $\mathcal{N}=4$ mirror symmetry of our Abelian gauge theories descends to a duality of these TQFTs. Finally, using our anomaly matching discussion, we describe how to connect, via the renormalization group, abstract local unitary 3d $\mathcal{N}=4$ SCFTs with certain 't Hooft anomalies for their internal symmetries to IR phases (partially) described by Abelian spin Chern-Simons theories.

hep-th↗

arXiv2024

A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs

When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.

cs.PL↗

arXiv2023

Alignment complete relational Hoare logics for some and all

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments of executions. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A single degenerate alignment rule (sequential composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the sense of Cook. The notion of alignment completeness was previously proposed as an additional measure, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. This paper proves alignment completeness with respect to a general class of $\forall\forall$ alignment automata, for a RHL comprised of standard rules together with a rule of semantics-preserving rewrites based on Kleene algebra with tests. A new logic for $\forall\exists$ properties is introduced and shown to be sound and alignment complete for a new general class of automata. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus both logics are complete in the sense of Cook. The paper includes discussion of why alignment is not the only important principle for relational reasoning and proposes entailment completeness as further means to evaluate RHLs.

cs.LO↗

arXiv2023

Non-Perturbative Explorations of Chiral Rings in 4d $\mathcal{N}=2$ SCFTs

We study the conditions under which 4d $\mathcal{N}=2$ superconformal field theories (SCFTs) have multiplets housing operators that are chiral with respect to an $\mathcal{N}=1$ subalgebra. Our main focus is on the set of often-ignored and relatively poorly understood $\overline{\mathcal{B}}$ representations. These multiplets typically evade direct detection by the most popular non-perturbative 4d $\mathcal{N}=2$ tools and correspondences. In spite of this fact, we demonstrate the ubiquity of $\overline{\mathcal{B}}$ multiplets and show they are associated with interesting phenomena. For example, we give a purely algebraic proof that they are present in all local unitary $\mathcal{N}>2$ SCFTs. We also show that $\overline{\mathcal{B}}$ multiplets exist in $\mathcal{N}=2$ theories with rank greater than one and a conformal manifold or a freely generated Coulomb branch. Using recent topological quantum field theory results, we argue that certain $\overline{\mathcal{B}}$ multiplets exist in broad classes of theories with the $\mathbb{Z}_2$-valued 't Hooft anomaly for $Sp(N)$ global symmetry. Motivated by these statements, we then study the question of whether $\overline{\mathcal{B}}$ multiplets exist in rank-one SCFTs with exactly $\mathcal{N}=2$ SUSY. We conclude with various open questions.

hep-th↗

arXiv2023

The WhyRel Prototype for Relational Verification

Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents WhyRel, a tool for the auto-active verification of relational properties of pointer programs based on relational region logic. WhyRel is evaluated through verification case studies, relying on SMT solvers orchestrated by the Why3 platform on which it builds. Case studies include establishing representation independence of ADTs, showing noninterference, and challenge problems from recent literature.

cs.PL↗

arXiv2023

Inductive Reasoning for Coinductive Types

We present AlgCo (Algebraic Coinductives), a practical framework for inductive reasoning over commonly used coinductive types such as conats, streams, and infinitary trees with finite branching factor. The key idea is to exploit the notion of algebraic complete partial order from domain theory to define continuous operations over coinductive types via primitive recursion on ``dense'' collections of their elements, enabling a convenient strategy for reasoning about algebraic coinductives by straightforward proofs by induction. We implement the AlgCo framework in Coq and demonstrate its power by verifying a stream variant of the sieve of Eratosthenes, a regular expression library based on coinductive trie encodings of formal languages, and expected value semantics for coinductive sampling processes over discrete probability distributions in the random bit model.

cs.LO↗

arXiv2022

Making Relational Hoare Logic Alignment Complete

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A RHL can be complete, in the ordinary sense, using a single degenerate alignment rule. The notion of alignment completeness was previously proposed as a more satisfactory measure, based on alignment automata, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. Using a rule of semantics-preserving rewrites based on Kleene algebra with tests, an RHL is shown to be alignment complete with respect to a very general class of alignment automata. Besides solving the open problem of general alignment completeness, this result bridges between human-friendly syntax-based reasoning and automata representations that facilitate automated verification.

cs.LO↗

arXiv2022

Formally Verified Samplers From Probabilistic Programs With Loops and Conditioning

We present Zar: a formally verified compiler pipeline from discrete probabilistic programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. We exploit the key idea that all discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates a cpGCL program into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct wrt. the conditional weakest pre-expectation semantics of cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples.

cs.PL↗

arXiv2022

Comments on Summing over Bordisms in TQFT

Recent works in quantum gravity, motivated by the factorization problem and baby universes, have considered sums over bordisms with fixed boundaries in topological quantum field theory (TQFT). We discuss this construction and observe a curious splitting formula for the total amplitude.

hep-th↗

arXiv2022

A Relational Program Logic with Data Abstraction and Dynamic Framing

Dedicated to Tony Hoare. In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extended to encompass dynamically allocated objects. In recent years, progress has been made towards formalizing the claim, for simulation, though mainly in semantic developments. In this article, hiding and simulation are combined with the idea in Hoare's 1969 paper: a logic of programs. For an object-based language with dynamic allocation, we introduce a relational Hoare logic with stateful frame conditions that formalizes encapsulation, hiding of invariants, and couplings that relate two implementations. Relations and other assertions are expressed in first-order logic. Specifications can express a wide range of relational properties such as conditional equivalence and noninterference with declassification. The proof rules facilitate relational reasoning by means of convenient alignments and are shown sound with respect to a conventional operational semantics. A derived proof rule for equivalence of linked programs directly embodies representation independence. Applicability to representative examples is demonstrated using an SMT-based implementation.

cs.LO↗

arXiv2021

On Algebraic Abstractions for Concurrent Separation Logics

Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations. This paper provides an algebraic formalization of ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations. Morphisms of structures are a standard concept in algebra and category theory, but haven't seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.

cs.PL↗

arXiv2021

A Formal Proof of PAC Learnability for Decision Stumps

We present a formal proof in Lean of probably approximately correct (PAC) learnability of the concept class of decision stumps. This classic result in machine learning theory derives a bound on error probabilities for a simple type of classifier. Though such a proof appears simple on paper, analytic and measure-theoretic subtleties arise when carrying it out fully formally. Our proof is structured so as to separate reasoning about deterministic properties of a learning function from proofs of measurability and analysis of probabilities.

cs.LG↗

arXiv2020

Hyperkähler Isometries Of K3 Surfaces

We consider symmetries of K3 manifolds. Holomorphic symplectic automorphisms of K3 surfaces have been classified, and observed to be subgroups of the Mathieu group $M_{23}$. More recently, automorphisms of K3 sigma models commuting with $SU(2)\times SU(2)$ $R$-symmetry have been classified by Gaberdiel, Hohenegger, and Volpato. These groups are all subgroups of the Conway group. We fill in a small gap in the literature and classify the possible hyperkähler isometry groups of K3 manifolds. There is an explicit list of $40$ possible groups, all of which are realized in the moduli space. The groups are all subgroups of $M_{23}$.

hep-th↗

arXiv2020

Verification of ML Systems via Reparameterization

As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machine learning algorithms with formal guarantees about performance, robustness, or fairness. Yet, the analysis of these algorithms is often complex, and implementing such systems in practice introduces room for error. Proof assistants can be used to formally verify machine learning systems by constructing machine checked proofs of correctness that rule out such bugs. However, reasoning about probabilistic claims inside of a proof assistant remains challenging. We show how a probabilistic program can be automatically represented in a theorem prover using the concept of \emph{reparameterization}, and how some of the tedious proofs of measurability can be generated automatically from the probabilistic program. To demonstrate that this approach is broad enough to handle rather different types of machine learning systems, we verify both a classic result from statistical learning theory (PAC-learnability of decision stumps) and prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.

cs.LG↗

arXiv2019

Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations

In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.

cs.PL↗