![]() |
SSS Abstracts |
![]() |
A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
Monday, October 3rd, 2016 from 12-1 pm in GHC 6501.
Presented by Kuen-Bang Hou (Favonia), CSD
Following recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory, we constructed a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.
Because of the time limit, I will not show the proof of the main theorem, but will demonstrate how this theorem leads to the Freudenthal suspension theorem, an important corollary for understanding higher-dimensional loop structures of spheres.
This is joint work with Eric Finster, Eric Finster, Dan Licata and Peter LeFanu Lumsdaine, and was presented under the same title in LICS 2016.
In partial fulfillment of the Speaking Requirement.
Factors affecting bimanual grasping
Monday, October 10th, 2016 from 12-1 pm in GHC 6501.
Presented by Yuzuko Nakamura, CSD
In daily life, humans often make use of both hands simultaneously (bimanual manipulation). However, it is not known how often people use bimanual manipulation or what factors cause them to use two hands.
In our work, we focus on the simple task of grasping. In particular, we investigate the effect of object size, weight, and position as well as the presence of a balance requirement on whether bimanual grasping is used in a bowl-moving task. Grasp poses are also collected and analyzed. We find that position and balance have a strong effect on bimanual usage, and weight has a weaker effect. Size, weight, and balance (but not position) affect the pose used to grasp the bowls. We conclude that the choice of strategy is most likely determined by stability requirements and the desire to minimize both body rotation and the need to reach across the body.
Finally, I discuss applications of this work to computer graphics and robotics.
In partial fulfillment of the Speaking Requirement.
MXNet: Flexible Deep Learning Framework from Distributed GPU Clouds to Embedded Systems
Friday, October 14th, 2016 from 12-1 pm in GHC 4303.
Presented by Mu Li, CSD
Abstract: This talk will describe MXNet that is a new deep learning framework developed by collaborators from over 10 institutes. It is designed for both flexiblity and optimized performance, with easy to use interfaces in 7 programming languages including Python, Scala and R. We will discuss the technologies to scale out the framework to distributed clouds, in which we can achieve 74x speedup by using 80 M40s, and also memory optimizations to fit into embedded systems like mobile phones.
In Partial Fulfillment of the Speaking Requirement
Reinforcement Learning via Recurrent Convolutional Neural Networks
Monday, October 17th, 2016 from 12-1 pm in GHC 6501.
Presented by Tanmay Shankar, RI
Deep Reinforcement Learning has enabled the learning of policies for complex tasks in partially observable environments, without explicitly learning the underlying model of the tasks. While such model-free methods do achieve considerable performance, they often ignore the structure of task. We present a more natural representation of the solutions to Reinforcement Learning (RL) problems, within 3 Recurrent Convolutional Neural Network (RCNN) architectures to better exploit this inherent structure. The forward passes of each RCNN execute an efficient Value Iteration, propagate beliefs of state in partially observable environments, and choose optimal actions respectively. Applying backpropagation to these RCNNs allows the system to explicitly learn the Transition Model and Reward Function associated with the underlying MDP, serving as an elegant alternative to classical model-based RL. We evaluate the proposed algorithms in simulation, considering a robot planning problem; and demonstrate the capability of our framework to reduce the cost of re-planning, learn accurate MDP models, and finally replan with learnt models to achieve near-optimal policies.
Joint work with Prof. S. K. Dwivedy and Prof. Prithwijit Guha at the Indian Institute of Technology Guwahati, accepted at the International Conference of Pattern Recognition, 2016.
Active Exploration in 3D-rich Planetary Environments
Monday, November 14th, 2016 from 12-1 pm in GHC 6501.
Presented by Wennie Tabib, CSD
Some of the most compelling targets for future science and exploration in our solar system lie in terrain that is inaccessible by state-of-art robots. The presence of water has been confirmed on Martian recurring slope lineae, but these RSLs are located on steep walls and escarpments that are beyond reach of traditional rovers. Dramatic ridges, cracks, craters, crevasses and spires await on icy moons, but these defy existing robot technology. Pits on Mars and the Moon are similarly enticing and challenging. Planetary drones hold the prospect to fly where others cannot roll or climb. Beyond the physical form of mobility, essential innovations include the enabling autonomy required to make these new forms of exploration possible.
This talk will present an active perception and exploration framework that enables planetary robots to efficiently explore rich, significantly 3D environments including pits, caves, RSL, and geysers. The approach seeks to achieve real-time operation on computationally constrained systems while ensuring energy efficient information acquisition. The trajectory generation formulation is based on state-lattice motion primitives and evaluation of the Cauchy-Schwarz Quadratic Mutual Information at each lattice state. Trajectories are selected by maximizing a measure of information gain per expected execution cost (e.g., time or energy). An extension to the exploration framework that considers multi-modal sensing and mapping will also be presented.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
A Game Theoretic Treatment of Peer Grading in MOOCs
Monday, November 21st, 2016 from 12-1 pm in GHC 6501.
Presented by Alejandro Carbonara, CSD
In Massively Open Online Courses (MOOCs) TA resources are limited. In order to deal with this, MOOCs use peer assessments to grade assignments and then use TA resource to check over some of these assignments. We present an extension to the Stackelberg game model that models the challenge involved in allocating the limited TA resource. We discuss what makes this new model difficult difficult, and then we present an algorithm that computes an approximate solution.
Joint work with Anupam Datta, Arunesh Sinha, Yair Zick
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
Incremental Voronoi Diagrams
Monday, December 5th, 2016 from 12-1 pm in GHC 6501.
Presented by Sarah R. Allen, CSD
We study the amortized number of combinatorial changes (edge insertions and removals) needed to update the graph structure of the Voronoi diagram VD(S) (and several variants thereof) of a set S of n sites in the plane as sites are added to the set. To that effect, we define a general update operation for planar graphs that can be used to model the incremental construction of several variants of Voronoi diagrams as well as the incremental construction of an intersection of halfspaces in 3 Dimensional space. We show that the amortized number of edge insertions and removals needed to add a new site to the Voronoi diagram is O(sqrt{n}). A matching Omega(sqrt{n}) combinatorial lower bound is shown, even in the case where the graph representing the Voronoi diagram is a tree. This contrasts with the O(log n) upper bound of Aronov et al. (2006) for farthest-point Voronoi diagrams in the special case where the points are inserted in clockwise order along their convex hull.
We then present a semi-dynamic data structure that maintains the Voronoi diagram of a set S of n sites in convex position. This data structure supports the insertion of a new site p (and hence the addition of its Voronoi cell) and finds the asymptotically minimal number K of edge insertions and removals needed to obtain the diagram of S including p from the diagram of the original S, in time O(K polylog n) worst case, which is O(sqrt{n} ;polylog n) amortized by the aforementioned combinatorial result.
The most distinctive feature of this data structure is that the graph of the Voronoi diagram is maintained explicitly at all times and can be retrieved and traversed in the natural way; this contrasts with other structures supporting nearest neighbor queries in that they do not maintain the Voronoi diagram after each insertion. This structure supports general search operations on the current Voronoi diagram, which can, for example, be used to perform point location queries in the cells of the current Voronoi diagram in O(log n) time, or to determine whether two given sites are neighbors in the Delaunay triangulation
Joint work with Luis Barba, John Iacono, and Stefan Langerman
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
Just Join for Parallel Ordered Sets
Friday, December 9th, 2016 from 12-1 pm in GHC 4303.
Presented by Yihan Sun, CSD
Ordered sets (and maps when data is associated with each key) are one of the most important and useful data types. The set-set functions union, intersection and difference are particularly useful in certain applications. Brown and Tarjan first described an algorithm for these functions, based on 2-3 trees, that meet the optimal O(mlog(n/m + 1)) time bounds in the comparison model (n and m n are the input sizes). Later Adams showed very elegant algorithms for the functions, and others, based on weight-balanced trees. They only require a single function that is specific to the balancing scheme--a function that joins two balanced trees--and hence can be applied to other balancing schemes. Furthermore the algorithms are naturally parallel. However, in the twenty-four years since, no one has shown that the algorithms, sequential or parallel are asymptotically work optimal.
In this paper we show that Adams' algorithms are both work efficient and highly parallel (polylog span) across four different balancing schemes--AVL trees, red-black trees, weight balanced trees and treaps. To do this we use careful, but simple, algorithms for JOIN that maintain certain invariants, and our proof is (mostly) generic across the schemes. To understand how the algorithms perform in practice we have also implemented them (all code except JOIN is generic across the balancing schemes). Interestingly the implementations on all four balancing schemes and three set functions perform similarly in time and speedup (more than 45x on 64 cores). We also compare the performance of our implementation to other existing libraries and algorithms.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.
Web contact: sss+www@cs