Searcharxiv⌕ Search

arXiv subjects

Vasily Pestun

Publications and source records attributed to Vasily Pestun.

At least 19 recordsLinked to original sources
arXiv2024

Graph2Tac: Online Representation Learning of Formal Math Concepts

In proof assistants, the physical proximity between two formal mathematical concepts is a strong predictor of their mutual relevance. Furthermore, lemmas with close proximity regularly exhibit similar proof structures. We show that this locality property can be exploited through online learning techniques to obtain solving agents that far surpass offline learners when asked to prove theorems in an unseen mathematical setting. We extensively benchmark two such online solvers implemented in the Tactician platform for the Coq proof assistant: First, Tactician's online $k$-nearest neighbor solver, which can learn from recent proofs, shows a $1.72\times$ improvement in theorems proved over an offline equivalent. Second, we introduce a graph neural network, Graph2Tac, with a novel approach to build hierarchical representations for new definitions. Graph2Tac's online definition task realizes a $1.5\times$ improvement in theorems solved over an offline baseline. The $k$-NN and Graph2Tac solvers rely on orthogonal online data, making them highly complementary. Their combination improves $1.27\times$ over their individual performances. Both solvers outperform all other general-purpose provers for Coq, including CoqHammer, Proverbot9001, and a transformer baseline by at least $1.48\times$ and are available for practical use by end-users.

cs.LG↗
arXiv2023

Seiberg-Witten Geometry of Four-Dimensional $\mathcal N=2$ Quiver Gauge Theories

Seiberg-Witten geometry of mass deformed $\mathcal N=2$ superconformal ADE quiver gauge theories in four dimensions is determined. We solve the limit shape equations derived from the gauge theory and identify the space $\mathfrak M$ of vacua of the theory with the moduli space of the genus zero holomorphic (quasi)maps to the moduli space ${\rm Bun}_{\mathbf G} (\mathcal E)$ of holomorphic $G^{\mathbb C}$-bundles on a (possibly degenerate) elliptic curve $\mathcal E$ defined in terms of the microscopic gauge couplings, for the corresponding simple ADE Lie group $G$. The integrable systems $\mathfrak P$ underlying the special geometry of $\mathfrak M$ are identified. The moduli spaces of framed $G$-instantons on ${\mathbb R}^{2} \times {\mathbb T}^{2}$, of $G$-monopoles with singularities on ${\mathbb R}^{2} \times {\mathbb S}^{1}$, the Hitchin systems on curves with punctures, as well as various spin chains play an important rôle in our story. We also comment on the higher-dimensional theories.

hep-th↗
arXiv2023

Transformer Models for Type Inference in the Simply Typed Lambda Calculus: A Case Study in Deep Learning for Code

Despite a growing body of work at the intersection of deep learning and formal languages, there has been relatively little systematic exploration of transformer models for reasoning about typed lambda calculi. This is an interesting area of inquiry for two reasons. First, typed lambda calculi are the lingua franc of programming languages. A set of heuristics that relate various typed lambda calculi to effective neural architectures would provide a systematic method for mapping language features (e.g., polymorphism, subtyping, inheritance, etc.) to architecture choices. Second, transformer models are widely used in deep learning architectures applied to code, but the design and hyperparameter space for them is large and relatively unexplored in programming language applications. Therefore, we suggest a benchmark that allows us to explore exactly this through perhaps the simplest and most fundamental property of a programming language: the relationship between terms and types. Consequently, we begin this inquiry of transformer architectures for typed lambda calculi by exploring the effect of transformer warm-up and optimizer selection in the task of type inference: i.e., predicting the types of lambda calculus terms using only transformers. We find that the optimization landscape is difficult even in this simple setting. One particular experimental finding is that optimization by Adafactor converges much faster compared to the optimization by Adam and RAdam. We conjecture that such different performance of optimizers might be related to the difficulties of generalization over formally generated dataset.

cs.PL↗
arXiv2022

Formalization of a Stochastic Approximation Theorem

Stochastic approximation algorithms are iterative procedures which are used to approximate a target value in an environment where the target is unknown and direct observations are corrupted by noise. These algorithms are useful, for instance, for root-finding and function minimization when the target function or model is not directly known. Originally introduced in a 1951 paper by Robbins and Monro, the field of Stochastic approximation has grown enormously and has come to influence application domains from adaptive signal processing to artificial intelligence. As an example, the Stochastic Gradient Descent algorithm which is ubiquitous in various subdomains of Machine Learning is based on stochastic approximation theory. In this paper, we give a formal proof (in the Coq proof assistant) of a general convergence theorem due to Aryeh Dvoretzky, which implies the convergence of important classical methods such as the Robbins-Monro and the Kiefer-Wolfowitz algorithms. In the process, we build a comprehensive Coq library of measure-theoretic probability theory and stochastic processes.

cs.LO↗
arXiv2022

Lax matrices from antidominantly shifted Yangians and quantum affine algebras: A-type

We construct a family of $GL_n$ rational and trigonometric Lax matrices $T_D(z)$ parametrized by $Λ^+$-valued divisors $D$ on $\mathbb{P}^1$. To this end, we study the shifted Drinfeld Yangians $Y_μ(\mathfrak{gl}_n)$ and quantum affine algebras $U_{μ^+,μ^-}(L\mathfrak{gl}_n)$, which slightly generalize their $\mathfrak{sl}_n$-counterparts. Our key observation is that both algebras admit the RTT type realization when $μ$ (respectively, $μ^+$ and $μ^-$) are antidominant coweights. We prove that $T_D(z)$ are polynomial in $z$ (up to a rational factor) and obtain explicit simple formulas for those linear in $z$. This generalizes the recent construction by the first two authors of linear rational Lax matrices in both trigonometric and higher $z$-degree directions. Furthermore, we show that all $T_D(z)$ are normalized limits of those parametrized by $D$ supported away from $\{\infty\}$ (in the rational case) or $\{0,\infty\}$ (in the trigonometric case). The RTT approach provides conceptual and elementary proofs for the construction of the coproduct homomorphisms on shifted Yangians and quantum affine algebras of $\mathfrak{sl}_n$, previously established via rather tedious computations. Finally, we establish a close relation between a certain collection of explicit linear Lax matrices and the well-known parabolic Gelfand-Tsetlin formulas.

math.RT↗
arXiv2020

CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires a recent line of work on formally constrained reinforcement learning; however, these methods place the implementation of the learning algorithm in their Trusted Computing Base. The crucial correctness property of these implementations is a guarantee that the learning algorithm converges to an optimal policy. This paper begins the work of closing this gap by developing a Coq formalization of two canonical reinforcement learning algorithms: value and policy iteration for finite state Markov decision processes. The central results are a formalization of Bellman's optimality principle and its proof, which uses a contraction property of Bellman optimality operator to establish that a sequence converges in the infinite horizon limit. The CertRL development exemplifies how the Giry monad and mechanized metric coinduction streamline optimality proofs for reinforcement learning algorithms. The CertRL library provides a general framework for proving properties about Markov decision processes and reinforcement learning algorithms, paving the way for further work on formalization of reinforcement learning algorithms.

cs.AI↗
arXiv2019

Multiplicative Hitchin Systems and Supersymmetric Gauge Theory

Multiplicative Hitchin systems are analogues of Hitchin's integrable system based on moduli spaces of G-Higgs bundles on a curve C where the Higgs field is group-valued, rather than Lie algebra valued. We discuss the relationship between several occurences of these moduli spaces in geometry and supersymmetric gauge theory, with a particular focus on the case where C = CP1 with a fixed framing at infinity. In this case we prove that the identification between multiplicative Higgs bundles and periodic monopoles proved by Charbonneau and Hurtubise can be promoted to an equivalence of hyperkähler spaces, and analyze the twistor rotation for the multiplicative Hitchin system. We also discuss quantization of these moduli spaces, yielding the modules for the Yangian Y(g) discovered by Gerasimov, Kharchev, Lebedev and Oblezin.

math.AG↗
arXiv2019

Super instanton counting and localization

We study the super instanton solution in the gauge theory with U$(n_{+}| n_{-})$ gauge group. Based on the ADHM construction generalized to the supergroup theory, we derive the instanton partition function from the super instanton moduli space through the equivariant localization. We derive the Seiberg-Witten geometry and its quantization for the supergroup gauge theory from the instanton partition function, and study the connection with classical and quantum integrable systems. We also argue the brane realization of the supergroup quiver gauge theory, and possible connection to the non-supergroup quiver gauge theories.

hep-th↗
arXiv2019

Twisted reduction of quiver W-algebras

We consider the $k$-twisted Nekrasov-Shatashvili limit (NS$_k$ limit) of 5d (K-theoretic) and 6d (elliptic) quiver gauge theory, where one of the multiplicative equivariant parameters is taken to be the $k$-th root of unity. We obtain the extended center of the associated $q$-deformed quiver W-algebras constructed by our formalism [arXiv:1512.08533; arXiv:1608.04651; arXiv:1705.04410], which provides gauge theoretic proof of Bouwknegt-Pilch's statement on the relation to the representation ring of quantum affine algebra.

hep-th↗
arXiv2019

A Family of ${\rm GL}_r$ Multiplicative Higgs Bundles on Rational Base

In this paper we study a restricted family of holomorphic symplectic leaves in the Poisson-Lie group ${\rm GL}_r(\mathcal{K}_{\mathbb{P}^1_x})$ with rational quadratic Sklyanin brackets induced by a one-form with a single quadratic pole at $\infty \in \mathbb{P}_{1}$. The restriction of the family is that the matrix elements in the defining representation are linear functions of $x$. We study how the symplectic leaves in this family are obtained by the fusion of certain fundamental symplectic leaves. These symplectic leaves arise as minimal examples of (i) moduli spaces of multiplicative Higgs bundles on $\mathbb{P}^{1}$ with prescribed singularities, (ii) moduli spaces of $U(r)$ monopoles on $\mathbb{R}^2 \times S^1$ with Dirac singularities, (iii) Coulomb branches of the moduli space of vacua of 4d $\mathcal{N}=2$ supersymmetric $A_{r-1}$ quiver gauge theories compactified on a circle. While degree 1 symplectic leaves regular at $\infty \in \mathbb{P}^1$ (Coulomb branches of the superconformal quiver gauge theories) are isomorphic to co-adjoint orbits in $\mathfrak{gl}_{r}$ and their Darboux parametrization and quantization is well known, the case irregular at infinity (asymptotically free quiver gauge theories) is novel. We also explicitly quantize the algebra of functions on these moduli spaces by presenting the corresponding solutions to the quantum Yang-Baxter equation valued in Heisenberg algebra (free field realization).

hep-th↗
arXiv2018

Fractional quiver W-algebras

We introduce quiver gauge theory associated with the non-simply-laced type fractional quiver, and define fractional quiver W-algebras by using construction of arXiv:1512.08533 and arXiv:1608.04651 with representation of fractional quivers.

hep-th↗
arXiv2018

Quiver W-algebras

For a quiver with weighted arrows we define gauge-theory K-theoretic W-algebra generalizing the definition of Shiraishi et al., and Frenkel and Reshetikhin. In particular, we show that the qq-character construction of gauge theory presented by Nekrasov is isomorphic to the definition of the W-algebra in the operator formalism as a commutant of screening charges in the free field representation. Besides, we allow arbitrary quiver and expect interesting applications to representation theory of generalized Borcherds-Kac-Moody Lie algebras, their quantum affinizations and associated W-algebras.

hep-th↗
arXiv2018

Quiver elliptic W-algebras

We define elliptic generalization of W-algebras associated with arbitrary quiver using the formalism of arXiv:1512.08533 applied to six-dimensional quiver gauge theory compactified on elliptic curve.

hep-th↗
arXiv2017

Language as a matrix product state

We propose a statistical model for natural language that begins by considering language as a monoid, then representing it in complex matrices with a compatible translation invariant probability measure. We interpret the probability measure as arising via the Born rule from a translation invariant matrix product state.

cs.CL↗
arXiv2017

Tensor network language model

We propose a new statistical model suitable for machine learning of systems with long distance correlations such as natural languages. The model is based on directed acyclic graph decorated by multi-linear tensor maps in the vertices and vector spaces in the edges, called tensor network. Such tensor networks have been previously employed for effective numerical computation of the renormalization group flow on the space of effective quantum field theories and lattice models of statistical mechanics. We provide explicit algebro-geometric analysis of the parameter moduli space for tree graphs, discuss model properties and applications such as statistical translation.

cs.CL↗
arXiv2017

Localization for ${\cal N}=2$ Supersymmetric Gauge Theories in Four Dimensions

This is the 5th article in the collection of reviews "Exact results on N=2 supersymmetric gauge theories", ed. J. Teschner. We review the supersymmetric localization of $\mathcal{N}=2$ theories on curved backgrounds in four dimensions using $\mathcal{N}=2$ supergravity and generalised conformal Killing spinors. We review some known backgrounds and give examples of new geometries such as local $T^2$-bundle fibrations. We discuss in detail a topological four-sphere with generic $T^2$-invariant metric.

hep-th↗
arXiv2016

Introduction to localization in quantum field theory

This is the introductory chapter to the volume. We review the main idea of the localization technique and its brief history both in geometry and in QFT. We discuss localization in diverse dimensions and give an overview of the major applications of the localization calculations for supersymmetric theories. We explain the focus of the present volume.

hep-th↗