Search for: All records

Large models have shown generalization across datasets for many low-level vision tasks, like depth estimation, but no such general models exist for scene flow. Even though scene flow prediction has wide potential, its practical use is limited because of the lack of generalization of current predictive models. We identify three key challenges and propose solutions for each. First, we create a method that jointly estimates geometry and motion for accurate prediction. Second, we alleviate scene flow data scarcity with a data recipe that affords us 1M annotated training samples across diverse synthetic scenes. Third, we evaluate different parameterizations for scene flow prediction and adopt a natural and effective parameterization. Our model outperforms existing methods as well as baselines built on large-scale models in terms of 3D end-point error, and shows zero-shot generalization to the casually captured videos from DAVIS and the robotic manipulation scenes from RoboTAP. Overall, our approach makes scene flow prediction more practical in-the-wild. Website: https://research.nvidia.com/labs/lpr/zero msf/ 

Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 26% shorter proofs 27% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 31.8% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms. 

Abstract Droplet impact on substrates is the cornerstone of several processes relevant to many industrial applications. Imposing substrate oscillation modifies the impact dynamics and can, therefore, be used to control the ensuing heat, mass, and energy transfer between the substrate and the impacting droplet. Previous research has shown that substrate oscillation strongly influences the spreading behavior of the droplet. In this study, we extend this understanding to examine how substrate oscillations can further modulate the retraction dynamics of the droplet, consequently affecting its long-term behavior, with a particular focus on induced jetting and subsequent breakup. We systematically examine the breakup of jets formed by the recoiling droplet through experimental investigations across a range of oscillation frequencies and amplitudes. Our findings reveal two distinct jet breakup modes: early and late, each governed by different time scales. Subsequently, we present a mechanistic description of the jetting process. Furthermore, we derive a simple scaling analysis based on energy balance to identify the critical condition required for jet breakup. Finally, we compare the experimental data with the scaling analyses to show its efficacy. 

"Important physical observations in rupture dynamics such as static fault friction, short-slip, self-healing, and supershear phenomenon in cracks are studied. A continuum model of rupture dynamics is developed using the field dislocation mechanics (FDM) theory. The energy density function in our model encodes accepted and simple physical facts related to rocks and granular materials under compression. We work within a 2-dimensional ansatz of FDM where the rupture front is allowed to move only in a horizontal fault layer sandwiched between elastic blocks. Damage via the degradation of elastic modulus is allowed to occur only in the fault layer, characterized by the amount of plastic slip. The theory dictates the evolution equation of the plastic shear strain to be a Hamilton-Jacobi (H-J) equation, resulting in the representation of a propagating rupture front. A Central-Upwind scheme is used to solve the H-J equation. The rupture propagation is fully coupled to elastodynamics in the whole domain, and our simulations recover static friction laws as emergent features of our continuum model, without putting in by hand any such discontinuous criteria in our model. Estimates of material parameters of cohesion and friction angle are deduced. Short-slip and slip-weakening (crack-like) behaviors are also reproduced as a function of the degree of damage behind the rupture front. The long-time behavior of a moving rupture front is probed, and it is deduced that the equilibrium profiles under no shear stress are not traveling wave profiles under non-zero shear load in our model. However, it is shown that a traveling wave structure is likely attained in the limit of long times. Finally, a crack-like damage front is driven by an initial impact loading, and it is observed in our numerical simulations that an upper bound to the crack speed is the dilatational wave speed of the material unless the material is put under pre-stressed conditions, in which case supersonic motion can be obtained. Without pre-stress, intersonic (supershear) motion is recovered under appropriate conditions." 

We study the problem of learning under arbitrary distribution shift, where the learner is trained on a labeled set from one distribution but evaluated on a different, potentially adversarially generated test distribution. We focus on two frameworks: PQ learning [GKKM'20], allowing abstention on adversarially generated parts of the test distribution, and TDS learning [KSV'23], permitting abstention on the entire test distribution if distribution shift is detected. All prior known algorithms either rely on learning primitives that are computationally hard even for simple function classes, or end up abstaining entirely even in the presence of a tiny amount of distribution shift. We address both these challenges for natural function classes, including intersections of halfspaces and decision trees, and standard training distributions, including Gaussians. For PQ learning, we give efficient learning algorithms, while for TDS learning, our algorithms can tolerate moderate amounts of distribution shift. At the core of our approach is an improved analysis of spectral outlier-removal techniques from learning with nasty noise. Our analysis can (1) handle arbitrarily large fraction of outliers, which is crucial for handling arbitrary distribution shifts, and (2) obtain stronger bounds on polynomial moments of the distribution after outlier removal, yielding new insights into polynomial regression under distribution shifts. Lastly, our techniques lead to novel results for tolerant testable learning [RV'23], and learning with nasty noise.