MathZero, The Classification Problem, and Set-Theoretic Type Theory
AlphaZero learns to play go, chess and shogi at a superhuman level through self play given only the rules of the game. This raises the question of whether a similar thing could be done for mathematics -- a MathZero. MathZero would require a formal foundation and an objective. We propose the foundation of set-theoretic dependent type theory and an objective defined in terms of the classification problem -- the problem of classifying concept instances up to isomorphism. The natural numbers arise as the solution to the classification problem for finite sets. Here we generalize classical Bourbaki set-theoretic isomorphism to set-theoretic dependent type theory. To our knowledge we give the first isomorphism inference rules for set-theoretic dependent type theory with propositional set-theoretic equality. The presentation is intended to be accessible to mathematicians with no prior exposure to type theory.
Code (0)
등록된 구현이 없습니다.
Tasks
ClassificationGeneral ClassificationVocal Bursts Type PredictionSimilar Papers 제목 키워드 기반
Bayesian Classification and Inference in a Probabilistic Type Theory with Records
We propose a probabilistic account of semantic inference and classification formulated in terms of probabilistic type theory with records, building on Cooper et. al. (2014) and Cooper et. al. (2015). We suggest probabili…
ClassificationVocal Bursts Type PredictionTheory-Inspired Path-Regularized Differential Network Architecture Search
Despite its high search efficiency, differential architecture search (DARTS) often selects network architectures with dominated skip connections which lead to performance degradation. However, theoretical understandings …
image-classificationImage ClassificationSemantic Classification and Learning Using a Linear Tranformation Model in a Probabilistic Type Theory with Records
Starting from an existing account of semantic classification and learning from interaction formulated in a Probabilistic Type Theory with Records, encompassing Bayesian inference and learning with a frequentist flavour, …
Bayesian InferenceClassificationGeneralization in Machine Learning via Analytical Learning Theory
This paper introduces a novel measure-theoretic theory for machine learning that does not require statistical assumptions. Based on this theory, a new regularization method in deep learning is derived and shown to outper…
BIG-bench Machine LearningDeep LearningLearning TheoryOne-Shot Learning+1Large scale classification in deep neural network with Label Mapping
In recent years, deep neural network is widely used in machine learning. The multi-class classification problem is a class of important problem in machine learning. However, in order to solve those types of multi-class c…
BIG-bench Machine LearningClassificationGeneral ClassificationMulti-class Classification