Abstract Rendering: Computing All that is Seen in Gaussian Splat Scenes

TL;DR

The paper tackles uncertainty propagation in rendering under camera pose and scene variability for Gaussian splat scenes. It introduces AbstractSplat, a linear-relational abstraction pipeline that converts the GaussianSplat rendering steps into linear bounds, uses a Taylor-series approach to bound matrix inverses, and replaces depth-based sorting with an index-free blending mechanism to maintain tight bounds. The method achieves sound, scalable bounds on pixel colors and reports substantial speedups (2–14×) over mesh-based abstract methods while handling up to 750k Gaussians, with tunable tile/batch configurations for memory–time tradeoffs. These contributions enable rigorous uncertainty-aware verification of vision-based systems in dynamic environments and provide techniques potentially transferable to broader rendering problems and safety-critical perception pipelines.

Abstract

We introduce abstract rendering, a method for computing a set of images by rendering a scene from a continuously varying range of camera positions. The resulting abstract image-which encodes an infinite collection of possible renderings-is represented using constraints on the image matrix, enabling rigorous uncertainty propagation through the rendering process. This capability is particularly valuable for the formal verification of vision-based autonomous systems and other safety-critical applications. Our approach operates on Gaussian splat scenes, an emerging representation in computer vision and robotics. We leverage efficient piecewise linear bound propagation to abstract fundamental rendering operations, while addressing key challenges that arise in matrix inversion and depth sorting-two operations not directly amenable to standard approximations. To handle these, we develop novel linear relational abstractions that maintain precision while ensuring computational efficiency. These abstractions not only power our abstract rendering algorithm but also provide broadly applicable tools for other rendering problems. Our implementation, AbstractSplat, is optimized for scalability, handling up to 750k Gaussians while allowing users to balance memory and runtime through tile and batch-based computation. Compared to the only existing abstract image method for mesh-based scenes, AbstractSplat achieves 2-14x speedups while preserving precision. Our results demonstrate that continuous camera motion, rotations, and scene variations can be rigorously analyzed at scale, making abstract rendering a powerful tool for uncertainty-aware vision applications.

Figures (2)

• Figure 1: Renderings of a Gaussian splat scene with a Lego bulldozer (from mildenhall2020nerf). Rendered image before ( Left) and after camera shifts horizontally by 10cm ( Center left). The lower ( Center right) and upper ( Right) bounds on the abstract image computed by our abstract rendering method for the given camera movement. For every pixel, the color in any image generated by the camera movement is guaranteed to lie between the corresponding pixel values in these lower and upper bound images.
• Figure 2: Visualization of a 3D Gaussian Scene: Gaussians are defined in world coordinates (right), transformed into camera coordinates (middle), and projected onto the image plane/pixel coordinates (left). Here, $f$ denotes the focal length, and $\mathsf{uw}[1]$, $\mathsf{uc}[1]$, and $\mathsf{up}[1]$ represent the red Gaussian's mean in the respective coordinate systems.

Theorems & Definitions (4)

• definition thmcounterdefinition
• proposition thmcounterproposition
• corollary thmcountercorollary
• lemma thmcounterlemma