检索结果-内蒙古大学图书馆

Fundamental Components of Deep Learning A category-theoretic approach

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Gavranović, Bruno Mathematically Structured Programming Group University of Strathclyde Glasgow United Kingdom

Deep learning, despite its remarkable achievements, is still a young field. Like the early stages of many scientific disciplines, it is marked by the discovery of new phenomena, ad-hoc design decisions, and the lack of a uniform and compositional mathematical foundation. From the intricacies of the implementation of backpropagation, through a growing zoo of neural network architectures, to the new and poorly understood phenomena such as double descent, scaling laws or in-context learning, there are few unifying principles in deep learning. This thesis develops a novel mathematical foundation for deep learning based on the language of category theory. We develop a new framework that is a) end-to-end, b) unform, and c) not merely descriptive, but prescriptive, meaning it is amenable to direct implementation in programming languages with sufficient features. We also systematise many existing approaches, placing many existing constructions and concepts from the literature under the same umbrella. In Part I, the theory, we identify and model two main properties of deep learning systems: they are parametric and bidirectional. We expand on the previously defined construction of actegories and Para to study the former, and define weighted optics to study the latter. Combining them yields parametric weighted optics, a categorical model of artificial neural networks, and more: constructions in Part I have close ties to many other kinds of bidirectional processes such as bayesian updating, value iteraton, and game theory. Part II justifies the abstractions from Part I, applying them to model backpropagation, architectures, and supervised learning. We provide a lens-theoretic axiomatisation of differentiation, covering not just smooth spaces, but discrete settings of boolean circuits as well. We survey existing, and develop new categorical models of neural network architectures. We formalise the notion of optimisers and lastly, combine all the existing concepts together, provid

关键词： Backpropagation

Learning functors using gradient descent

学校读者我要写书评

暂无评论

arXiv 2020年

作者： Gavranović, Bruno Mathematically Structured Programming Group University of Strathclyde Glasgow United Kingdom

Neural networks are a general framework for differentiable optimization which includes many other machine learning approaches as special cases. In this paper we build a category-theoretic formalism around a neural network system called CycleGAN [15]. CycleGAN is a general approach to unpaired image-to-image translation that has been getting attention in the recent years. Inspired by categorical database systems, we show that CycleGAN is a "schema", i.e. a specific category presented by generators and relations, whose specific parameter instantiations are just set-valued functors on this schema. We show that enforcing cycle-consistencies amounts to enforcing composition invariants in this category. We generalize the learning procedure to arbitrary such categories and show a special class of functors, rather than functions, can be learned using gradient descent. Using this framework we design a novel neural network system capable of learning to insert and delete objects from images without paired data. We qualitatively evaluate the system on the CelebA dataset and obtain promising results. Copyright © 2020, The Authors. All rights reserved.

关键词： Gradient methods

A Semantic Proof of Generalised Cut Elimination for Deep Inference

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Atkey, Robert Kokke, Wen Mathematically Structured Programming Group Computer and Information Sciences University of Strathclyde Glasgow United Kingdom

Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "before" or "sequencing". MAV is also an extenson of the the logic Basic System Virtual (BV) with additives. Formulas in BV have an appealing reading as processes with parallel and sequential composition. MAV adds internal and external choice operators. BV and MAV are also closely related to Concurrent Kleene Algebras. Proof systems for MAV and BV are Deep Inference systems, which allow inference rules to be applied anywhere inside a structure. As with any proof system, a key question is whether proofs in MAV can be reduced to a normal form, removing detours and the introduction of structures not present in the original goal. In Sequent Calcluli systems, this property is referred to as Cut Elimination. Deep Inference systems have an analogous Cut rule and other rules that are not present in normalised proofs. Cut Elimination for Deep Inference systems has the same metatheoretic benefits as for Sequent Calculi systems, including consistency and decidability. Proofs of Cut Elimination for BV, MAV, and other Deep Inference systems present in the literature have relied on intrincate syntactic reasoning and complex termination measures. We present a concise semantic proof that all MAV proofs can be reduced to a normal form avoiding the Cut rule and other "non analytic" rules. We also develop soundness and completeness proofs of MAV (and BV) with respect to a class of models. We have mechanised all our proofs in the Agda proof assistant, which provides both assurance of their correctness as well as yielding an executable normalisation procedure. Our technique extends to include exponentials and the additive units. © 2024, CC BY.

关键词： Algebra

Actegories for the Working Amthematician

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Capucci, Matteo Gavranović, Bruno Mathematically Structured Programming Group Department of Computer and Information Sciences University of Strathclyde Glasgow United Kingdom

Actions of monoidal categories on categories, also known as actegories, have been familiar to category theorists for a long time, and yet a comprehensive overview of this topic seems to be missing from the literature. Recently, actegories have been increasingly employed in applied category theory, thereby encouraging an effort to fill this gap according to the new needs of these applications. This work started as an investigation of the notion of monoidal actegory, a compatible pair of monoidal and actegorical structures, and ended up including a sizable reference on the elementary theory of actegories. We cover basic definitions and results on actegories and biactegories, spelling out explicitly many folkloric definitions, including their tensor product and their hom-tensor adjunction. We give new definitions of actegories with monoidal, braided monoidal and symmetric monoidal structure. In the last section, we provide three Cayley-like classification results for these *** Codes 18-02 © 2022, CC BY-SA.

关键词： Tensors

Rendering string diagrams recursively

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Rubio-Madrigal, Celia Hedges, Jules CISPA Helmholtz Center for Information Security Germany Mathematically Structured Programming group University of Strathclyde United Kingdom Institute for Categorical Cybernetics

String diagrams are a graphical language used to represent processes that can be composed sequentially or in parallel, which correspond graphically to horizontal or vertical juxtaposition. In this paper we demonstrate how to compute the layout of a string diagram by folding over its algebraic representation in terms of sequential and parallel composition operators. The algebraic representation can be seen as a term of a free monoidal category or a proof tree for a small fragment of linear logic. This contrasts to existing non-compositional approaches that use graph layout techniques. The key innovation is storing the diagrams in binary space-partition trees, maintaining a right-trapezoidal shape for the diagram's outline as an invariant. We provide an implementation in Haskell, using an existing denotational graphics library called Diagrams. Our renderer also supports adding semantics to diagrams to serve as a compiler, with matrix algebra used as an example. Copyright © 2024, The Authors. All rights reserved.

关键词： Semantics

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Daggitt, Matthew L. Kokke, Wen Atkey, Robert Arnaboldi, Luca Komendantskya, Ekaterina Department of Computer Science Heriot-Watt University Edinburgh United Kingdom Mathematically Structured Programming Group University of Strathclyde Glasgow United Kingdom Laboratory for Foundations of Computer Science University of Edinburgh Edinburgh United Kingdom

Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs. © 2022, CC BY.

关键词： Problem oriented languages

On a Fibrational Construction for Optics, Lenses, and Dialectica Categories

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Capucci, Matteo Gavranović, Bruno Malik, Abdullah Rios, Francisco Weinberger, Jonathan Mathematically Structured Programming University of Strathclyde Glasgow United Kingdom Symbolica AI Department of Mathematics Florida State University TallahasseeFL United States Quantum Computational Science Group Oak Ridge National Laboratory Oak RidgeTN United States Chapman University OrangeCA United States

MSC Codes 18M35, 18D30, 18M05, 03G30, 03B38Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this work, we show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra’s construction of Dialectica fibrations and Spivak’s construction of generalized lenses. This construction turns a tower of Grothendieck fibrations into another tower of fibrations by iteratively twisting each of the components, using the opposite fibration construction. © 2024, CC BY.

关键词： Optical instrument lenses