-
Torus cannot collapse to a segment
Authors:
Mikhail G. Katz
Abstract:
In earlier work, we analyzed the impossibility of codimension-one collapse for surfaces of negative Euler characteristic under the condition of a lower bound for the Gaussian curvature. Here we show that, under similar conditions, the torus cannot collapse to a segment. Unlike the torus, the Klein bottle can collapse to a segment; we show that in such a situation, the loops in a short basis for ho…
▽ More
In earlier work, we analyzed the impossibility of codimension-one collapse for surfaces of negative Euler characteristic under the condition of a lower bound for the Gaussian curvature. Here we show that, under similar conditions, the torus cannot collapse to a segment. Unlike the torus, the Klein bottle can collapse to a segment; we show that in such a situation, the loops in a short basis for homology must stay a uniform distance apart.
△ Less
Submitted 10 May, 2020; v1 submitted 18 February, 2020;
originally announced February 2020.
-
Mathematical conquerors, Unguru polarity, and the task of history
Authors:
Mikhail G. Katz
Abstract:
We compare several approaches to the history of mathematics recently proposed by Blasjo, Fraser--Schroter, Fried, and others. We argue that tools from both mathematics and history are essential for a meaningful history of the discipline.
In an extension of the Unguru-Weil controversy over the concept of geometric algebra, Michael Fried presents a case against both Andre Weil the "privileged obse…
▽ More
We compare several approaches to the history of mathematics recently proposed by Blasjo, Fraser--Schroter, Fried, and others. We argue that tools from both mathematics and history are essential for a meaningful history of the discipline.
In an extension of the Unguru-Weil controversy over the concept of geometric algebra, Michael Fried presents a case against both Andre Weil the "privileged observer" and Pierre de Fermat the "mathematical conqueror." We analyze Fried's version of Unguru's alleged polarity between a historian's and a mathematician's history. We identify some axioms of Friedian historiographic ideology, and propose a thought experiment to gauge its pertinence.
Unguru and his disciples Corry, Fried, and Rowe have described Freudenthal, van der Waerden, and Weil as Platonists but provided no evidence; we provide evidence to the contrary. We analyze how the various historiographic approaches play themselves out in the study of the pioneers of mathematical analysis including Fermat, Leibniz, Euler, and Cauchy.
△ Less
Submitted 1 February, 2020;
originally announced February 2020.
-
An inequality for length and volume in the complex projective plane
Authors:
Mikhail G. Katz
Abstract:
We prove a new inequality relating volume to length of closed geodesics on area minimizers for generic metrics on the complex projective plane. We exploit recent regularity results for area minimizers by Moore and White, and the Kronheimer--Mrowka proof of the Thom conjecture.
We prove a new inequality relating volume to length of closed geodesics on area minimizers for generic metrics on the complex projective plane. We exploit recent regularity results for area minimizers by Moore and White, and the Kronheimer--Mrowka proof of the Thom conjecture.
△ Less
Submitted 8 September, 2020; v1 submitted 1 January, 2020;
originally announced January 2020.
-
Varieties in Cages: a Little Zoo of Algebraic Geometry
Authors:
Gabriel Katz
Abstract:
A $d^{\{n\}}$-cage $\mathsf K$ is the union of $n$ groups of hyperplanes in $\Bbb P^n$, each group containing $d$ members. The hyperplanes from the distinct groups are in general position, thus producing $d^n$ points, where hyperplanes from all groups intersect. These points are called the nodes of $\mathsf K$. We study the combinatorics of nodes that impose independent conditions on the varieties…
▽ More
A $d^{\{n\}}$-cage $\mathsf K$ is the union of $n$ groups of hyperplanes in $\Bbb P^n$, each group containing $d$ members. The hyperplanes from the distinct groups are in general position, thus producing $d^n$ points, where hyperplanes from all groups intersect. These points are called the nodes of $\mathsf K$. We study the combinatorics of nodes that impose independent conditions on the varieties $X \subset \Bbb P^n$ containing them. We prove that if $X$, given by homogeneous polynomials of degrees $\leq d$, contains the points from such a special set $\mathsf A$ of nodes, then it contains all the nodes of $\mathsf K$. Such a variety $X$ is very special: in particular, $X$ is a complete intersection.
△ Less
Submitted 13 July, 2021; v1 submitted 12 December, 2019;
originally announced December 2019.
-
RankML: a Meta Learning-Based Approach for Pre-Ranking Machine Learning Pipelines
Authors:
Doron Laadan,
Roman Vainshtein,
Yarden Curiel,
Gilad Katz,
Lior Rokach
Abstract:
The explosion of digital data has created multiple opportunities for organizations and individuals to leverage machine learning (ML) to transform the way they operate. However, the shortage of experts in the field of machine learning -- data scientists -- is often a setback to the use of ML. In an attempt to alleviate this shortage, multiple approaches for the automation of machine learning have b…
▽ More
The explosion of digital data has created multiple opportunities for organizations and individuals to leverage machine learning (ML) to transform the way they operate. However, the shortage of experts in the field of machine learning -- data scientists -- is often a setback to the use of ML. In an attempt to alleviate this shortage, multiple approaches for the automation of machine learning have been proposed in recent years. While these approaches are effective, they often require a great deal of time and computing resources. In this study, we propose RankML, a meta-learning based approach for predicting the performance of whole machine learning pipelines. Given a previously-unseen dataset, a performance metric, and a set of candidate pipelines, RankML immediately produces a ranked list of all pipelines based on their predicted performance. Extensive evaluation on 244 datasets, both in regression and classification tasks, shows that our approach either outperforms or is comparable to state-of-the-art, computationally heavy approaches while requiring a fraction of the time and computational cost.
△ Less
Submitted 20 November, 2019; v1 submitted 31 October, 2019;
originally announced November 2019.
-
DeepLine: AutoML Tool for Pipelines Generation using Deep Reinforcement Learning and Hierarchical Actions Filtering
Authors:
Yuval Heffetz,
Roman Vainstein,
Gilad Katz,
Lior Rokach
Abstract:
Automatic machine learning (AutoML) is an area of research aimed at automating machine learning (ML) activities that currently require human experts. One of the most challenging tasks in this field is the automatic generation of end-to-end ML pipelines: combining multiple types of ML algorithms into a single architecture used for end-to-end analysis of previously-unseen data. This task has two cha…
▽ More
Automatic machine learning (AutoML) is an area of research aimed at automating machine learning (ML) activities that currently require human experts. One of the most challenging tasks in this field is the automatic generation of end-to-end ML pipelines: combining multiple types of ML algorithms into a single architecture used for end-to-end analysis of previously-unseen data. This task has two challenging aspects: the first is the need to explore a large search space of algorithms and pipeline architectures. The second challenge is the computational cost of training and evaluating multiple pipelines. In this study we present DeepLine, a reinforcement learning based approach for automatic pipeline generation. Our proposed approach utilizes an efficient representation of the search space and leverages past knowledge gained from previously-analyzed datasets to make the problem more tractable. Additionally, we propose a novel hierarchical-actions algorithm that serves as a plugin, mediating the environment-agent interaction in deep reinforcement learning problems. The plugin significantly speeds up the training process of our model. Evaluation on 56 datasets shows that DeepLine outperforms state-of-the-art approaches both in accuracy and in computational cost.
△ Less
Submitted 31 October, 2019;
originally announced November 2019.
-
An Abstraction-Based Framework for Neural Network Verification
Authors:
Yizhak Yisrael Elboher,
Justin Gottschlich,
Guy Katz
Abstract:
Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been proposed. However, these approaches afford limited scalability, and applying them to large networks can be challenging. In th…
▽ More
Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been proposed. However, these approaches afford limited scalability, and applying them to large networks can be challenging. In this paper, we propose a framework that can enhance neural network verification techniques by using over-approximation to reduce the size of the network - thus making it more amenable to verification. We perform the approximation such that if the property holds for the smaller (abstract) network, it holds for the original as well. The over-approximation may be too coarse, in which case the underlying verification tool might return a spurious counterexample. Under such conditions, we perform counterexample-guided refinement to adjust the approximation, and then repeat the process. Our approach is orthogonal to, and can be integrated with, many existing verification techniques. For evaluation purposes, we integrate it with the recently proposed Marabou framework, and observe a significant improvement in Marabou's performance. Our experiments demonstrate the great potential of our approach for verifying larger neural networks.
△ Less
Submitted 21 July, 2020; v1 submitted 31 October, 2019;
originally announced October 2019.
-
Simplifying Neural Networks using Formal Verification
Authors:
Sumathi Gokulanathan,
Alexander Feldsher,
Adi Malca,
Clark Barrett,
Guy Katz
Abstract:
Deep neural network (DNN) verification is an emerging field, with diverse verification engines quickly becoming available. Demonstrating the effectiveness of these engines on real-world DNNs is an important step towards their wider adoption. We present a tool that can leverage existing verification engines in performing a novel application: neural network simplification, through the reduction of t…
▽ More
Deep neural network (DNN) verification is an emerging field, with diverse verification engines quickly becoming available. Demonstrating the effectiveness of these engines on real-world DNNs is an important step towards their wider adoption. We present a tool that can leverage existing verification engines in performing a novel application: neural network simplification, through the reduction of the size of a DNN without harming its accuracy. We report on the work-flow of the simplification process, and demonstrate its potential significance and applicability on a family of real-world DNNs for aircraft collision avoidance, whose sizes we were able to reduce by as much as 10%.
△ Less
Submitted 10 August, 2020; v1 submitted 25 October, 2019;
originally announced October 2019.
-
Convexity, critical points, and connectivity radius
Authors:
Mikhail G. Katz
Abstract:
We study the level sets of the distance function from a boundary point of a convex set in Euclidean space. We provide a lower bound for the range of connectivity of the level sets, in terms of the critical points of the distance function in the sense of Grove-Shiohama-Gromov-Cheeger.
We study the level sets of the distance function from a boundary point of a convex set in Euclidean space. We provide a lower bound for the range of connectivity of the level sets, in terms of the critical points of the distance function in the sense of Grove-Shiohama-Gromov-Cheeger.
△ Less
Submitted 8 January, 2020; v1 submitted 6 October, 2019;
originally announced October 2019.
-
On-the-Fly Construction of Composite Events in Scenario-Based Modeling using Constraint Solvers
Authors:
Guy Katz,
Assaf Marron,
Aviran Sadon,
Gera Weiss
Abstract:
Scenario-Based Programming is a methodology for modeling and constructing complex reactive systems from simple, stand-alone building blocks, called scenarios. These scenarios are designed to model different traits of the system, and can be interwoven together and executed to produce cohesive system behavior. Existing execution frameworks for scenario-based programs allow scenarios to specify their…
▽ More
Scenario-Based Programming is a methodology for modeling and constructing complex reactive systems from simple, stand-alone building blocks, called scenarios. These scenarios are designed to model different traits of the system, and can be interwoven together and executed to produce cohesive system behavior. Existing execution frameworks for scenario-based programs allow scenarios to specify their view of what the system must, may, or must not do only through very strict interfaces. This limits the methodology's expressive power and often prevents users from modeling certain complex requirements. Here, we propose to extend Scenario-Based Programming's execution mechanism to allow scenarios to specify how the system should behave using rich logical constraints. We then leverage modern constraint solvers (such as SAT or SMT solvers) to resolve these constraints at every step of running the system, towards yielding the desired overall system behavior. We provide an implementation of our approach and demonstrate its applicability to various systems that could not be easily modeled in an executable manner by existing Scenario-Based approaches.
△ Less
Submitted 10 October, 2020; v1 submitted 1 September, 2019;
originally announced September 2019.
-
Real polynomials with constrained real divisors. I. Fundamental groups
Authors:
Gabriel Katz,
Boris Shapiro,
Volkmar Welker
Abstract:
In the late 80s, V.~Arnold and V.~Vassiliev initiated the topological study of the space of real univariate polynomials of a given degree d and with no real roots of multiplicity exceeding a given positive integer. Expanding their studies, we consider the spaces of real monic univariate polynomials of degree d whose real divisors avoid sequences of root multiplicities taken from a given poset of c…
▽ More
In the late 80s, V.~Arnold and V.~Vassiliev initiated the topological study of the space of real univariate polynomials of a given degree d and with no real roots of multiplicity exceeding a given positive integer. Expanding their studies, we consider the spaces of real monic univariate polynomials of degree d whose real divisors avoid sequences of root multiplicities taken from a given poset of compositions which is closed under certain natural combinatorial operations. In this paper, we concentrate on the fundamental group of such spaces. We find explicit presentations for the fundamental groups in terms of generators and relations and show that in a number of cases they are free with rank bounded from above by a quadratic function in d. We also show that the fundamental group stabilizes for d large. We further show that the fundamental groups admit an interpretation as special bordisms of immersions of 1-manifolds into the cylinder S^1 \times R, whose images avoid the tangency patterns from the poset with respect to the generators of the cylinder.
△ Less
Submitted 23 August, 2023; v1 submitted 21 August, 2019;
originally announced August 2019.
-
Assessing the Quality of Scientific Papers
Authors:
Roman Vainshtein,
Gilad Katz,
Bracha Shapira,
Lior Rokach
Abstract:
A multitude of factors are responsible for the overall quality of scientific papers, including readability, linguistic quality, fluency,semantic complexity, and of course domain-specific technical factors. These factors vary from one field of study to another. In this paper, we propose a measure and method for assessing the overall quality of the scientific papers in a particular field of study. W…
▽ More
A multitude of factors are responsible for the overall quality of scientific papers, including readability, linguistic quality, fluency,semantic complexity, and of course domain-specific technical factors. These factors vary from one field of study to another. In this paper, we propose a measure and method for assessing the overall quality of the scientific papers in a particular field of study. We evaluate our method in the computer science domain, but it can be applied to other technical and scientific fields.Our method is based on the corpus linguistics technique. This technique enables the extraction of required information and knowledge associated with a specific domain. For this purpose, we have created a large corpus, consisting of papers from very high impact conferences. First, we analyze this corpus in order to extract rich domain-specific terminology and knowledge. Then we use the acquired knowledge to estimate the quality of scientific papers by applying our proposed measure. We examine our measure on high and low scientific impact test corpora. Our results show a significant difference in the measure scores of the high and low impact test corpora. Second, we develop a classifier based on our proposed measure and compare it to the baseline classifier. Our results show that the classifier based on our measure over-performed the baseline classifier. Based on the presented results the proposed measure and the technique can be used for automated assessment of scientific papers.
△ Less
Submitted 12 August, 2019;
originally announced August 2019.
-
19th century real analysis, forward and backward
Authors:
Jacques Bair,
Piotr Blaszczyk,
Peter Heinig,
Vladimir Kanovei,
Mikhail G. Katz
Abstract:
19th century real analysis received a major impetus from Cauchy's work. Cauchy mentions variable quantities, limits, and infinitesimals, but the meaning he attached to these terms is not identical to their modern meaning.
Some Cauchy historians work in a conceptual scheme dominated by an assumption of a teleological nature of the evolution of real analysis toward a preordained outcome. Thus, Gil…
▽ More
19th century real analysis received a major impetus from Cauchy's work. Cauchy mentions variable quantities, limits, and infinitesimals, but the meaning he attached to these terms is not identical to their modern meaning.
Some Cauchy historians work in a conceptual scheme dominated by an assumption of a teleological nature of the evolution of real analysis toward a preordained outcome. Thus, Gilain and Siegmund-Schultze assume that references to limite in Cauchy's work necessarily imply that Cauchy was working with an Archi-medean continuum, whereas infinitesimals were merely a convenient figure of speech, for which Cauchy had in mind a complete justification in terms of Archimedean limits. However, there is another formalisation of Cauchy's procedures exploiting his limite, more consistent with Cauchy's ubiquitous use of infinitesimals, in terms of the standard part principle of modern infinitesimal analysis.
We challenge a misconception according to which Cauchy was allegedly forced to teach infinitesimals at the Ecole Polytechnique. We show that the debate there concerned mainly the issue of rigor, a separate one from infinitesimals. A critique of Cauchy's approach by his contemporary de Prony sheds light on the meaning of rigor to Cauchy and his contemporaries. An attentive reading of Cauchy's work challenges received views on Cauchy's role in the history of analysis, and indicates that he was a pioneer of infinitesimal techniques as much as a harbinger of the Epsilontik.
△ Less
Submitted 17 July, 2019;
originally announced July 2019.
-
On mathematical realism and the applicability of hyperreals
Authors:
Emanuele Bottazzi,
Vladimir Kanovei,
Mikhail G. Katz,
Thomas Mormann,
David Sherry
Abstract:
We argue that Robinson's hyperreals have just as much claim to applicability as the garden variety reals. In a recent text, Easwaran and Towsner (ET) analyze the applicability of mathematical techniques in the sciences, and introduce a distinction between techniques that are applicable and those that are merely instrumental. Unfortunately the authors have not shown that their distinction is a clea…
▽ More
We argue that Robinson's hyperreals have just as much claim to applicability as the garden variety reals. In a recent text, Easwaran and Towsner (ET) analyze the applicability of mathematical techniques in the sciences, and introduce a distinction between techniques that are applicable and those that are merely instrumental. Unfortunately the authors have not shown that their distinction is a clear and fruitful one, as the examples they provide are superficial and unconvincing. Moreover, their analysis is vitiated by a reliance on a naive version of object realism which has long been abandoned by most philosophical realists in favor of truth-value realism. ET's argument against the applicability of hyperreals based on automorphisms of hyperreal models involves massaging the evidence and is similarly unconvincing. The purpose of the ET text is to argue that Robinson's infinitesimal analysis is merely instrumental rather than applicable. Yet in spite of Robinson's techniques being applied in physics, probability, and economics, ET don't bother to provide a meaningful analysis of even a single case in which these techniques are used. Instead, ET produce page after page of speculations mainly imitating Connesian chimera-type arguments `from first principles' against Robinson. In an earlier paper Easwaran endorsed real applicability of the sigma-additivity of measures, whereas the ET text rejects real applicability of the axiom of choice, voicing a preference for ZF. Since it is consistent with ZF that the Lebesgue measure is not sigma-additive, Easwaran is thereby walking back his earlier endorsement. We note a related inaccuracy in the textbook Measure Theory by Paul Halmos.
△ Less
Submitted 30 July, 2019; v1 submitted 16 July, 2019;
originally announced July 2019.
-
Transferable Cost-Aware Security Policy Implementation for Malware Detection Using Deep Reinforcement Learning
Authors:
Yoni Birman,
Shaked Hindi,
Gilad Katz,
Asaf Shabtai
Abstract:
Malware detection is an ever-present challenge for all organizational gatekeepers, who must maintain high detection rates while minimizing interruptions to the organization's workflow. To improve detection rates, organizations often deploy an ensemble of detectors. While effective, this approach is computationally expensive, since every file - even clear-cut cases - needs to be analyzed by all det…
▽ More
Malware detection is an ever-present challenge for all organizational gatekeepers, who must maintain high detection rates while minimizing interruptions to the organization's workflow. To improve detection rates, organizations often deploy an ensemble of detectors. While effective, this approach is computationally expensive, since every file - even clear-cut cases - needs to be analyzed by all detectors. Moreover, with an ever-increasing number of files to process, the use of ensembles may incur unacceptable processing times and costs (e.g., cloud resources). In this study, we propose SPIREL, a reinforcement learning-based method for cost-effective malware detection. Our method enables organizations to directly associate costs to correct/incorrect classification, computing resources and run-time, and then dynamically establishes a security policy. This security policy is then implemented, and for each inspected file, a different set of detectors is assigned and a different detection threshold is set. Our evaluation on two malware domains- Portable Executable (PE) and Android Application Package (APK)files - shows that SPIREL is both accurate and extremely resource-efficient: the proposed method either outperforms the best performing baselines while achieving a modest improvement in efficiency, or reduces the required running time by ~80% while decreasing the accuracy and F1-score by only 0.5%. We also show that our approach is both highly transferable across different datasets and adaptable to changes in individual detector performance.
△ Less
Submitted 20 May, 2020; v1 submitted 25 May, 2019;
originally announced May 2019.
-
New Item Consumption Prediction Using Deep Learning
Authors:
Michael Shekasta,
Gilad Katz,
Asnat Greenstein-Messica,
Lior Rokach,
Bracha Shapira
Abstract:
Recommendation systems have become ubiquitous in today's online world and are an integral part of practically every e-commerce platform. While traditional recommender systems use customer history, this approach is not feasible in 'cold start' scenarios. Such scenarios include the need to produce recommendations for new or unregistered users and the introduction of new items. In this study, we pres…
▽ More
Recommendation systems have become ubiquitous in today's online world and are an integral part of practically every e-commerce platform. While traditional recommender systems use customer history, this approach is not feasible in 'cold start' scenarios. Such scenarios include the need to produce recommendations for new or unregistered users and the introduction of new items. In this study, we present the Purchase Intent Session-bAsed (PISA) algorithm, a content-based algorithm for predicting the purchase intent for cold start session-based scenarios. Our approach employs deep learning techniques both for modeling the content and purchase intent prediction. Our experiments show that PISA outperforms a well-known deep learning baseline when new items are introduced. In addition, while content-based approaches often fail to perform well in highly imbalanced datasets, our approach successfully handles such cases. Finally, our experiments show that combining PISA with the baseline in non-cold start scenarios further improves performance.
△ Less
Submitted 12 May, 2019; v1 submitted 5 May, 2019;
originally announced May 2019.
-
Systolically extremal nonpositively curved surfaces are flat with finitely many singularities
Authors:
Mikhail Katz,
Stephane Sabourau
Abstract:
The regularity of systolically extremal surfaces is a notoriously difficult problem already discussed by M. Gromov in 1983, who proposed an argument toward the existence of $L^2$-extremizers exploiting the theory of $r$-regularity developed by P. A. White and others by the 1950s. We propose to study the problem of systolically extremal metrics in the context of generalized metrics of nonpositive c…
▽ More
The regularity of systolically extremal surfaces is a notoriously difficult problem already discussed by M. Gromov in 1983, who proposed an argument toward the existence of $L^2$-extremizers exploiting the theory of $r$-regularity developed by P. A. White and others by the 1950s. We propose to study the problem of systolically extremal metrics in the context of generalized metrics of nonpositive curvature. A natural approach would be to work in the class of Alexandrov surfaces of finite total curvature, where one can exploit the tools of the completion provided in the context of Radon measures as studied by Reshetnyak and others. However the generalized metrics in this sense still don't have enough regularity. Instead, we develop a more hands-on approach and show that, for each genus, every systolically extremal nonpositively curved surface is piecewise flat with finitely many conical singularities. This result exploits a decomposition of the surface into flat systolic bands and nonsystolic polygonal regions, as well as the combinatorial/topological estimates of Malestein-Rivin-Theran, Przytycki, Aougab-Biringer-Gaster and Greene on the number of curves meeting at most once, combined with a kite excision move. The move merges pairs of conical singularities on a surface of genus $g$ and leads to an asymptotic upper bound $g^{4+ε}$ on the number of singularities.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
Leibniz's well-founded fictions and their interpretations
Authors:
Jacques Bair,
Piotr Blaszczyk,
Robert Ely,
Peter Heinig,
Mikhail G. Katz
Abstract:
Leibniz used the term fiction in conjunction with infinitesimals. What kind of fictions they were exactly is a subject of scholarly dispute. The position of Bos and Mancosu contrasts with that of Ishiguro and Arthur. Leibniz's own views, expressed in his published articles and correspondence, led Bos to distinguish between two methods in Leibniz's work: (A) one exploiting classical `exhaustion' ar…
▽ More
Leibniz used the term fiction in conjunction with infinitesimals. What kind of fictions they were exactly is a subject of scholarly dispute. The position of Bos and Mancosu contrasts with that of Ishiguro and Arthur. Leibniz's own views, expressed in his published articles and correspondence, led Bos to distinguish between two methods in Leibniz's work: (A) one exploiting classical `exhaustion' arguments, and (B) one exploiting inassignable infinitesimals together with a law of continuity. Of particular interest is evidence stemming from Leibniz's work Nouveaux Essais sur l'Entendement Humain as well as from his correspondence with Arnauld, Bignon, Dagincourt, Des Bosses, and Varignon. A careful examination of the evidence leads us to the opposite conclusion from Arthur's. We analyze a hitherto unnoticed objection of Rolle's concerning the lack of justification for extending axioms and operations in geometry and analysis from the ordinary domain to that of infinitesimal calculus, and reactions to it by Saurin and Leibniz. A newly released 1705 manuscript by Leibniz (Puisque des personnes...) currently in the process of digitalisation, sheds light on the nature of Leibnizian inassignable infinitesimals. In a pair of 1695 texts Leibniz made it clear that his incomparable magnitudes violate Euclid's Definition V.4, a.k.a. the Archimedean property, corroborating the non-Archimedean construal of the Leibnizian calculus.
Keywords: Archimedean property; assignable vs inassignable quantity; Euclid's Definition V.4; infinitesimal; law of continuity; law of homogeneity; logical fiction; Nouveaux Essais; pure fiction; quantifier-assisted paraphrase; syncategorematic; transfer principle; Arnauld; Bignon; Des Bosses; Rolle; Saurin; Varignon
△ Less
Submitted 11 February, 2019; v1 submitted 1 December, 2018;
originally announced December 2018.
-
MDGAN: Boosting Anomaly Detection Using \\Multi-Discriminator Generative Adversarial Networks
Authors:
Yotam Intrator,
Gilad Katz,
Asaf Shabtai
Abstract:
Anomaly detection is often considered a challenging field of machine learning due to the difficulty of obtaining anomalous samples for training and the need to obtain a sufficient amount of training data. In recent years, autoencoders have been shown to be effective anomaly detectors that train only on "normal" data. Generative adversarial networks (GANs) have been used to generate additional trai…
▽ More
Anomaly detection is often considered a challenging field of machine learning due to the difficulty of obtaining anomalous samples for training and the need to obtain a sufficient amount of training data. In recent years, autoencoders have been shown to be effective anomaly detectors that train only on "normal" data. Generative adversarial networks (GANs) have been used to generate additional training samples for classifiers, thus making them more accurate and robust. However, in anomaly detection GANs are only used to reconstruct existing samples rather than to generate additional ones. This stems both from the small amount and lack of diversity of anomalous data in most domains. In this study we propose MDGAN, a novel GAN architecture for improving anomaly detection through the generation of additional samples. Our approach uses two discriminators: a dense network for determining whether the generated samples are of sufficient quality (i.e., valid) and an autoencoder that serves as an anomaly detector. MDGAN enables us to reconcile two conflicting goals: 1) generate high-quality samples that can fool the first discriminator, and 2) generate samples that can eventually be effectively reconstructed by the second discriminator, thus improving its performance. Empirical evaluation on a diverse set of datasets demonstrates the merits of our approach.
△ Less
Submitted 11 October, 2018;
originally announced October 2018.
-
The Disk-Based Origami Theorem and a Glimpse of Holography for Traversing Flows
Authors:
Gabriel Katz
Abstract:
This paper describes a mechanism by which a traversally generic flow $v$ on a smooth connected manifold $X$ with boundary produces a compact $CW$-complex $\mathcal T(v)$, which is homotopy equivalent to $X$ and such that $X$ embeds in $\mathcal T(v)\times \mathbf R$. The $CW$-complex $\mathcal T(v)$ captures some residual information about the smooth structure on $X$ (such as the stable tangent bu…
▽ More
This paper describes a mechanism by which a traversally generic flow $v$ on a smooth connected manifold $X$ with boundary produces a compact $CW$-complex $\mathcal T(v)$, which is homotopy equivalent to $X$ and such that $X$ embeds in $\mathcal T(v)\times \mathbf R$. The $CW$-complex $\mathcal T(v)$ captures some residual information about the smooth structure on $X$ (such as the stable tangent bundle of $X$). Moreover, $\mathcal T(v)$ is obtained from a simplicial \emph{origami map} $O: D^n \to \mathcal T(v)$, whose source space is a disk $D^n \subset \partial X$ of dimension $n = \dim(X) -1$. The fibers of $O$ have the cardinality $(n+1)$ at most.
The knowledge of the map $O$, together with the restriction to $D^n$ of a Lyapunov function $f:X \to \mathbf R$ for $v$, make it possible to reconstruct the topological type of the pair $(X, \mathcal F(v))$, were $\mathcal F(v)$ is the $1$-foliation, generated by $v$. This fact motivates the use of "holography" in the title.
△ Less
Submitted 6 October, 2018;
originally announced October 2018.
-
On Holographic Structures, Traversing Flows, and Exotic Spheres
Authors:
Gabriel Katz
Abstract:
Any traversally generic vector flow on a compact manifold $X$ with boundary leaves some residual structure on its boundary $\d X$. A part of this structure is the flow-generated causality map $C_v$, which takes a region of $\d X$ to the complementary region. By the Holography Theorem from \cite{K4}, the map $C_v$ allows to reconstruct $X$ together with the unparametrized flow. The reconstruction i…
▽ More
Any traversally generic vector flow on a compact manifold $X$ with boundary leaves some residual structure on its boundary $\d X$. A part of this structure is the flow-generated causality map $C_v$, which takes a region of $\d X$ to the complementary region. By the Holography Theorem from \cite{K4}, the map $C_v$ allows to reconstruct $X$ together with the unparametrized flow. The reconstruction is a manifestation of holographic description of the flow.
In the paper, we introduce and study the holographic structures on a given closed manifold $Y$, which mimics $\d X$. We generalize the Holography Theorem so that is stated in terms of fillable holographic structures on $Y$. Such structures are intimately linked with traversally generic vector flows on manifolds $X$ whose boundary is $Y$. We conclude with few observations about the richness of holographic structures on smooth exotic spheres.
△ Less
Submitted 27 June, 2018;
originally announced June 2018.
-
A footnote to The crisis in contemporary mathematics
Authors:
Boris Katz,
Mikhail G. Katz,
Sam Sanders
Abstract:
We examine the preparation and context of the paper "The Crisis in Contemporary Mathematics" by Errett Bishop, published 1975 in Historia Mathematica. Bishop tried to moderate the differences between Hilbert and Brouwer with respect to the interpretation of logical connectives and quantifiers. He also commented on Robinson's Non-standard Analysis, fearing that it might lead to what he referred to…
▽ More
We examine the preparation and context of the paper "The Crisis in Contemporary Mathematics" by Errett Bishop, published 1975 in Historia Mathematica. Bishop tried to moderate the differences between Hilbert and Brouwer with respect to the interpretation of logical connectives and quantifiers. He also commented on Robinson's Non-standard Analysis, fearing that it might lead to what he referred to as 'a debasement of meaning.' The 'debasement' comment can already be found in a draft version of Bishop's lecture, but not in the audio file of the actual lecture of 1974. We elucidate the context of the 'debasement' comment and its relation to Bishop's position vis-a-vis the Law of Excluded Middle.
Keywords: Constructive mathematics; Robinson's framework; infinitesimal analysis.
△ Less
Submitted 8 April, 2018;
originally announced April 2018.
-
Klein vs Mehrtens: restoring the reputation of a great modern
Authors:
Jacques Bair,
Piotr BÅ‚aszczyk,
Peter Heinig,
Mikhail G. Katz,
Jan Peter Schäfermeyer,
David Sherry
Abstract:
Historian Herbert Mehrtens sought to portray the history of turn-of-the-century mathematics as a struggle of modern vs countermodern, led respectively by David Hilbert and Felix Klein. Some of Mehrtens' conclusions have been picked up by both historians (Jeremy Gray) and mathematicians (Frank Quinn).
We argue that Klein and Hilbert, both at Goettingen, were not adversaries but rather modernist a…
▽ More
Historian Herbert Mehrtens sought to portray the history of turn-of-the-century mathematics as a struggle of modern vs countermodern, led respectively by David Hilbert and Felix Klein. Some of Mehrtens' conclusions have been picked up by both historians (Jeremy Gray) and mathematicians (Frank Quinn).
We argue that Klein and Hilbert, both at Goettingen, were not adversaries but rather modernist allies in a bid to broaden the scope of mathematics beyond a narrow focus on arithmetized analysis as practiced by the Berlin school.
Klein's Goettingen lecture and other texts shed light on Klein's modernism. Hilbert's views on intuition are closer to Klein's views than Mehrtens is willing to allow. Klein and Hilbert were equally interested in the axiomatisation of physics. Among Klein's credits is hel** launch the career of Abraham Fraenkel, and advancing the careers of Sophus Lie, Emmy Noether, and Ernst Zermelo, all four surely of impeccable modernist credentials.
Mehrtens' unsourced claim that Hilbert was interested in production rather than meaning appears to stem from Mehrtens' marxist leanings. Mehrtens' claim that [the future SS-Brigadefuehrer] "Theodor Vahlen ... cited Klein's racist distinctions within mathematics, and sharpened them into open antisemitism" fabricates a spurious continuity between the two figures mentioned and is thus an odious misrepresentation of Klein's position.
Keywords: arithmetized analysis; axiomatisation of geometry; axiomatisation of physics; formalism; intuition; mathematical realism; modernism; Felix Klein; David Hilbert; Karl Weierstrass
△ Less
Submitted 6 March, 2018;
originally announced March 2018.
-
Monotone subsequence via ultrapower
Authors:
Piotr Blaszczyk,
Vladimir Kanovei,
Mikhail G. Katz,
Tahl Nowik
Abstract:
An ultraproduct can be a helpful organizing principle in presenting solutions of problems at many levels, as argued by Terence Tao. We apply it here to the solution of a calculus problem: every infinite sequence has a monotone infinite subsequence, and give other applications.
Keywords: ordered structures; monotone subsequence; ultrapower; saturation; compactness
An ultraproduct can be a helpful organizing principle in presenting solutions of problems at many levels, as argued by Terence Tao. We apply it here to the solution of a calculus problem: every infinite sequence has a monotone infinite subsequence, and give other applications.
Keywords: ordered structures; monotone subsequence; ultrapower; saturation; compactness
△ Less
Submitted 1 March, 2018;
originally announced March 2018.
-
What makes a theory of infinitesimals useful? A view by Klein and Fraenkel
Authors:
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Thomas Mormann
Abstract:
Felix Klein and Abraham Fraenkel each formulated a criterion for a theory of infinitesimals to be successful, in terms of the feasibility of implementation of the Mean Value Theorem. We explore the evolution of the idea over the past century, and the role of Abraham Robinson's framework therein.
Felix Klein and Abraham Fraenkel each formulated a criterion for a theory of infinitesimals to be successful, in terms of the feasibility of implementation of the Mean Value Theorem. We explore the evolution of the idea over the past century, and the role of Abraham Robinson's framework therein.
△ Less
Submitted 1 February, 2018;
originally announced February 2018.
-
Toward Scalable Verification for Safety-Critical Deep Networks
Authors:
Lindsey Kuper,
Guy Katz,
Justin Gottschlich,
Kyle Julian,
Clark Barrett,
Mykel Kochenderfer
Abstract:
The increasing use of deep neural networks for safety-critical applications, such as autonomous driving and flight control, raises concerns about their safety and reliability. Formal verification can address these concerns by guaranteeing that a deep learning system operates as intended, but the state of the art is limited to small systems. In this work-in-progress report we give an overview of ou…
▽ More
The increasing use of deep neural networks for safety-critical applications, such as autonomous driving and flight control, raises concerns about their safety and reliability. Formal verification can address these concerns by guaranteeing that a deep learning system operates as intended, but the state of the art is limited to small systems. In this work-in-progress report we give an overview of our work on mitigating this difficulty, by pursuing two complementary directions: devising scalable verification techniques, and identifying design choices that result in deep learning systems that are more amenable to verification.
△ Less
Submitted 2 February, 2018; v1 submitted 18 January, 2018;
originally announced January 2018.
-
Fermat's dilemma: Why did he keep mum on infinitesimals? and the European theological context
Authors:
Jacques Bair,
Mikhail G. Katz,
David Sherry
Abstract:
The first half of the 17th century was a time of intellectual ferment when wars of natural philosophy were echoes of religious wars, as we illustrate by a case study of an apparently innocuous mathematical technique called adequality pioneered by the honorable judge Pierre de Fermat, its relation to indivisibles, as well as to other hocus-pocus. Andre Weil noted that simple applications of adequal…
▽ More
The first half of the 17th century was a time of intellectual ferment when wars of natural philosophy were echoes of religious wars, as we illustrate by a case study of an apparently innocuous mathematical technique called adequality pioneered by the honorable judge Pierre de Fermat, its relation to indivisibles, as well as to other hocus-pocus. Andre Weil noted that simple applications of adequality involving polynomials can be treated purely algebraically but more general problems like the cycloid curve cannot be so treated and involve additional tools--leading the mathematician Fermat potentially into troubled waters. Breger attacks Tannery for tampering with Fermat's manuscript but it is Breger who tampers with Fermat's procedure by moving all terms to the left-hand side so as to accord better with Breger's own interpretation emphasizing the double root idea. We provide modern proxies for Fermat's procedures in terms of relations of infinite proximity as well as the standard part function.
Keywords: adequality; atomism; cycloid; hylomorphism; indivisibles; infinitesimal; jesuat; jesuit; Edict of Nantes; Council of Trent 13.2
△ Less
Submitted 1 January, 2018;
originally announced January 2018.
-
Cauchy, infinitesimals and ghosts of departed quantifiers
Authors:
Jacques Bair,
Piotr Blaszczyk,
Robert Ely,
Valerie Henry,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Taras Kudryk,
Semen S. Kutateladze,
Thomas McGaffey,
Thomas Mormann,
David M. Schaps,
David Sherry
Abstract:
Procedures relying on infinitesimals in Leibniz, Euler and Cauchy have been interpreted in both a Weierstrassian and Robinson's frameworks. The latter provides closer proxies for the procedures of the classical masters. Thus, Leibniz's distinction between assignable and inassignable numbers finds a proxy in the distinction between standard and nonstandard numbers in Robinson's framework, while Lei…
▽ More
Procedures relying on infinitesimals in Leibniz, Euler and Cauchy have been interpreted in both a Weierstrassian and Robinson's frameworks. The latter provides closer proxies for the procedures of the classical masters. Thus, Leibniz's distinction between assignable and inassignable numbers finds a proxy in the distinction between standard and nonstandard numbers in Robinson's framework, while Leibniz's law of homogeneity with the implied notion of equality up to negligible terms finds a mathematical formalisation in terms of standard part. It is hard to provide parallel formalisations in a Weierstrassian framework but scholars since Ishiguro have engaged in a quest for ghosts of departed quantifiers to provide a Weierstrassian account for Leibniz's infinitesimals. Euler similarly had notions of equality up to negligible terms, of which he distinguished two types: geometric and arithmetic. Euler routinely used product decompositions into a specific infinite number of factors, and used the binomial formula with an infinite exponent. Such procedures have immediate hyperfinite analogues in Robinson's framework, while in a Weierstrassian framework they can only be reinterpreted by means of paraphrases departing significantly from Euler's own presentation. Cauchy gives lucid definitions of continuity in terms of infinitesimals that find ready formalisations in Robinson's framework but scholars working in a Weierstrassian framework bend over backwards either to claim that Cauchy was vague or to engage in a quest for ghosts of departed quantifiers in his work. Cauchy's procedures in the context of his 1853 sum theorem (for series of continuous functions) are more readily understood from the viewpoint of Robinson's framework, where one can exploit tools such as the pointwise definition of the concept of uniform convergence.
Keywords: historiography; infinitesimal; Latin model; butterfly model
△ Less
Submitted 1 December, 2017;
originally announced December 2017.
-
Applying Gromov's Amenable Localization to Geodesic Flows
Authors:
Gabriel Katz
Abstract:
Let $M$ be a compact smooth Riemannian $n$-manifold with boundary. We combine Gromov's amenable localization technique with the Poincaré duality to study the {\sf traversally generic} geodesic flows on $SM$, the space of the spherical tangent bundle. Such flows generate stratifications of $SM$, governed by rich universal combinatorics. The stratification reflects the ways in which the flow traject…
▽ More
Let $M$ be a compact smooth Riemannian $n$-manifold with boundary. We combine Gromov's amenable localization technique with the Poincaré duality to study the {\sf traversally generic} geodesic flows on $SM$, the space of the spherical tangent bundle. Such flows generate stratifications of $SM$, governed by rich universal combinatorics. The stratification reflects the ways in which the flow trajectories are tangent to the boundary $\partial(SM)$. Specifically, we get lower estimates of the numbers of connected components of these flow-generated strata of any given codimension $k$ in terms of the normed homology $H_k(M; \mathbf R)$ and $H_k(DM; \mathbf R)$, where $DM = M\cup_{\partial M} M$ denotes the double of $M$. The norms here are the {\sf simplicial semi-norms} in homology. The more complex the metric on $M$ is, the more numerous the strata of $SM$ and $S(DM)$ are. %So one may regard our estimates as analogues of the Morse inequalities for the geodesics on manifolds with boundary. It turns out that the normed homology spaces form obstructions to the existence of globally $k$-{\sf convex} traversally generic metrics on $M$. We also prove that knowing the geodesic scattering map on $M$ makes it possible to reconstruct the stratified topological type of the space of geodesics, as well as the amenably localized Poincaré duality operators on $SM$.
△ Less
Submitted 6 October, 2020; v1 submitted 17 October, 2017;
originally announced October 2017.
-
DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks
Authors:
Divya Gopinath,
Guy Katz,
Corina S. Pasareanu,
Clark Barrett
Abstract:
Deep neural networks have become widely used, obtaining remarkable results in domains such as computer vision, speech recognition, natural language processing, audio recognition, social network filtering, machine translation, and bio-informatics, where they have produced results comparable to human experts. However, these networks can be easily fooled by adversarial perturbations: minimal changes…
▽ More
Deep neural networks have become widely used, obtaining remarkable results in domains such as computer vision, speech recognition, natural language processing, audio recognition, social network filtering, machine translation, and bio-informatics, where they have produced results comparable to human experts. However, these networks can be easily fooled by adversarial perturbations: minimal changes to correctly-classified inputs, that cause the network to mis-classify them. This phenomenon represents a concern for both safety and security, but it is currently unclear how to measure a network's robustness against such perturbations. Existing techniques are limited to checking robustness around a few individual input points, providing only very limited guarantees. We propose a novel approach for automatically identifying safe regions of the input space, within which the network is robust against adversarial perturbations. The approach is data-guided, relying on clustering to identify well-defined geometric regions as candidate safe regions. We then utilize verification techniques to confirm that these regions are safe or to provide counter-examples showing that they are not safe. We also introduce the notion of targeted robustness which, for a given target label and region, ensures that a NN does not map any input in the region to the target label. We evaluated our technique on the MNIST dataset and on a neural network implementation of a controller for the next-generation Airborne Collision Avoidance System for unmanned aircraft (ACAS Xu). For these networks, our approach identified multiple regions which were completely safe as well as some which were only safe for specific labels. It also discovered several adversarial perturbations of interest.
△ Less
Submitted 30 January, 2020; v1 submitted 2 October, 2017;
originally announced October 2017.
-
Provably Minimally-Distorted Adversarial Examples
Authors:
Nicholas Carlini,
Guy Katz,
Clark Barrett,
David L. Dill
Abstract:
The ability to deploy neural networks in real-world, safety-critical systems is severely limited by the presence of adversarial examples: slightly perturbed inputs that are misclassified by the network. In recent years, several techniques have been proposed for increasing robustness to adversarial examples --- and yet most of these have been quickly shown to be vulnerable to future attacks. For ex…
▽ More
The ability to deploy neural networks in real-world, safety-critical systems is severely limited by the presence of adversarial examples: slightly perturbed inputs that are misclassified by the network. In recent years, several techniques have been proposed for increasing robustness to adversarial examples --- and yet most of these have been quickly shown to be vulnerable to future attacks. For example, over half of the defenses proposed by papers accepted at ICLR 2018 have already been broken. We propose to address this difficulty through formal verification techniques. We show how to construct provably minimally distorted adversarial examples: given an arbitrary neural network and input sample, we can construct adversarial examples which we prove are of minimal distortion. Using this approach, we demonstrate that one of the recent ICLR defense proposals, adversarial retraining, provably succeeds at increasing the distortion required to construct adversarial examples by a factor of 4.2.
△ Less
Submitted 20 February, 2018; v1 submitted 28 September, 2017;
originally announced September 2017.
-
Towards Proving the Adversarial Robustness of Deep Neural Networks
Authors:
Guy Katz,
Clark Barrett,
David L. Dill,
Kyle Julian,
Mykel J. Kochenderfer
Abstract:
Autonomous vehicles are highly complex systems, required to function reliably in a wide variety of situations. Manually crafting software controllers for these vehicles is difficult, but there has been some success in using deep neural networks generated using machine-learning. However, deep neural networks are opaque to human engineers, rendering their correctness very difficult to prove manually…
▽ More
Autonomous vehicles are highly complex systems, required to function reliably in a wide variety of situations. Manually crafting software controllers for these vehicles is difficult, but there has been some success in using deep neural networks generated using machine-learning. However, deep neural networks are opaque to human engineers, rendering their correctness very difficult to prove manually; and existing automated techniques, which were not designed to operate on neural networks, fail to scale to large systems. This paper focuses on proving the adversarial robustness of deep neural networks, i.e. proving that small perturbations to a correctly-classified input to the network cannot cause it to be misclassified. We describe some of our recent and ongoing work on verifying the adversarial robustness of networks, and discuss some of the open questions we have encountered and how they might be addressed.
△ Less
Submitted 8 September, 2017;
originally announced September 2017.
-
Minimal axiomatic frameworks for definable hyperreals with transfer
Authors:
Frederik S. Herzberg,
Vladimir Kanovei,
Mikhail G. Katz,
Vassily Lyubetsky
Abstract:
We modify the definable ultrapower construction of Kanovei and Shelah (2004) to develop a ZF-definable extension of the continuum with transfer provable using countable choice only, with an additional mild hypothesis on well-ordering implying properness. Under the same assumptions, we also prove the existence of a definable, proper elementary extension of the standard superstructure over the reals…
▽ More
We modify the definable ultrapower construction of Kanovei and Shelah (2004) to develop a ZF-definable extension of the continuum with transfer provable using countable choice only, with an additional mild hypothesis on well-ordering implying properness. Under the same assumptions, we also prove the existence of a definable, proper elementary extension of the standard superstructure over the reals.
Keywords: definability; hyperreal; superstructure; elementary embedding.
△ Less
Submitted 1 July, 2017;
originally announced July 2017.
-
Analyzing Benardete's comment on decimal notation
Authors:
Jacques Bair,
Piotr Blaszczyk,
Karin U. Katz,
Mikhail G. Katz,
Taras Kudryk,
David Sherry
Abstract:
Philosopher Benardete challenged both the conventional wisdom and the received mathematical treatment of zero, dot, nine recurring. An initially puzzling passage in Benardete on the intelligibility of the continuum reveals challenging insights into number systems, the foundations of modern analysis, and mathematics education. A key concept here is, in Terry Tao's terminology, that of an ultralimit…
▽ More
Philosopher Benardete challenged both the conventional wisdom and the received mathematical treatment of zero, dot, nine recurring. An initially puzzling passage in Benardete on the intelligibility of the continuum reveals challenging insights into number systems, the foundations of modern analysis, and mathematics education. A key concept here is, in Terry Tao's terminology, that of an ultralimit.
Keywords: real analysis; infinitesimals; decimal notation; procedures vs ontology
△ Less
Submitted 1 June, 2017;
originally announced June 2017.
-
A positive function with vanishing Lebesgue integral in Zermelo-Fraenkel set theory
Authors:
Vladimir Kanovei,
Mikhail G. Katz
Abstract:
Can a positive function on R have zero Lebesgue integral? It depends on how much choice one has.
Keywords: Lebesgue integral; Zermelo--Fraenkel theory; Feferman-Levy model
Can a positive function on R have zero Lebesgue integral? It depends on how much choice one has.
Keywords: Lebesgue integral; Zermelo--Fraenkel theory; Feferman-Levy model
△ Less
Submitted 1 May, 2017;
originally announced May 2017.
-
Cauchy's infinitesimals, his sum theorem, and foundational paradigms
Authors:
Tiziana Bascelli,
Piotr Blaszczyk,
Alexandre Borovik,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Semen S. Kutateladze,
Thomas McGaffey,
David M. Schaps,
David Sherry
Abstract:
Cauchy's sum theorem is a prototype of what is today a basic result on the convergence of a series of functions in undergraduate analysis. We seek to interpret Cauchy's proof, and discuss the related epistemological questions involved in comparing distinct interpretive paradigms. Cauchy's proof is often interpreted in the modern framework of a Weierstrassian paradigm. We analyze Cauchy's proof clo…
▽ More
Cauchy's sum theorem is a prototype of what is today a basic result on the convergence of a series of functions in undergraduate analysis. We seek to interpret Cauchy's proof, and discuss the related epistemological questions involved in comparing distinct interpretive paradigms. Cauchy's proof is often interpreted in the modern framework of a Weierstrassian paradigm. We analyze Cauchy's proof closely and show that it finds closer proxies in a different modern framework.
Keywords: Cauchy's infinitesimal; sum theorem; quantifier alternation; uniform convergence; foundational paradigms.
△ Less
Submitted 9 May, 2017; v1 submitted 25 April, 2017;
originally announced April 2017.
-
Causal Holography in Application to the Inverse Scattering Problems
Authors:
Gabriel Katz
Abstract:
For a given smooth compact manifold $M$, we introduce an open class $\mathcal G(M)$ of Riemannian metrics, which we call \emph{metrics of the gradient type}. For such metrics $g$, the geodesic flow $v^g$ on the spherical tangent bundle $SM \to M$ admits a Lyapunov function (so the $v^g$-flow is traversing). It turns out, that metrics of the gradient type are exactly the non-trap** metrics.
For…
▽ More
For a given smooth compact manifold $M$, we introduce an open class $\mathcal G(M)$ of Riemannian metrics, which we call \emph{metrics of the gradient type}. For such metrics $g$, the geodesic flow $v^g$ on the spherical tangent bundle $SM \to M$ admits a Lyapunov function (so the $v^g$-flow is traversing). It turns out, that metrics of the gradient type are exactly the non-trap** metrics.
For every $g \in \mathcal G(M)$, the geodesic scattering along the boundary $\partial M$ can be expressed in terms of the \emph{scattering map} $C_{v^g}: \partial_1^+(SM) \to \partial_1^-(SM)$. It acts from a domain $\partial_1^+(SM)$ in the boundary $\partial(SM)$ to the complementary domain $\partial_1^-(SM)$, both domains being diffeomorphic. We prove that, for a \emph{boundary generic} metric $g \in \mathcal G(M)$ the map $C_{v^g}$ allows for a reconstruction of $SM$ and of the geodesic foliation $\mathcal F(v^g)$ on it, up to a homeomorphism (often a diffeomorphism).
Also, for such $g$, the knowledge of the scattering map $C_{v^g}$ makes it possible to recover the homology of $M$, the Gromov simplicial semi-norm on it, and the fundamental group of $M$. Additionally, $C_{v^g}$ allows to reconstruct the naturally stratified topological type of the space of geodesics on $M$.
△ Less
Submitted 11 November, 2018; v1 submitted 26 March, 2017;
originally announced March 2017.
-
Approaches to analysis with infinitesimals following Robinson, Nelson, and others
Authors:
Peter Fletcher,
Karel Hrbacek,
Vladimir Kanovei,
Mikhail G. Katz,
Claude Lobry,
Sam Sanders
Abstract:
This is a survey of several approaches to the framework for working with infinitesimals and infinite numbers, originally developed by Abraham Robinson in the 1960s, and their constructive engagement with the Cantor-Dedekind postulate and the Intended Interpretation hypothesis. We highlight some applications including (1) Loeb's approach to the Lebesgue measure, (2) a radically elementary approach…
▽ More
This is a survey of several approaches to the framework for working with infinitesimals and infinite numbers, originally developed by Abraham Robinson in the 1960s, and their constructive engagement with the Cantor-Dedekind postulate and the Intended Interpretation hypothesis. We highlight some applications including (1) Loeb's approach to the Lebesgue measure, (2) a radically elementary approach to the vibrating string, (3) true infinitesimal differential geometry. We explore the relation of Robinson's and related frameworks to the multiverse view as developed by Hamkins. Keywords: axiomatisations, infinitesimal, nonstandard analysis, ultraproducts, superstructure, set-theoretic foundations, multiverse, naive integers, intuitionism, soritical properties, ideal elements, protozoa.
△ Less
Submitted 1 March, 2017;
originally announced March 2017.
-
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
Authors:
Guy Katz,
Clark Barrett,
David Dill,
Kyle Julian,
Mykel Kochenderfer
Abstract:
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The…
▽ More
Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.
△ Less
Submitted 19 May, 2017; v1 submitted 3 February, 2017;
originally announced February 2017.
-
From Pythagoreans and Weierstrassians to true infinitesimal calculus
Authors:
Mikhail G. Katz,
Luie Polev
Abstract:
In teaching infinitesimal calculus we sought to present basic concepts like continuity and convergence by comparing and contrasting various definitions, rather than presenting "the definition" to the students as a monolithic absolute. We hope that this could be useful to other instructors wishing to follow this method of instruction. A poll run at the conclusion of the course indicates that studen…
▽ More
In teaching infinitesimal calculus we sought to present basic concepts like continuity and convergence by comparing and contrasting various definitions, rather than presenting "the definition" to the students as a monolithic absolute. We hope that this could be useful to other instructors wishing to follow this method of instruction. A poll run at the conclusion of the course indicates that students tend to favor infinitesimal definitions over epsilon, delta ones.
△ Less
Submitted 18 January, 2017;
originally announced January 2017.
-
Gregory's sixth operation
Authors:
Tiziana Bascelli,
Piotr Blaszczyk,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Semen S. Kutateladze,
Tahl Nowik,
David M. Schaps,
David Sherry
Abstract:
In relation to a thesis put forward by Marx Wartofsky, we seek to show that a historiography of mathematics requires an analysis of the ontology of the part of mathematics under scrutiny. Following Ian Hacking, we point out that in the history of mathematics the amount of contingency is larger than is usually thought. As a case study, we analyze the historians' approach to interpreting James Grego…
▽ More
In relation to a thesis put forward by Marx Wartofsky, we seek to show that a historiography of mathematics requires an analysis of the ontology of the part of mathematics under scrutiny. Following Ian Hacking, we point out that in the history of mathematics the amount of contingency is larger than is usually thought. As a case study, we analyze the historians' approach to interpreting James Gregory's expression ultimate terms in his paper attempting to prove the irrationality of pi. Here Gregory referred to the last or ultimate terms of a series. More broadly, we analyze the following questions: which modern framework is more appropriate for interpreting the procedures at work in texts from the early history of infinitesimal analysis? as well as the related question: what is a logical theory that is close to something early modern mathematicians could have used when studying infinite series and quadrature problems? We argue that what has been routinely viewed from the viewpoint of classical analysis as an example of an "unrigorous" practice, in fact finds close procedural proxies in modern infinitesimal theories. We analyze a mix of social and religious reasons that had led to the suppression of both the religious order of Gregory's teacher degli Angeli, and Gregory's books at Venice, in the late 1660s.
△ Less
Submitted 18 December, 2016;
originally announced December 2016.
-
Toward a history of mathematics focused on procedures
Authors:
Piotr Blaszczyk,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Semen S. Kutateladze,
David Sherry
Abstract:
Abraham Robinson's framework for modern infinitesimals was developed half a century ago. It enables a re-evaluation of the procedures of the pioneers of mathematical analysis. Their procedures have been often viewed through the lens of the success of the Weierstrassian foundations. We propose a view without passing through the lens, by means of proxies for such procedures in the modern theory of i…
▽ More
Abraham Robinson's framework for modern infinitesimals was developed half a century ago. It enables a re-evaluation of the procedures of the pioneers of mathematical analysis. Their procedures have been often viewed through the lens of the success of the Weierstrassian foundations. We propose a view without passing through the lens, by means of proxies for such procedures in the modern theory of infinitesimals. The real accomplishments of calculus and analysis had been based primarily on the elaboration of novel techniques for solving problems rather than a quest for ultimate foundations. It may be hopeless to interpret historical foundations in terms of a punctiform continuum, but arguably it is possible to interpret historical techniques and procedures in terms of modern ones. Our proposed formalisations do not mean that Fermat, Gregory, Leibniz, Euler, and Cauchy were pre-Robinsonians, but rather indicate that Robinson's framework is more helpful in understanding their procedures than a Weierstrassian framework.
△ Less
Submitted 15 September, 2016;
originally announced September 2016.
-
A non-standard analysis of a cultural icon: The case of Paul Halmos
Authors:
Piotr Blaszczyk,
Alexandre Borovik,
Vladimir Kanovei,
Mikhail G. Katz,
Taras Kudryk,
Semen S. Kutateladze,
David Sherry
Abstract:
We examine Paul Halmos' comments on category theory, Dedekind cuts, devil worship, logic, and Robinson's infinitesimals. Halmos' scepticism about category theory derives from his philosophical position of naive set-theoretic realism. In the words of an MAA biography, Halmos thought that mathematics is "certainty" and "architecture" yet 20th century logic teaches us is that mathematics is full of u…
▽ More
We examine Paul Halmos' comments on category theory, Dedekind cuts, devil worship, logic, and Robinson's infinitesimals. Halmos' scepticism about category theory derives from his philosophical position of naive set-theoretic realism. In the words of an MAA biography, Halmos thought that mathematics is "certainty" and "architecture" yet 20th century logic teaches us is that mathematics is full of uncertainty or more precisely incompleteness. If the term architecture meant to imply that mathematics is one great solid castle, then modern logic tends to teach us the opposite lession, namely that the castle is floating in midair. Halmos' realism tends to color his judgment of purely scientific aspects of logic and the way it is practiced and applied. He often expressed distaste for nonstandard models, and made a sustained effort to eliminate first-order logic, the logicians' concept of interpretation, and the syntactic vs semantic distinction. He felt that these were vague, and sought to replace them all by his polyadic algebra. Halmos claimed that Robinson's framework is "unnecessary" but Henson and Keisler argue that Robinson's framework allows one to dig deeper into set-theoretic resources than is common in Archimedean mathematics. This can potentially prove theorems not accessible by standard methods, undermining Halmos' criticisms.
Keywords: Archimedean axiom; bridge between discrete and continuous mathematics; hyperreals; incomparable quantities; indispensability; infinity; mathematical realism; Robinson.
△ Less
Submitted 1 July, 2016;
originally announced July 2016.
-
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Authors:
Burak Ekici,
Guy Katz,
Chantal Keller,
Alain Mebsout,
Andrew J. Reynolds,
Cesare Tinelli
Abstract:
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting…
▽ More
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.
△ Less
Submitted 19 June, 2016;
originally announced June 2016.
-
The Mathematical Intelligencer flunks the Olympics
Authors:
Alexander E. Gutman,
Mikhail G. Katz,
Taras S. Kudryk,
Semen S. Kutateladze
Abstract:
The Mathematical Intelligencer recently published a note by Y. Sergeyev that challenges both mathematics and intelligence. We examine Sergeyev's claims concerning his purported Infinity computer. We compare his grossone system with the classical Levi-Civita fields and with the hyperreal framework of A. Robinson, and analyze the related algorithmic issues inevitably arising in any genuine computer…
▽ More
The Mathematical Intelligencer recently published a note by Y. Sergeyev that challenges both mathematics and intelligence. We examine Sergeyev's claims concerning his purported Infinity computer. We compare his grossone system with the classical Levi-Civita fields and with the hyperreal framework of A. Robinson, and analyze the related algorithmic issues inevitably arising in any genuine computer implementation. We show that Sergeyev's grossone system is unnecessary and vague, and that whatever consistent subsystem could be salvaged is subsumed entirely within a stronger and clearer system (IST). Lou Kauffman, who published an article on a grossone, places it squarely outside the historical panorama of ideas dealing with infinity and infinitesimals.
△ Less
Submitted 1 June, 2016;
originally announced June 2016.
-
Is Leibnizian calculus embeddable in first order logic?
Authors:
Piotr Blaszczyk,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Taras Kudryk,
Thomas Mormann,
David Sherry
Abstract:
To explore the extent of embeddability of Leibnizian infinitesimal calculus in first-order logic (FOL) and modern frameworks, we propose to set aside ontological issues and focus on procedural questions. This would enable an account of Leibnizian procedures in a framework limited to FOL with a small number of additional ingredients such as the relation of infinite proximity. If, as we argue here,…
▽ More
To explore the extent of embeddability of Leibnizian infinitesimal calculus in first-order logic (FOL) and modern frameworks, we propose to set aside ontological issues and focus on procedural questions. This would enable an account of Leibnizian procedures in a framework limited to FOL with a small number of additional ingredients such as the relation of infinite proximity. If, as we argue here, first order logic is indeed suitable for develo** modern proxies for the inferential moves found in Leibnizian infinitesimal calculus, then modern infinitesimal frameworks are more appropriate to interpreting Leibnizian infinitesimal calculus than modern Weierstrassian ones.
Keywords: First order logic; infinitesimal calculus; ontology; procedures; Leibniz; Weierstrass; Abraham Robinson
△ Less
Submitted 11 May, 2016;
originally announced May 2016.
-
Interpreting the infinitesimal mathematics of Leibniz and Euler
Authors:
Jacques Bair,
Piotr Blaszczyk,
Robert Ely,
Valerie Henry,
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Semen S. Kutateladze,
Thomas McGaffey,
Patrick Reeder,
David M. Schaps,
David Sherry,
Steven Shnider
Abstract:
We apply Benacerraf's distinction between mathematical ontology and mathematical practice (or the structures mathematicians use in practice) to examine contrasting interpretations of infinitesimal mathematics of the 17th and 18th century, in the work of Bos, Ferraro, Laugwitz, and others. We detect Weierstrass's ghost behind some of the received historiography on Euler's infinitesimal mathematics,…
▽ More
We apply Benacerraf's distinction between mathematical ontology and mathematical practice (or the structures mathematicians use in practice) to examine contrasting interpretations of infinitesimal mathematics of the 17th and 18th century, in the work of Bos, Ferraro, Laugwitz, and others. We detect Weierstrass's ghost behind some of the received historiography on Euler's infinitesimal mathematics, as when Ferraro proposes to understand Euler in terms of a Weierstrassian notion of limit and Fraser declares classical analysis to be a "primary point of reference for understanding the eighteenth-century theories." Meanwhile, scholars like Bos and Laugwitz seek to explore Eulerian methodology, practice, and procedures in a way more faithful to Euler's own.
Euler's use of infinite integers and the associated infinite products is analyzed in the context of his infinite product decomposition for the sine function. Euler's principle of cancellation is compared to the Leibnizian transcendental law of homogeneity. The Leibnizian law of continuity similarly finds echoes in Euler.
We argue that Ferraro's assumption that Euler worked with a classical notion of quantity is symptomatic of a post-Weierstrassian placement of Euler in the Archimedean track for the development of analysis, as well as a blurring of the distinction between the dual tracks noted by Bos. Interpreting Euler in an Archimedean conceptual framework obscures important aspects of Euler's work. Such a framework is profitably replaced by a syntactically more versatile modern infinitesimal framework that provides better proxies for his inferential moves.
Keywords: Archimedean axiom; infinite product; infinitesimal; law of continuity; law of homogeneity; principle of cancellation; procedure; standard part principle; ontology; mathematical practice; Euler; Leibniz
△ Less
Submitted 2 May, 2016;
originally announced May 2016.
-
Quantum thermodynamics in strong coupling: heat transport and refrigeration
Authors:
Gil Katz,
Ronnie Kosloff
Abstract:
The performance characteristics of a heat rectifier and a heat pump are studied in a non Markovian framework. The device is constructed from a molecule connected to a hot and cold reservoir. The heat baths are modelled using the stochastic surrogate Hamiltonian method. The molecule is modelled by an asymmetric double-well potential. Each well is semi-locally connected to a heat bath composed of sp…
▽ More
The performance characteristics of a heat rectifier and a heat pump are studied in a non Markovian framework. The device is constructed from a molecule connected to a hot and cold reservoir. The heat baths are modelled using the stochastic surrogate Hamiltonian method. The molecule is modelled by an asymmetric double-well potential. Each well is semi-locally connected to a heat bath composed of spins. The dynamics is driven by a combined system-bath Hamiltonian. The temperature of the baths is regulated by a secondary spin bath composed of identical spins in thermal equilibrium. A random swap operation exchange spins between the primary and secondary baths. The combined system is studied in various system-bath coupling strengths. In all cases the average heat current always flows from the hot towards the cold bath in accordance to the second law of thermodynamics. The asymmetry of the double well generates a rectifying effect meaning that when the left and right baths are exchanged the heat current follows the hot to cold direction. The heat current is larger when the high frequency is coupled to the hot bath. Adding an external driving field can reverse the transport direction. Such a refrigeration effect is modelled by a periodic driving field in resonance with the frequency difference of the two potential wells. A minimal driving amplitude is required to overcome the heat leak effect. In the strong driving regime the cooling power is non-monotonic with the system-bath coupling.
△ Less
Submitted 1 May, 2016;
originally announced May 2016.
-
A quantitative obstruction to collapsing surfaces
Authors:
Mikhail G. Katz
Abstract:
We provide a quantitative obstruction to collapsing surfaces of genus at least 2 under a lower curvature bound and an upper diameter bound. Keywords: curvature; diameter; volume; filling radius; systole; Gromov-Hausdorff distance
We provide a quantitative obstruction to collapsing surfaces of genus at least 2 under a lower curvature bound and an upper diameter bound. Keywords: curvature; diameter; volume; filling radius; systole; Gromov-Hausdorff distance
△ Less
Submitted 24 October, 2019; v1 submitted 21 April, 2016;
originally announced April 2016.
-
Small oscillations of the pendulum, Euler's method, and adequality
Authors:
Vladimir Kanovei,
Karin U. Katz,
Mikhail G. Katz,
Tahl Nowik
Abstract:
Small oscillations evolved a great deal from Klein to Robinson. We propose a concept of solution of differential equation based on Euler's method with infinitesimal mesh, with well-posedness based on a relation of adequality following Fermat and Leibniz. The result is that the period of infinitesimal oscillations is independent of their amplitude.
Keywords: harmonic motion; infinitesimal; pendul…
▽ More
Small oscillations evolved a great deal from Klein to Robinson. We propose a concept of solution of differential equation based on Euler's method with infinitesimal mesh, with well-posedness based on a relation of adequality following Fermat and Leibniz. The result is that the period of infinitesimal oscillations is independent of their amplitude.
Keywords: harmonic motion; infinitesimal; pendulum; small oscillations
△ Less
Submitted 13 April, 2016;
originally announced April 2016.