arXiv subjects

Jonathan Frankle

Publications and source records attributed to Jonathan Frankle.

39 records · Page 3Linked to original sources

arXiv2019

Dissecting Pruned Neural Networks

Pruning is a standard technique for removing unnecessary structure from a neural network to reduce its storage footprint, computational demands, or energy consumption. Pruning can reduce the parameter-counts of many state-of-the-art neural networks by an order of magnitude without compromising accuracy, meaning these networks contain a vast amount of unnecessary structure. In this paper, we study the relationship between pruning and interpretability. Namely, we consider the effect of removing unnecessary structure on the number of hidden units that learn disentangled representations of human-recognizable concepts as identified by network dissection. We aim to evaluate how the interpretability of pruned neural networks changes as they are compressed. We find that pruning has no detrimental effect on this measure of interpretability until so few parameters remain that accuracy beings to drop. Resnet-50 models trained on ImageNet maintain the same number of interpretable concepts and units until more than 90% of parameters have been pruned.

cs.LG↗

arXiv2019

The Lottery Ticket Hypothesis: Finding Sparse, Trainable Neural Networks

Neural network pruning techniques can reduce the parameter counts of trained networks by over 90%, decreasing storage requirements and improving computational performance of inference without compromising accuracy. However, contemporary experience is that the sparse architectures produced by pruning are difficult to train from the start, which would similarly improve training performance. We find that a standard pruning technique naturally uncovers subnetworks whose initializations made them capable of training effectively. Based on these results, we articulate the "lottery ticket hypothesis:" dense, randomly-initialized, feed-forward networks contain subnetworks ("winning tickets") that - when trained in isolation - reach test accuracy comparable to the original network in a similar number of iterations. The winning tickets we find have won the initialization lottery: their connections have initial weights that make training particularly effective. We present an algorithm to identify winning tickets and a series of experiments that support the lottery ticket hypothesis and the importance of these fortuitous initializations. We consistently find winning tickets that are less than 10-20% of the size of several fully-connected and convolutional feed-forward architectures for MNIST and CIFAR10. Above this size, the winning tickets that we find learn faster than the original network and reach higher test accuracy.

cs.LG↗

arXiv2015

Type-Directed Synthesis of Products

Software synthesis - the process of generating complete, general-purpose programs from specifications - has become a hot research topic in the past few years. For decades the problem was thought to be insurmountable: the search space of possible programs is far too massive to efficiently traverse. Advances in efficient constraint solving have overcome this barrier, enabling a new generation of effective synthesis systems. Most existing systems compile synthesis tasks down to low-level SMT instances, sacrificing high-level semantic information while solving only first-order problems (i.e., filling integer holes). Recent work takes an alternative approach, using the Curry-Howard isomorphism and techniques from automated theorem proving to construct higher-order programs with algebraic datatypes. My thesis involved extending this type-directed synthesis engine to handle product types, which required significant modifications to both the underlying theory and the tool itself. Product types streamline other language features, eliminating variable-arity constructors among other workarounds employed in the original synthesis system. A form of logical conjunction, products are invertible, making it possible to equip the synthesis system with an efficient theorem-proving technique called focusing that eliminates many of the nondeterministic choices inherent in proof search. These theoretical enhancements informed a new version of the type-directed synthesis prototype implementation, which remained performance-competitive with the original synthesizer. A significant advantage of the type-directed synthesis framework is its extensibility; this thesis is a roadmap for future such efforts to increase the expressive power of the system.

cs.PL↗