Abstract Rendering:  Certified Rendering Under 3D Semantic Uncertainty
Authors: Chenxi Ji
Yangge Li
Xiangru Zhong
Huan Zhang
Sayan Mitra
Venue: NeurIPS 2025 spotlight ()
Keywords: Abstract Rendering
Certifiable Classification
Gaussian Splat
Neural Radiance Field
alpha-beta-CROWN
Primary area: social_and_economic_aspects_of_machine_learning

Abstract: Rendering produces 2D images from 3D scene representations, yet how continuous variations in camera pose and scenes influence these images—and, consequently, downstream visual models—remains underexplored. We introduce **abstract rendering**, a framework that computes provable bounds on all images rendered under continuously varying camera poses and scenes. The resulting abstract image, expressed as a set of constraints over the image matrix, enables rigorous uncertainty propagation through downstream neural networks and thereby supports certification of model behavior under realistic 3D semantic perturbations, far beyond traditional pixel-level noise models. Our approach propagates camera pose uncertainty through each rendering step using efficient piecewise linear bounds, including custom abstractions for three rendering-specific operations—matrix inversion, sorting-based aggregation, and cumulative product summation—not supported by standard tools. Our implementation, ABSTRACTRENDER, targets two state-of-the-art photorealistic scene representations—3D Gaussian Splats and Neural Radiance Fields (NeRF)—and scales to complex scenes with up to 1M Gaussians. Our computed abstract images achieve up to 3% over-approximation error compared to sampling results (baseline). Through experiments on classification (ResNet), object detection (YOLO), and pose estimation (GATENet) tasks, we demonstrate that abstract rendering enables formal certification of downstream models under realistic 3D variations—an essential step toward safety-critical vision systems.

Abstract Rendering: Certified Rendering Under 3D Semantic Uncertainty
Chenxi Ji; Yangge Li, Xiangru Zhong, Huan Zhang, Sayan Mitra University of Illinois Urbana-Champaign {chenxij2, 1i213, xiangru4, huanz, mitras)@illinois edu
Abstract
Rendering produces 2D images from 3D scene representations, yet how continuous variations in camera pose and scenes influence these images-and andd, consequently, downstream visual medell--remains underexplored. We introduce abstract ren- dering, framework that computes provable bounds on all images rendered under continuously varying camera poses and scenes. The resulting abstract image, ex- pressed as set of constraints over the image matrix, enables rigorous uncertainty propagation through downstream neural networks and thereby supports certification of model behavior under realistic 3D semantic perturbations, far beyond traditional pixel-level noise models. Our approach propagates camera pose uncertainty through each rendering step using efficient piecewise lincar bounds, including custom ab- stractions for three rendering-spene -ppeinii- operations- matrix inversion, sorting- based aggregation, and cumulative product summation not supported by standard tools. Our implementation, ABSTRACTRENDER, targets two state-of-the- photore- alistic scene representations 3D Gaussian Splats and Neural Radiance Fields (NeRF) and scales to complex scenes with up to IM Gaussians. Our computed abstract images achieve up 3% over-approximation results (baseline). Through experiments on classification (ResNet), object detec- tion (YOLO), and pose estimation (GATENet) tasks, we demonstrate that abstract rendering enables formal certification of downstream models under realistic 3D variations-an an essential step toward safety-critical vision systems.
compared to sampling
Introduction
Rendering produces 2D images from 3D scenes and underpins visual computing. Two prominent neural scene representations
Gaussian Splats [ and Neural Radiance Fields (NeRFs) (2). Gaussian Splats represent a scene as a collection of 3D Gaussians whose colors are blended after projection onto the image plane, whereas NeRFs encode scenes neural networks mapping 3D positions and viewing directions to color and density, rendered via ray casting and volumetric integration. These methods exemplify rasterization- and may-casting-basee paradigms that achieve photorealistic reconstruction and novel-view synthesis [3]. However, rigorous analysis of how variations in camera pose scene geometry affect the rendered outputs-and consequently the predictions of downstream models such as classifiers, object detectors, and pose estimators- limited, leaving the robustness of vision systems under realistic 3D perturbations largely unexplored.
Although formal verification has been extensively developed for standalone neural networks 5) verifying rendering pipelines poses fundamentally different challenge. A recent work [6] considers version of this problem for simpler mesh- based scenes, but a general treatment remains open. Formal verification of rendering seeks to compute the set of all possible images generated under continuous variations in camera pose and scene. When coupled with downstream perception models this enables guarantees like "no misclassification occurs during camera panning within specified range" or
Equua contribution.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

"the relative pose error remains bounded within tolerance across viewpoints." Such guarantees are crucial for safety-critical applications 77 including aircraft auto-landing & and formation- (rmation-fligh()) Verifying rendering is challenging because ray ray-casting and rasterization involve neural components, volumetric integration, and nonsmooth operations such as sorting. Consequently, reasoning about rendering requires composing verification techniques across heterogeneous computational layers, capability absent from existing frameworks.
In this paper, we introduce Abstract Rendering, a method for computing the set of all possible images rendered from a continuously varying range of camera poses looking a scene with a range variations. This set of images, referred to as an Abstract Image. is compactly represented using constraints on the image matrix, such as interval or linear bounds. This computed abstract image can then be passed through an existing neural network verification tool 4 to verify models for visual tasks. Our framework illustrated in Figure [ with representative results in Figure 4 For example, consider a ResNet classifier downstream of a camera rotating 360 around an airplane in 3D scene; our method certifies the subrange of viewing angles over which the airplane is classified correctly.
Our framework: Abstract Rendering + Downstream Certification
Douar: (0.75.0.)
Chain (0,05.22)
Tral:: [0.25.0.8]
3D scene Camera poses (with uncortaintyl
Abstract Rendering (bound propagation)
Abstract image (lower upper bound)
Downstream Network Class Scores
(bound propagation) (lawer and upper bound)
Pipeline of applying abstract rendering to certify downstream network. A range of camera pose uncertainty in NeRF scene (Left) is propagated step step through the rendering process (Left Mid) to produce abstract images (Mid). These abstract images then passed through the downstream network layer by layer (Right Mid), yielding per-class output bounds (Right). For classification, if the lower bound of the Dozer class exceeds the upper bounds of all other classes, the prediction is certified under the given camera uncertainty.
Figure 1:
Our abstract rendering algorithm applies linear sets represent and propagate uncertainties from camera pose and scene parameters, through the rendering pipeline. By decomposing the rendering process into composition of basic operations, we develop linear bound propagation rules that maintain tight output bounds when transforming linear input sets. This compositional approach ultimately produces an abstract image that preserves uncertainty information. To optimize the trade-off between for handling standard bound precision and computational efficiency, we adopt CROWN [10 11 operations like division and matrix multiplication.
However, certain operators in the rendering process lack native support. To address this, we develop novel linear bound propagation techniques for three rendering-specific operations: matrix inversion, sorting- based aggregation, and cumulative product summation. For matrix inversion required in computing projected 2D Gaussian probability densities, our Taylor series-based approximation produces tighter linear bounds than standard adjugate methods. Sorting- based aggregation, critical for occlusion determination between Gaussians, reformulated as an equivalent indicator-basee process to mitigate over-approximation caused by independently bounding sorted outputs while ignoring index mutual exclusivity. Cumulative product summation, used in opacity/occlusion-we weighteed value aggregation, employs an ordered strategy that significantly improves bound tightness (particularly beyond 1,000 terms) at moderate computational expense.
In summary, our key contributions are as follows. (1) We introduce the first abstract rendering algorithm to compute abstract images for scenes represented by Gaussian Splats and NeRFs under semantic variations in the 3D world. (2) We develop a unified mathematical and software frame- work for abstracting rendering pipelines, with novel techniques for matrix inversion, sorting- based aggregation, and cumulative product summation, extending beyond what is supported by existing tools like CROWN. (3) We integrate abstract rendering with neural network verification tool CROWN, to certify visual tasks such image classification, pose estimation, and object detection, enabling statements like: "Across camera viewpoints or scene variations, the target model consistently classifies, estimates, detects object within specified error bounds."
2

---

2
Related Work
The only closely related work computes abstract images for triangular mesh scenes (6. To handle camera-pose uncertainty, that method collects each pixel's RGB values into intervals over all possible viewpoints. In practice, this amounts to computing partial interval depth-images for each triangle and merging them using depth-based union, resulting in an interval image that over-approximates all concrete images for that region of poses. This work considers only camera translations, not rotations. Our method works with Gaussian splatting or NeRF which involve more complex operations and are learnable.
including SMT- based approaches 17 and MIP-based techniques [18]. Among these, linear bound propagation has emerged as a prominent strategy, leveraging linear relaxations of nonlinear activations and propagating these bounds layer-wise to efficiently compute output guarantees [19 I 20]. Researchers have further advanced the field by introducing complex geometric abstractions such as polyhedra [2I], zonotopes [22], and starsets [T6] 14. However, our work diverges conceptually from traditional neural network verification: rather than verifying neural networks themselves. focus verifying a broader algorithmic framework that embeds neural networks as components. Crucially, many operations encountered in this context, such matrix inverse, sorting cumulative product, not handled by existing neural network verification tools, necessitating novel theoretical and technical innovations.
Numerous methods exist in neural network verification 5 12
13
14
15
Adversarial robustness has been studied most deeply for pixel-space perturbations, where attacks 23
24
25 image, Follow-up work broadened the threat model to 2D semantic transforms (29 30 31
26,
27 and certificates 20 J4] 66 28 are constrained to small Ip balls around the original
33
40], including global hue or brightness shifts, in-plane rotations, trans laissatioos, elastic warps, but still treats the scene as rigid 2D grid. Our method, instead, handles semantic, 3D
14
35
36
37
38
39)
perturbations that stem from changing the camera pose itself (e.g., orbiting translating the camera around a fixed object), which jointly affect all pixels in a niewpoint-consitten manner.
synthesizes 3D-printable adversarial objects that fool classifiers over many viewpoints, yet offer no formal guarantee of success across the entire pose distribution. Camera- Motion Smoothing (CMS) by Hu [42 provides the first certificates for small six-DoF camera perturbations via randomized smoothing, but relies on dense point-cloud supervision and is restricted to narrow pose radii. In Hu's 's later work (43, he partitions pose space and smooths in the image domain to improve efficiency, yet still yields conservative bounds over only modest displacements. View-Invariant. Adversarial Perturbations (VIAP) 44 craft attacks that remain effective across multiple viewpoints, but-as as with Athalye et al.- d..-provide no certification. Our approach is the first to deliver tight, end-to-end formal guarantees for standard vision networks across a full 360 camera sweep with realistic rendering.
Only handful of papers explore this regime. Athalye 41
3 Preliminaries: Linear Approximations and Rendering Algorithms
Abstract Rendering bounds uncertainty in rendered images by propagating linear bound through each operation within the rendering pipeline. In this section, we delineate the fundamental operations integral to rendering algorithms and demonstrate their amenability to tight linear aperaapproximations Subsequently, we provide an overview of two prominent neural rendering techniques: 3D Gaussian Splatting and Neural Radiance Fields (NeRF).
3.1 Linear Over-approximabiliyy
Notations. For vectors or matrices æ, y of the same shape, x < y denotes element-wise comparison. The Frobenius norm of a vector or matrix is denoted by ||æ||. Boldface (e.g.. pc) indicates set- valued variables, while non-bold (c.g.. pc) denotes fixed values. A linear set (or polytope) is defined as {x E R" Ar < b), where Ar < b specifies linear constraints. A piecewise linear relation has the form {<x,)) v) Ar + b < y S Ax + 5, Ax S b). where A, A, b. define linear bounds on y given x. A constant relation
R C
Rd x R
special case where We consider class functions that can be tightly overaapproximated by piecewise linear lower and upper bounds over any compact input domain.
A 0.
3

---

Definition 1. A function f S - R is called linearly over wer-approximable if. for any compact X C S and 0, there exist piecewise linear maps xx, ux X I. such that for all æ E X, (x(x) S (z) S ux (x) and (wx(2) 110--xx1 (x(x) <.
Proposition 1. Any continuous functtonn is linearly over-approximable
Although Proposition I implies piecewise linear bounds on continuous functions can be adjusted sufficiently tight by shrinking the neighborhood, finding accurate bounds over larger neighborhoods remains significant challenge. Our implementation of abstract rendering employs CROWN [IO] for computing such bounds. Except for Ind and Sort, all the basic operations listed in Table are continuous and therefore linearly over-approximable. Moreover, since Ind is piecewise constant function, it can be tightly bounded on each subdomain by partitioning at x = 0, allowing it to be treated as a linearly over-approximable function. This formalized in Corollary
Corollary 1. All operations in Table 7 except for Sort, are linearly over-approximable
Table 1: Basic Operation Table. Conditional A?B : returns B if A is true and otherwise C. Permuting x based means reordering the elements of according to the indices that sort y in ascending order. E.g.. permuting (9,3, 7) based on (5, 13, 8) results in (9, 7,3).
Operation
Inputs
Output
Math Representation
Element-wise add (Add)
xr y E IRaxm
E Raxm
Fig = Tay yhj
Element-wise multiply (Mul)
3r y E IRaxm
E Raxm
2ij = Taj" Vkj
Division (Div)
x E RS0
2 E Ruxm
2y = 1 1/203
Matrix multiplication (Mmul)
E Roxm, y Renk
E R
2 y
Matrix inverse (Inv)
x E RTx", det(x) # #0
& E RO*
$ = x 1
Matrix power (Pow)
C gaxp lk C N
RaxD
2
Summation (Sum)
E R"
e R
2 A 22
Product (Prod)
E R"
B R
2 I
Matrix transpose (T)
x C Raxm
2 C RMXX
Jj = TTj
Element-wise exponential (Exp)
C 1
C Raxm
4j C
Frobenius norm (Norm)
I' E Raxm
R20
= |
Element-wise indicator (Ind)
& C Raxm
2 C Rixm
4j (nn > 0)?1: :0
Sorting (Sort)
E R"
RD 1 ER" R""
permute based y
3.2 Rendering Algorithms: Gaussian Splat and NeRF
Scenes and Camera Model A 3D Gaussian scene ScG is defined as a finite collection of 3D Gaussians in world coordinate frame w indexed by I. Each 3D Gaussian specified by its mean Mw. covariance Σw, opacity and RGB color c. For simplicity, we use RGB instead of spherical harmonics to represent 3D Gaussians' colors. A neural radiance field ScN consists of an opacity network F. mapping 3D points to opacity, a color network F. mapping 3D points and view directions to color, maximum sampling distance and sampling count N. A camera is characterized by translation T E R33 rotation R 3x3 focal lengths (fx, fy) E RR² and principal point offsets (Gx, cy) 2
Gaussian Splat rendering Algorithm takes a Gaussian scene ScG, camera C and a pixel coordinate and outputs the rendered RGB value pc at pixel u. Rendering proceeds in four steps: (1) it transforms 3D Gaussians from world to camera coordinate (Ht. Σz) (Line 3): (2) projects 3D Gaussians onto image plane (Hp. Σ,) and computes its weighed probability density at pixel
(Line 4 10 (3) it sorts the Gaussians according to the distance of their means to the image plane
(Line 11 ; (4) it computes pc by aggregating the colors of all Gaussians weighted according to
their relative positions (Line 16 18). The full image is rendered by applying GAUSSIANSPLAT at
every pixel location.
NeRF rendering Algorithm 2 takes as input a neural radiance field ScN, a camera C, and pixel coordinate u, and outputs the rendered RGB value pc at that pixel. The rendering proceeds in three steps: (1) it computes the normalized direction of the camera ray dir, corresponding N points x along the ray within the maximum range L (Line 4 (2) it evaluates the opacity and
and samples

---

Algorithm 2 NERF(ScN, C, u)
Algorithm 1 GAUSSIANSPLAT C,
for all do
1: dir.
4.-
F
by
2:
Mc
R
(now)
T)
2: dirw
dir.xR
3:
R
X
Iw
dirrll
3:
for all
E raagg((N) do
4:
K[]]
p=li.2
4:
x[i
<- T (2i (2i-1)-.de D.L.dir.
0
2N
[12
5:
c
f- Fx dirw)
Me[R.2]
0
M. 1.2
6:
oli
f Fx((l
5:
0
7:
ali]
+ Exp
ofi-
(.22
N
6:
Mp_i
K M
8: ocli] |1 (1 ali))
7:
Σp J[i] x Σ. J[i]
9: end for
8:
Conic[i] + Inv (2p))
10: pc - (ocli) ai] <(i))
9:
qii + (u-MP[ii
x Conic[i] x (u Mpli)
11: return pc
10:
al
+ - -
11: dii
2c]
Algorithm 3 MATRIXINV(X. Xref, k)
12: end for
as Sort(a, d)
1: AX (X Xref)
Xxel
2: assert |4X|| <
14: cs + Sort
for all do
3: Xp <- Σi=o X-1 x Pow Pow(AX,i)
16: octi] - j=1 asii)
4: XR <- ||x|=||| 1-1|aXI
17: end for
5: IXinv <- Xp XR
pc EE [
asii] cs(i))
6: uXinv t- Xp + XR
19: return
7: return (IXinv, uXinv)
color of each sampled point using the networks F. and F. (Line 6 (3) it aggregates the colors along the ray by computing weighted sum based on the opacity and depth ordering of the samples (Line I0
Having introduced two representative rendering algorithms, we now present a formal definition of abstract rendering.
Abstract rendering problem. Our goal is to design an algorithm that for all pixel u E WH, it takes input a linear of scenes Se and cameras C, and outputs linear set of pixel color pc such that GAUSSIANSPLAT(SC, C, C,u)
E pe or NERF(Sc, C, E pc) for each Sc E Sc and C E C.
Methodology: Abstract Rendering
Our abstract rendering algorithm processes scene and camera inputs by incrementally building piecewise linear relations berween intermediate variables and inputs through standard rendering steps, proceeding until pixel-input relationships are established. These relations enable linear bound computation for each pixel, yielding linear bound for image. Since most GAUSSIANSPLAN and NERF operations are linear, their relations compose directly. In this section, we highlight three rendering- specific nonlinear operations (matrix inverse, sorting-based aggregation and cumulative product summation) and introduce tailored techniques tightly bound them with linear over-approximations.
4.1
Abstracting Matrix Inverse by Taylor Series
Bounding matrix inversion (Line 8 of GAUSSIANŠPL.N via the adjugate method often introduces significant over-approximation due uncertainty in the denominator. To address this, we propose Taylor series-based algorithm, MATRIXINV (Algorithm 3. which reformulates matrix inversion using only addition, multiplication, and the inverse of fixed reference matrix. Although the remainder term still involves division, its influence diminishes the Taylor order increases.
TThe adjugate method computes the inverse the adjugate matrix divided by the determinant.
5

---

Algorithm 4 VR-IND(a, c,
Algorithm 5 SUMCUMPROD(a.c)
1: for all E do
pc < [0, 0,
2: oc[ < | (1 -0--al ali] Ind -
2: for all E reverse do
3: end for
pc <- ali] .cli + (1 ali)) pc
4: pc f - (ocli) a[]] cli))
4: end for
5: return pc
return pc
MATRIXINV takes a non-singular matrix X, a non-singular reference matrix X and a Taylor order k as imput, and returns lower and upper bounds IXinv and uXinv for X- The algorithm first checks the convergence condition (Line 2). then computes the k-th order Taylor approximation and its remainder (Lines and finally derives bounds via basic addition and subtraction (Lines 6
Given any non-singular matrix X, the output of Algorithm MATRIXINV (IXinv, uXinv) satisfies that: IXinv < Inv(X)= I uXinv.
Lemma 1.
Lemma D guarantees that MATRIXINV yields valid bounds for the Inv operation with fixed input. When extended to a linear set of input matrices, the linear bounds of IXinv and uXinv can be obtained by propagating linear relations line by line. Their union defines the overall linear bounds for the inversion. Example illlusrates the advantage of using MATRIXINY over the adjugate method in terms of bound tightness.
Example 1. Given the constant lower and upper bounds of input matrices,
0.60
-0.2
[0..0 0.02
0.00
0.90
=
0.02
1.30
we combine lower bound of IXinv and upper bound of uXinv as overall bounds for luv operation. and take |uXinn- IXinv|| measurement for bound tightness. The adjugate method yields bound width of 1.22, while MATRIXINV reduces it to 0.70, closely matching the empirical value of 0.66.
4.2 Abstracting Sorting- Summation by Indicator
The sorting step in Lines 13 14 of GAUSSIANSPLAT models occlusion: front Gaussian occludes those behind, but not vice versa. Bounding sorted elements independently introduces large over- approximations in the final pixel color (Line 18), as it neglects the inherent ordering constraint. To mitigate this, we introduce VR-IND (Algorithm 4. which replaces sorting with pairwise indicator- based occlusion modeling. This approach preserves the output while significantly improving bound tightness in linear relaxation.
Lemma 2.
For any given imputs effective opacities a, colors and depth d, VR-IND outputs the same value as computation from Line 73 Line 78 in GAUSSIANSPLAT.
Lemma 2 confirms that VR-IND produces the same output as Lines B 18 in GAUSSIANSPLAT. capturing both occlusion (Line Z and color aggregation (Line 4 without explicit sorting. Example 2 further demonstrates its advantage in reducing over-approximation
Example 2. Consider scene with three Gaussians (red, green, blue) and camera the origin facing upward, with each coordinate perturbed by +0.3. As shown in Figure 2 the upper bound obtained via linear relaxation through VR-IND is significantly tighter than that derived from direct bound propagation through GAUSSIANSPLATT An analytical example is given in Appendix A
4.3 Abstract Summation of Cumulative Product
The summation of cumulative products arises in Lines 8 10 of NERF, where occlusion effects are computed and colors are aggregated produce the final pixel color. Naively bounding each element of oc independently and then aggregating can lead to significant over-approximation since the intermediate terms a are shared across multiple entries. To mitigate this, we propose a factorization- based formulation, SUMCUMPROD (A (Algorithm 5) which computes each element of only once in the final expression for pc. This approach preserves exactness for fixed inputs while enabling substantially tighter bounds during linear relaxation.
Lemma 3. For any given inputs- - effective opacities a, colors c, SUMCUMPROD outputs the same
value computation from Line 8 to Line 10 in NERF.

---

Figure 2: Example (1cft) shows the three-Gaussian
Gaussian scene. The corresponding upper bounds are visualized follows: via GAUSSIANSPLAT (mid-left), via VR-IND (mid-right), and sampling (right). Notably, the bounds produced by VR-IND are tighter (darker) and closely align with the sampled results.
Lemma confirms that, for fixed imput, SUMCUMPROD exactly reproduces the original NERF output without explicitly computing occlusion for each sampled point. Example 3 shows that it produces much tighter bounds than the standard method. However, SUMCUMPROD has two limitations: (I) its recursive structure necessitates iterative bound propagation, thereby increasing computational cost; (2) it assumes fixed order of restricting its applicability Gaussian-representee scenes where the Gaussian depth order remains unchanged, such as in scenarios involving camera translation uncertainty.
Example 3. Consider single-channel color [0.8, 1.0, and effective opacity [0.2, 0.5, 0.6, 0.8, 0.1] with +0.1 perturbations on each ali]. SUMCUMPROD yields a light bound on outpul pixel color, [0.826, 0.926). versus a looser [0.780, 1. 1.029] from Lines T0 of NERF. Sampling 10,000 random perturbations gives (0.33, closely matching the result from SUMCUMPROD.
4.4 Linear Approximability of ABSTRACTRENDER
The operations in MATRIXINV, VR-IND, and SUMCUMPROD fall within those listed in Table I Since sorting can be eliminated using VR-IND, and all remaining operations are linear over- approximable, we arrive at Theorem I It states that both GAUSSIANSPLAT and NERF can be rewritten using only linearly approximable operations, enabling computation of tight bounds via input domain partitioning.
Theorem 1. By replacing components of GAUSSIANSPLAT and NERF with MATRIXINV, VR-IND, and SUMCUMPROD, both rendering algorithms are fully linear over-approximable.
5 Experiments with Abstract Rendering
We implemented the abstract rendering algorithm ABSTRACTRENDER described in Section with both GAUSSIANSPLAT and NERF. As mentioned earlier, the linear approximation of the continuous operations in Table i implemented using CROWN [10].
Scene Description. We evaluate ABSTRACTRENDES on scenes of varying scales and complexities, represented using GAUSSIANSPLAY and NERF. The scenes include: Lego, Chair, and Drums (2]. which are single-object scenes on empty backgrounds; PineTree (6) a synthetic boulevard scene with trees; Airport [8], large-scale photorealistic airport environment; Garden M. real-world scene; and Airplane, Truck, and Car, containing objects corresponding to CIFAR-I0 10 classes. GAUSSIANSPLAT reconstructions are generated using Splatfacto [45). while those of NERF are trained with the vanilla NERF algorithm (2), both implemented with standard Nerfstudio settings. Further details of these scenes are provided in the appendix.
Experimental Setup. For each scene, evaluate poses and input perturbations. As baseline, we construct empirical bound images by (1) sampling 50 images per input partition (the full perturbation range divided into hundreds thousands of partitions) and (2) computing pixel-wise lower and upper bounds across the samples. Since exhaustive enumeration infeasible, these empirical bound images are under-approximations of the exact set of renderable images, whereas our framework provides sound over-approximations The proximity of ABSTRACTRENDEE results the empirical bound images indicates the tightness of our computed bounds.
under varying camera
7

---

Metrics and Evaluation. To measure the tightness between the pixel-wise lower and upper bound images, we report Mean Pixel Gap (MPG) and Max Pixel Gap (XPG), defined as:
MPG
pall,
XPG
max je WH
PG
Pc
WH
JEWH
where PCj and PG denote the pixel-wise upper and lower bounds, and WH represents the set all pixel coordinates on the image plane. Smaller values of MPG or XPG indicate a smaller difference between summarizes the results across different scene represen- Visualizes the comparison between A ABSTR ACTRENDER results and empirical bounds for two scenes: Airplane and Lego.
the lower and upper bound images. Table 2
tations and perturbations, while Figure 3
Table 2:
results for scenes represented by GAUSSIANSPLAT (GS) and NERF,
along with empirical bounds. CPR: Camera Perturbation Range; Dim: Perturbation Dimension; Res:
Rendered Image Resolution; Rt; Runtime (min); MPG: mean pixel gap; XPG: maximum pixel gap.
GS
NeRF
Empirical
Scene
CPR
Dim
Res
Rt
MPG
XPG
Rt
MPG
XPG
MPG XPG
Lego
0.1 (rad)
yaw
80x80
22
0.51
1.73
25
0.40
1.73
0.22
1.57
Chair
0.1 (rad)
yaw
50x50
17
0.46
1.73
0.40
1.73
0.40
1.72
Drums
0.1 (m)
X
50x50
5.3
0.19
1.62
5.8
0.16
1.55
0.13
1.54
PineTTree
(m)
x
72x72
4.1
0.27
1.73
0.23
1.73
0.06
1.37
Pine'Tree
10 (m)
X
72x72
24 0.47
1.73
28
0.36
1.73
0.18
1.37
Airport
0.027 (rad)
roll
160x 160
27
0.56
1.69
0.42
1.63
0.21
1.38
Airport
0.03 (rad)
roll
160x
160
30
0.59
1.70
43
0.51
1.68
0.22
1.41
Garden
0.5 (m)
x
100x 100
20
0.53
1.59
0.37
1.53
0.34
1.21
Airplane
2 (m)
x
80x80
16
0.41
1.68
19
0.33
1.61
0.15
1.39
AbstractRender Results
Empirical Results
Airplane
Lego
Comparison of lower and upper images produced by ABSTRACTRENDI (Left) and empirical approach (Right). The Airplane scene (Top) is represented by GAUSSIANSPLAT, while the Lego scene (Bottom) is represented by NERF. The experimental settings for both cases follow those reported in Table 2
Figure 3:
From Table 2 we see that ABSTRACTRENDER is applicable to diverse scenes, including single-object (Lego), synthetic (PineTree), and large-seale realistic (Airport, Garden) scenes, with reasonable runtime at 200 x 200 resolution. The framework supports camera perturbations in both position (x, z) and orientation (roll, pitch, yaw). The metrics (MPG and XPG) computed by ABSTRACTRENDER (under GS and NeRF columns in Table 2) are larger than the corresponding empirical bounds, as expected, since our framework produces over-approximations which inherently encompass larger image space than the under-approximated empirical bounds. We further observe that bounds computed NERF exhibit tighter margins than those for GAUSSIANSPI.A as indicated by smaller MPG/XPG gaps relative to empirical samples. This is because NERF can leverage our linear bound

---

relaxation for cumulative product summation (Section 4.3 whereas GAUSSIANSPLAT cannot, due variations in the depth of 3D Gaussians on the image plane under camera rotation uncertainty.
Overall, these experimental results confirm that our method produces sound over-approximmtions that meaningfully tight for rendered images from both GAUSSIANSPLAY and NERF under camera pose uncertainty.
ABSTRACTRENDER for Certified Classification This experiment evaluates ABSTRACTRENDER for certifying neural classifier robustness against camera pose perturbations. We test whether pretrained CIFAR-10 10 ResNet [46] maintains correct predictions as the camera orbits the target object azimuthally over 360 at fixed distance and elevation. The 360 range is partitioned into angular intervals, and RASTRACTRENDER computes abstract images for each, which are propagated through the classifier via CROWN [T0] for set-based certification. An interval is robust if the lower bound of the target label exceeds the upper bounds of all other classes. Verification coverage is the percentage of certifiably robust intervals. Table B shows results for Airplane, Car, and Truck in GAUSSIANSPLAT and NERF scenes. Figure 4 visualizes camera regions where the classifier is certifiably correct (green) and regions without such guarantees (red). Regions capturing more of the object or its distinctive features are more likely to be verified as robust, e.g., the lateral views of the airplane and car, and the front-left view of the truck.
Table 3: Classifier certification results. Obj: Target Object; SR: Scene Representation, either GAUSSIANSPLAT NERF: d: Distance Object Centroid (m): h: Camera Height to Object's Horizon Plane (m); Npart: Number of Partitions; PCP-S: Percentage of Correct Partitions via
Sampling; PCP-V: Percentage of Certified Partitions via Formal Verification; Rt: Runtime (min).
Obj
SR
d
h
Npart
PCP-S
PCP-V
Rt
Airplane
GS
40
10
62832
96.0%
74.5%
1140.5
Car
GS
8
2.5
62832
96.3%
76.7%
879.6
Truck
GS
1.2
62832
71.8%
31.9%
963.4
Airplane
NERF
40
36
3142
25.6%
22.8%
94.3
Car
NERF
0.5
3142
75.9%
42.1%
118.6
0
O
0 0gl
3it 2
Figure 4: Classifier certification results for Airplane, Car, and Truck in GAUSSIANSPLAN scenes captured within these camera
across 0-360 camera rotations. Green: certified positions are always predicted correctly. Red: uncertified regions-imagen captured within these camera positions may be predicted incorrectly.
ABSTRACT RENDER for certified pose estimation This experiment evaluates ABSTRACTRENDER for certifying the robustness of neural pose estimators against camera pose perturbations. We assess a target pose estimator built upon GateNet [47] (fine-tuned on our airplane and truck datasets) by partitioning the camera's 's translational perturbation range into intervals. ABSTRACTRENDEA ates abstract images capturing all photometric variations within each interval, which are propagated through the estimator via CROWN to verify whether positional errors between pose estimation and ground truth holds below a given error tolerance (20% divation from ground truth). Verification cov- erage is measured the proportion of robust intervals across the workspace. Table/rreports results
gener-

---

for Airplane and Truck in GAUSSIANSPLAT and NERF scenes, while F visualizes camera regions where the estimator meets the error tolerance (green) versus regions without guarantees (red). Regions where the target object occupies a substantial portion of the rendered image are easier to certify-for example, distant regions in GAUSSIANSPLAT scenes and closer regions in NERF scenes, reflecting the different default camera-object distances in the two settings.
Table 4: Pose estimator and object detecter certification results. Obj: Target Object; SR: Scene Representation, either GAUSSIANSPLAT or NERF; d: Distance Object Centroid; CPR: Camera
Perturbation Range (m): PCP-S: Percentage of Correct Partitions via Sampling; PCP-V: Percentage of Certified Partitions via Formal Verification; Thr: Threshold; Rt: Runtime(min).
Certified Pose Estimation
Certified Object Detection
Obj
SR
CPR
PCP-S PCP-V
Rt
Thr
CPR
PCP-S
PCP-V
Rt
Airplane
GS
174.4
52.4%
23.3%
362.2
0.45
6
81.5%
51.4%.
422.2
Truck
GS
7.8
37.6%
22.2%
311.3
0.46
1
47.2%
42.4%
367.3
Airplane NERF
40
20
46.7%
37.2%
82.4
0.12
3.5
92.2%
80.4%
121.3
Truck
NERF
75.1%
70.0%
53.4
0.12
1.5
100.0%
71.0%
66.5
Figure 5: Pose estimator certification results for Airplane and Truck in GAUSSIANSPLAT scenes (Left, Middle) and Truck NERF scene (Right) across linear camera translation. Green: certified regions camera positions where estimated poses always remain within given error tolerance. Red: uncertified regions camera positions where estimated poses may exceed given error tolerance.
ABSTRACTRENDER for certified object detection This experiment evaluates ABSTRACTREN DER for certifying neural object detectors under camera pose perturbations. We test a pretrained detector based on the YOLO2 architecture [48] with backbone from the VNN-COMP 2023 bench- markf] The goal is to assess whether the detector can consistently produce bounding boxes that exceeds predefined confidence threshold under camera translations. The camera's 's translational range partitioned into small intervals. For each interval, ABSTRACTRENDER computes abstract images. These images are propagated through the YOLO2 detector. An interval is considered robust if the detector maintains a high-confidence bounding box across all images rendered from that interval. Table 4 reports reports results for Airplane and Truck in GAUSSIANSPLAT and NERF scenes, demonstrating ÄBSTRACTI RESTRACTRENDER 's capacity to certify object detection models.
Conclusions
Limitations. ABSTRACTRENDER currently has several limitations: First, like other verification approaches, it takes more time than sampling-based approaches. Second, the correctness of the analysis assumes the reconstructed scene accurately represents reality. Third, our framework computes bounds for each pixel's 's color independently, ignoring correlations between neighboring pixels.
Despite these limitations, ABSTRACTRENDER is the first framework for computing abstract images of scenes represented by Gaussian Splats and NeRF under camera pose or scene uncertainty. It is built using novel linear relational approximations of three rendering-specinn operations. By integrating LBSTRACTRENDEE with CROWN, we have enabled certification of visual tasks with respect to semantic variations in 3D environments. A promising direction for future work is to accommodate scenes inaccuracies and to certify visual control functions.
10

---

Acknowledgments and Disclosure of Funding
Chenxi Ji, Yangge Li, and Sayan Mitra are supported by research grant from The Boeing Company and NSF (FMITF-2525287), Huan Zhang and Xiangru Zhong are supported in part by the A12050 program at Schmidt Sciences (A12050 Early Career Fellowship) and NSF (IIS SLES-2331967 CCF FMITF-2525287).
References
[1] Bernhard Kerbl, Georgios Kopanas, Thomas Leimküüler, and George Drettakis. 3d gaussian splatting for real-time radiance field rendering. ACM Trans. Graph., 42(4):139-1, 2023.
[2] Ben Mildenhall, Pratul Srinivasan, Matthew Tancik, Jonathan T Barron, Ravi Ramamoor- thi, and Ren Ng. Nerf: Representing scenes as neural radiance fields for view synthesis. Communications of the ACM, 65(1):99-106, 2021.
[3] Siting Zhu, Guangming Wang, Xin Kong, Dezhi Kong, and Hesheng Wang. 3d gaussian splatting in robotics: A survey. arXiv preprint 2xXx::2410.122622 2024.
[4] Christopher Brix, Stanley Bak, Taylor T. Johnson, and Haoze Wu. The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results, 2024.
[5] Matthias Koenig, Annelot W Bosman, Holger H Hoos, and Jan N Van Rijn. Critically assessing the state of the art in neural network verification. Journal of Machine Learning Research, 25(12):1 2024.
[6] Habeeb, Deepak D' D'Souza, Kamal Lodaya, and Pavithra Prabhakar. Interval image abstraction for verification of camera-based autonomous systems. IEEE Transactions Computer-Aided Design of Integrated Circuits and Systems, 43(11):4310 4321, 2024.
[7] Sayan Mitra, Corina Päsăreanu, Pavithra Prabhakar, Sanjit A. Seshia, Ravi Mangal, Yangge Li, Christopher Watson, Divya Gopinath, and Huafeng Yu. Formal Verification Techniques for Fision-Based Autonomous Systems - A Survey, pages 89-108. Springer Nature Switzerland, Cham, 2025.
[8] Yangge Li, Chenxi Ji, Jai Anchalia. Yixuan Jia, Benjamin C Yang. Daniel Zhuang, and Sayan Mitra. Lyapunov perception contracts for operating design domains. In 7th Annual Learning for Dynamics', & Control Conference, pages 1053-1065. PMLR, 2025.
[9] Chiao Hsieh, Yubin Koh, Yangge Li, and Sayan Mitra. Assuring safety of rision-based swarm formation control, 2023.
[10] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1 129-1141, 2020.
[11] Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neu- ral network robustness certification with general activation functions. Advances in neural information processing systems, 31, 2018.
[12] Hai Duong, Thanh Vu Nguyen, and Matthew Dwyer. Neuralsat: A high- perfrrerform verifica- tion tool for deep neural networks. In International Conference on Computer Aided Verification, pages 409 423. Springer, 2025.
[13] Guy Katz, Derek A Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The marabou framework for verification and analysis of deep neural networks. In International conference on computer aided verification, pages 452- Springer, 2019.
[14] Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, and Taylor T Johnson. Nnv 2.0: The neural network verification tool. In International Conference on Computer Aided Verification, pages 397-412. Springer, 2023.

---

[15] Augustin Lemesle, Julien Lehmann, and Tristan Le Gall. Neural network verification with pyrat. arXiv preprint arXiv:2410.23903, 2024.
[16] Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor T Johnson. Improved geometric path enumeration for verifying relu neural networks. In International Conference on Computer Aided Verification, pages 66-96. Springer, 2020.
[17] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pages 97-117. Springer, 2017.
[18) Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Proceedings of the 7th International Conference on Learning Representations, 2019.
[19] Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International conference on machine learning, pages 5286-5295. PMLR, 2018.
[20] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1- 30, 2019.
[21] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in neural information processing systems, 31, 2018.
[22] Timon Gehr, Matthew Mirman, Dana Brechsler-Cohene Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE symposium on security and privacy (SP), pages 3-18. IEEE, 2018.
[23] Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Good- fellow, and Rob Fergus. Intriguing properties of neural networks. In Proceedings of the 2nd International Conference on Learning Representations, 2014.
[24] Alexey Kurakin, Ian Goodfellow, and Samy Bengio. Adversarial examples in the physical world. In Artificial intelligence safety and security, pages 99-112. Chapman and Hall/CRC, 2018.
[25] Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In Proceedings of the 6th International Conference on Learning Representations, 2018
[26] Naveed Akhtar and Ajmal Mian. Threat of adversarial attacks on deep learning in computer vision: A survey. IEEE Access, 6: 6:14410-14430) 2018.
[27] Naveed Akhtar, Ajmal Mian, Navid Kardan, and Mubarak Shah. Advances in adversarial attacks and defenses in computer vision: A survey. IEEE access, 9:155161-155196, 2021.
[28] Mark Huasong Meng, Guangdong Bai, Sin Gee Teo, Zhe Hou, Yan Xiao, Yun Lin, and Jin Song Dong. Adversarial robustness of deep neural networks: A survey from formal verification perspective. IEEE Transactions on Dependable and Secure Computing, 2022.
[29] Logan Engstrom, Brandon Tran, Dimitris Tsipras, Ludwig Schmidt, and Aleksander Madry. Exploring the landscape of spatial robustness. In International conference on machine learning, pages 1802-1811, 1. PMLR, 2019.
[30] Chaowei Xiao, Jun Yan Zhu. Bo Li, Warren He, Mingyan Liu, and Dawn Song. Spatially transformed adversarial examples. In Proceedings of the 6th International Conference on Learning Representations, 2018.
[31] Hossein Hosseini and Radha Poovendran. Semantic adversarial examples. In Proceedings of the IEFE Conference on Computer Vision and Pattern Recognition Workshops, pages 1614-1619, 2018.
12

---

[32] Cassidy Laidlaw and Soheil Feizi. Functional adversarial attacks. Curran Associates Inc., Red Hook, NY, USA, 2019.
[33] Anand Bhattad, Min Jin Chong, Kaizhao Liang, Bo Li, and David A. Forsyth. Unrestricted adversarial examples via semantic manipulation. In Proceedings of the 8th International Conference Learning Representations, 2020.
[34] Ali Shahin Shamsabadi, Ricardo Sanchez-Matilla, and Andrea Cavallaro. Colorfool: Semantic adversarial colorization. In Proceedings the IEEF/CVF conference on computer vision and pattern recognition, pages 1 1151-1160, 2020.
[35] Rima Alaifari, Giovanni S. Alberti, and Tandri Gauksson. ADef: an iterative algorithm to construct adversarial deformations. In International Conference on Learning Representations, 2019.
[36] Dan Hendrycks and Thomas Dietterich. Benchmarking neural network robustness to common corruptions and perturbations. In International Conference on Learning Representations, 2019.
[37] Dan Hendrycks Norman Mu*, Ekin Dogus Cubuk, Barret Zoph, Justin Gilmer, and Balaji Lakshminarayanan. Augmix: A simple method to improve robustness and uncertainty under data shift. In International Conference on Learning Representations, 2020.
[38] Jeet Mohapatra, Tsui- Wei Weng. Pin- Yu Chen, Sijia Liu, and Luca Daniel. Towards verifying robustness of neural networks against family semantic perturbations. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pages 244-252, 2020.
[39] Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev Certifying geometric robustness of neural networks. Advances in Neural Information P Processing Systems, 32, 2019.
[40] Marc Fischer, Maximilian Baader, and Martin Vechev. Certified defense image transfor- mations via randomized smoothing. Advances in Neural information processing systems, 33:8404 8417, 2020.
[41] Anish Athalye, Logan Engstrom, Andrew Ilyas, and Kevin Kwok. Synthesizing robust adver- sarial examples. In International conference on machine learning, pages 284-293, PMLR, 2018.
[42] Hanjiang Hu, Zuxin Liu, Linyi Li, Jiacheng Zhu, and Ding Zhao. Robustness certification of visual perception models via camera motion smoothing. In Proceedings of the 6th Conference on Robot Learning, 2022.
[43] Hanjiang Hu, Zuxin Liu, Linyi Li. Jiacheng Zhu, and Ding Zhao. Pixel-wise smoothing for certified robustness against camera motion perturbations. In International Conference on Artificial Intelligence and Statistics, pages 217-225. PMLR, 2024.
[44] Christian Green, Mehmet Ergezer, and Abdurrahman Zeybey. Targeted view-invariant adversar- ial perturbations for 3d object recognition, 2024.
[45] Matthew Tancik, Ethan Weber, Evonne Ng. Ruilong Li, Brent Yi, Terrance Wang, Alexander Kristoffersen, Jake Austin, Kamyar Salahi, Abhik Ahuja, al. Nerfstudio: modular frame- work for neural radiance field development. In ACM SIGGRAPH 2023 conference proceedings, pages 1-12, 2023.
[46] Shiqi Wang. Huan Zhang. Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in neural information processing systems, 34:29909-2999 29921,, 2021.
[47] Huy Xuan Pham, Ilker Bozcan, Andriy Sarabakha, Sami Haddadin, and Erdal Kayacan. Gatenet: An efficient deep neural network architecture for gate perception using fish-eye camera in autonomous drone racing. In 202/ JEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 4176 4183. IEEE, 2021.
[48] Joseph Redmon and Ali Farhadi. Yolo9000: better, faster, stronger. In Proceedings of the IEFE conference computer vision and pattern recognition, pages 7263-7271, 2017.
13

---

A An analytical example illustrating the advantage of Algorithm VR-IND
Consider two purely white Gaussians (with color values set to whose probability densities and depth to the target pixel are given by {0.8, 0.5) and d {I, + 1}. respectively, where [11, We aim to compute the worst-case bound of volumetric blending follows:
sorl(a,d)
oc(0]
oc [1[ as [0]
pc = oc[0] x as(0] + oc[1] x as(1]
first determine the output range of pc via Naive interval approach. By plugging in range of into the expression of d, we have d[0] = x E [-1, 1]. and d[1j x+ E [0, 2]. Since the relative ordering between d[O] and d[]] cannot be inferred from their interval bound, must consider both possible cases: one where (as as [s[]]) (a(0), a(l]). and the other where the assignment is reversed. Thus, we have
as [0] [s [0.5,088) oc[1] E (0.2,0.5)
Hence, the resulting interval bound for pe is:
pc [1 0.5 + 0.2 0.5, 1 0.8 + 0.5 0.8] [0.6, 1.2]
Next, we determine the output range of pc via proposed algorithm VR-IND, in which the same computation encoded symbolically to account for valueddependent assignments. The volumetric blending procedure reformulated using indicator functions (Ind), making the dependencies on explicit:
oc[0] (1 a(0] Ind(d[o] d(o))) x (1 a[1] [nd([(] d(l))
oc = (1 a (0) x [nd(d[1) d(o))) x (1 a[1] [nd( d(1)))
pc oc[0] x al0] + oc[1] x a[1]
Given d[0] and d[1], we can compute the values of indicator functions Ind in the above formulation.
Ind[d[o] d[1]) Ind(x (xr + 1)) Ind(-11
Ind[d[1] d(O)) Ind( 1 - x) Ind(1) (1)
Ind[d[1] d d[1]) Ind(d[0) d(]) Ind(()
Substituting these indicator values yields:
oc[0] = (1 0.8 0) x1 (1- 0)
oc[1] (1 0.8 1) (1- 0.5 0) 0.2
pc = x 0.8 +.2 0.5 0.9
Hence, using VR-IND, we obtain a precise bound pe [0.9,0.9), 0.9). which is significantly tighter than the interval-base -basd bound of [0.6, 1.2]. Remark: in the real verification pipeline, VR- "R-INNprrduces linear relaxation set instead of a fixed value. Here we use simplified case highlighting VR-IND'S advantage in terms of bound tightness.
The naive interval method leads loose bounds due the loss of dependency information caused by Sort operation. In contrast, the proposed VR-Ind method preserves input-dependent relationships and yields significantly tighter bounds.
14

---

B Proofs
Proposition Any continuous function is linearly over-approximable.
Proof. We present simple proof for scalar / and this can be extended to higher dimensions. We fix To E R and a finite slope & E R. Since f(x)) k(x - rn) continuous, for any & > 0, there must exist an open neighborhood U (zo) around zo, such that Vx R,
If(z) f(zo) k(x -xool-
3
Equivalently,
f(x)) + k(x -x0) m0) - < <(x)) < f(xo) + k(x - zo)
(2)
3
We construct candidate linear upper and lower bounds over U as:
(xr = k(x - xo) + [(x)) - 6 3' uer(x) = k(x - mn) + f(x0) + 3
(3)
We can check that these linear functions by (x) and un are valid lower and upper bounds for (x)
over U, because Vz E (xro:
f(x) (x) = -((x) (k(x ro) + ((o)
)) >
8 8
3 0,
(4)
())) = [(x) (k(x x0) + f(x0)
3/
(5)
3
Additionally, difference between 1 (x) and my (x) is tightly bounded, as Vo E Uxro):
(x) - Lu (x) = (N=( =o) f(x)) /) (k(x zo) f(zo) 9)
2e
< E.
3 3
Now, for any compact set B, the collection = {U xx) x E B} forms an open cover of B. By the definition of compactness, there exists finite subcover of B, denoted by {U, (1x,,)
1, 1....,8). 8}. We can now define piecewise linear functions on B as follows:
ux(x) = min un, (z), jel
(6)
(b(x) max lu, (4), if E (U,]jE
jel
where 7 the index set of U, that cover æ. Consequently, we have
u = min un, (x) 2 f(x) 2 max Lu, (x) = 1b(2); jel
(7)
jel
and
(w)(2) - 1n(x)| s (x) -2) (x) V.ET.
(8)
Thus, f is linearly over-approximable.
Lemma Given any non-singular matrix X, the output of Algorithm MATRIXINV (IXinv, uXinv) satisfies that:
IXinv < (xv(X)= S uXiiv
Proof. For any non-singular n X n matrices X and X denote their difference as AX = - The kth order Taylor Polynomial Xp and remainder XR of matrix inverse of X, estimated at Xvef, can be written follows:
Xp
AX X-1)
(9)
ref
i=0
XR
X-1
(AX
x-1
(10)
k=+1
15

---

Assuming that | X
||
< 1, the remainder XR can be bounded by:
|4 X kt]
[R]
X
|A
X - ref
= ||x
(11)
ref
4X X
i=k-1
Using the bound in inequality 11
we obtain bounds on X-1:
Xp XR X S Xp + XR
(12)
Given the definition of IXinv = Xp XR and uXinv = Xp XR. we obtain the lower and upper bound for X- as:
IXinv S -x-1 S uXinv.
(13)
For any given inputs - effective opacities colors and depth d, VR-IND outputs the same value as computation from Line 13 to Line 18 in GAUSSIANSPLAT.
Lemma 2
Proof. We first derive the math expression of pixel color pc from GAUSSIANSPLAT. By denoting
arg sort(d) as a mapping a : I + I, where refers to the index set of Gaussians, as at Line 13 cs at Line [4] and at Line can be written follows.
as; (i(
(14)
C5: = Ca(i)
(15)
i-1
OG ar(
(16)
j=1
According to the definition of Ind operation, have:
Ind - dd) = {
if d; dj if d: dj.
(17)
Then by replacing i.j with (i), (j), and multiplying az(i) (1
becomes:
a Ind(do - dow)) = a
{20000
if d do() do)
(18)
dx()
For any fixed index i, by multiplying all the case in the second branch of (8). it follows:
II 20() Ind(( doo))) 1.
(19)
By applying Equation
T6
Equation
18 and Equation 19 into Line T6 oc; can be written as follows:
OG;
(1 am
(1 ao(i)
Ind(do doo)))
(20)
j=1
N
II (1 aoll) Ind(da - -do)))
Then by applying Equation can be expressed as:
20 into Line
18 the pixel color pc computed via Algorithm BLENDSORT
N
[I
a.()
Ind(d= (do)))aa
(21)
16

---

Since the summation and product operations are invariant to the reordering of input elements, and both indices i and j iterate over the entire index the reordering mapping a in Equation [21 can be eliminated, resulting in:
N
N II
[1 Ind(d; - dj))aig
(22)
1=1
The last equation comes from Next, we derive the math expression for pc in Algorithm VR-IND. oc at Line2can be written as:
N OC II (1 a, Ind(d: - dd))
(23)
j=1
Then, by applying Equation
into Line 4 of Algorithm VR-IND, the expression for pc becomes:
N I 1=1
Ind(d; dj))a;q
(24)
i=1
Note that the expressions for pc are identical in both Equation 22 and Equation 24 This demonstrates that Algorithms BLENDSORT and VR-IND yield the same input-output relationship while applying different operations, thus completing this proof.
17

---

Supplementary Experiment Results
C.1 Detailed Scenario Information
Table summarizes scene configurations and rendering quality metrics for the scenarios discussed in Section F depicts representative GAUSSIANSPLAT-rendeee images for each scene.
Table 5: Reconstruction quality for scenes are evaluated by the following metries: NGauss: Number of Gaussians used for scene representation, applicable only to Gaussian Splatting: PSNR: Peak Signal-to-Noiss Ratio; SSIM: Structural Similarity Index Measure; LPIPS: Learned Perceptual Image Patch Similarity.
Gaussian Splatting
NeRF
Scene
NGauss
PSNR
SSIM
LPIPS
PSNR
SSIM
LPIPS
Lego
43543
25.60
0.95
0.07
21.38
0.81
0.19
Chair
46108
22.98
0.94
0.08
22.56
0.89
0.11
Drums
50877
21.19
0.89
0.10
19.46
0.81
0.23
Pinetree
113368
31.06
0.97
0.06
22.41
0.79
0.20
Airport
617371
18.83
0.84
0.33
20.83
0.72
0.22
Garden
524407
18.74
0.37
0.32
22.15
0.80
0.20
Plane
51316
28.05
0.95
0.11
22.89
0.70
0.26
Truck
47895
24.70
0.94
0.09
23.53
0.75
0.19
Car
34699
26.98
0.93
0.10
20.75
0.69
0.27
Figure 6:
Example rendered image for scenario (left to right, top to bottom): Lego, Pinetree, Airport, Garden, Plane, Truck, Car by GAUSSIANSPLAT.
C.2
Supplementary Results for Certified Classification
Figure 7 compares certified classification regions with those verified by sampling.
C.3
Supplementary Results for Certified Pose Estimation
Figure compares certified estimated pose regions with those verified by sampling.
C.4
Supplementary Results for Certified Object Detection
Figure 9 compares certified detection with those verified by sampling.
18

---

O q
Figure 7: Classifier certification result for AIRPLANE, CAR, and TRUCK by GAUSSIANSPLAT across 0-360 camera rotation. Top row: Certified classification result. Bottom Classification result obtained via sampling. Green: Certified/Corret Camera Pose Region. Red: Uncertified/Incoreett Camera Pose Region.
Figure 8: Pose estimation certification results for Airplane, Truck by GAUSSIANSPLAT scenes and Truck by NERF scene. Top row: Certified pose estimation result. Bottom row: Pose estimation result obtained via sampling. Green: Certified/Correct Camera Regions. Red: Uncertified/Incorreet Camera Regions.
C.5 ABSTRACT RENDER Results for Scene Variations
In addition to handling camera pose variations as discussed in Section ABSTRACTRENDER can also accommodate scene variations. For GAUSSIANSPLAN scenes, we consider variations in meaningful sets of 3D Gaussian parameters-such as color, mean position, and opacity of objects like trees in a street scene. For NERF scenes, we consider variations in hue or saturation across all 3D point colors in the scene. Table 6 presents ABSTRACTRENDER results under these scene variations for both GAUSSIANSPLAT and NERF representations. Figure I0) visualizes the abstract image of the PineTree (a GAUSSIAN scene) scene under uncertainty in color, mean position, and opacity of two tree objects. Figure II shows the abstract image of the Lego scene (a NERF scene) under uncertainty in hue and saturation across all 3D points.
19

---

6
Figure 9: Object detection certification results for Airplane and Truck in GAUSSIANSPLAT scenes.
Top row: Certified object detection result. Bottom row: Object detection result obtained via sampling. Green: Certified/Correct Camera Regions. Red: Uncertified//ncomee Camera Regions.
Ours
Empirical
Scene
PR
Dim
SR
Res
MPG
XPG
MPG
XPG
Lego
0.15
hue NeRF 80x80
0.17
1.51
0.14
1.45
Lego
0.30
satur NeRF
80x80
0.10
1.34
0.09
1.33
Chair
0.20
hue NeRF 80x80
0.65
1.71
0.37
1.71
Chair
0.50
satur NeRF
80x80
0.76
1.73
0.52
1.73
Drums
0.20
hue NeRF
80x80
0.63
1.20
0.62
1.20
Drums
0.50
satur
NeRF
80x80
0.96
1.36
0.88
1.36
PineTTree
0.10
mean
GS
96x96
0.27
1.62
0.11
1.27
PineTree
0.20
mean
GS
96x96
0.41
1.73
0.25
1.43
PineTree
0.10
op
GS
96x96
0.29
1.53
0.14
1.25
PineTree 0.20
op
GS
96x96
0.59
1.73
0.27
1.23
Table 6: ABSTRACTRENDER results under scene variations, along with empirical bounds. PR:
Perturbation Range; Dim: Perturbation Dimension, satur for saturation, mean for the mean's position of set of Gaussians, op for opacity of a set of Gaussians; SR: Scene Representation; Res: Rendered Image Resolution; Rt: Runtime (min); MPG: mean pixel gap: XPG: maximum pixel gap.
20

---

Color
Mean Position
Opacity
Lower Bound
Upper Bound
Figure 10: Lower (Top) and upper (Bottom) bound under Gaussian color (Left), mean (Mid) and opacity (Right) perturbation.
AbstractRender Results
Empirical Results
Hue
Saturation
Figure 11: Comparison between ABSTRACTRENDER results and empirical results Legot scene under perturbations the hue of 3DD points (top row) and saturation of 3D points (bottom row).
21

---

NeurIPS Paper Checklist
1. Claims
Question:
Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification:
We clearly summarize work's contribution and main application in the
abstract.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or
NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question: Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification:
We discuss limitation of work in Discussion section.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create a separate "Limitations" section their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect how these assumptions might be violated in practice and what the implications would be.
The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect on the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution is low images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
the paper. The authors should use their best
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
22

---

Justification:
The assumptions are clearly stated and proof can be referred in supplementary
material.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proof's can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should properly referenced.
4. Experimental result reproducibility
Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Question:
Answer: [Yes]
Justification:
We upload our code to github and is reproductive.
Guidelines:
The answer NA means that the paper does include experiments. If the paper includes experiments, No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm. (b) If the contribution is primarily
model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome deseribe the particular way they provide for reproducibility, In the case of closed-source models, it may be that access to the model is limited in some way (e.g., registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results.
5. Open access to data and code
Question: Does the paper provide open access to the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
23

---

Answer: [Yes]
Justification:
Yes, we uploaded our code to github and is reproductive.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips. cc/
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https
http:///ppplicca..aa/oooo//eaaaa /
wwt.Subbmiiiioooiiioooooooio for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data,
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended the paper) is recommended, but including URLs to data and code is permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Training and test does not apply for our work, but we provide detail of experiment setting for ours and baseline.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Our work computes rigorous bounds of output images/label. Significance does not apply our work.
Statistical
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper.
The factors of variability that the error bars capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).

---

It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative enror rates).
If error bars reported in tables plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed reproduce the experiments?
Question:
Answer: [Yes]
Justification:
We run our experiment on 32G A A100 GPU. Running times are also provide.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary failed experiments that didn't make into the paper).
9. Code ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics httppp////eerrr...cco//////////a
Answer: [Yes]
Justification:
No human participants gets involved in our experiment.
Guidelines:
The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special cireumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g., if there is special consid- eration due to laws or regulations their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: Our work aims to verify the safety of downstream neural network, able to mitigating potential negative societal impacts existing work.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
25

---

The conference expects that many papers will be foundational research and not tied particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.
If there negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms monitor how system learns from feedback over time, improving the efficiency and accessibility of MI..
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our work doesn't 't have such risks.
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Lieenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper. properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification: We have done this.
Guidelines:
The answer NA means that the paper does existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset is used and, if possible, include URL.
The name of the license (c.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (c.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswi thcode. com com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
26

---

If this information is not available online, the authors are encouraged to reach out to the asset's creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification:
We provide readme for our upload code.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/cooe/mmoel as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset is used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: Not relevant to human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsoureing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included the main paper.
According the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question:
Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification:
Not relevant to human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and expect authors to adhere to the NeurlPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such the institution conducting the review.
16. Declaration of LLM usage
27

---

Question: Does the paper describe the usage of LLMs if it is important, original, or non-standard component of the core methods this research? Note that if the LLM used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Answer: [NA]
Justification: Not involve LLM.
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs any important, original, non-standard components.
Please refer to our LLM policy fattps://neurip:::: /ttpaarrpp..cco/ooofeeeeeee///// for what should or should not be described.
28


Reviews:
[{"review_id": "1cNlOZ3yWG", "reviewer": "Reviewer_fGys", "summary": "This paper proposes an “abstract rendering” framework for scenes represented by neural radiance fields, aiming to compute conservative bounds that encompass the set of all possible rendered images produced over a continuous range of camera poses. The authors design algorithms for propagating input uncertainty through the rendering pipeline, constructing conservative bounds on the output images for verification.", "questions": "1. Please see the weakness section.\n2. What is the practical benefit of the proposed method, compared to dense empirical sampling of the rendering pipeline, especially given the real-time performance of modern 3DGS/NeRF?\n3. Colors in Algorithm 1 should be view-dependent, i.e. perturbing the camera may yield different colors for the same Gaussian, which is not captured in the proposed algorithm.", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "**Strengths**\n1. The paper extends abstract image computation techniques from mesh-based rendering to Gaussian splatting and NeRF, which are emerging and popular scene representations.\n2. Adapting abstract image computation to the rendering process for Gaussian splats and NeRF is mathematically nontrivial.\n3. Empirical results show that the proposed method can approximate the pixel-color bounds on the rendered images, which are affected by uncertainty in camera poses.\n\n\n**Weaknesses**\n1. The practical value of the proposed verification is questionable, as the method operates on fixed scene representations obtained via inverse rendering pipelines that already assume known camera parameters. In practice, 3D Gaussian splats or neural radiance fields are optimized to be **consistent** with training camera poses; if the camera poses used during scene capture were uncertain, that uncertainty would already affect the scene representation, not just the rendered images. Thus, verifying possible rendered images from a fixed scene under varying cameras does not reflect real-world verification needs.\n2. Questionable Need Over Empirical Approaches: Robustness to camera pose or scene perturbations could be empirically evaluated by sampling (as Table 1 illustrated), given that 3DGS and NeRF rendering are already **real-time**. The paper does not convincingly justify the necessity of complex and approximate abstraction over simple sampling for practical applications.\n3. The formal bounds produced are over low-level pixel values, whereas safety properties are typically defined at the level of object detection, semantics, or control decisions. The paper does not address end-to-end safety or correctness of downstream tasks.", "was_revised": true, "final_justification": "The paper takes a first step to extend abstract image computation techniques from mesh-based rendering to Gaussian splatting and NeRF, which are emerging and popular scene representations.\nAfter the rebuttal, I understand the practical values of the proposed method, especially when compared with the sampling-based method.\nThe proposed method is still useful even without modelling the reconstruction uncertainty or an advanced rendering scheme, especially considering that adapting abstract image computation to the rendering process for Gaussian splats and NeRF is mathematically nontrivial.", "rebuttal": "Our Abstract Rendering (AR) is the *first* to provide *provable guarantees* over ML-based image generation and perception pipelines involving modern photorealistic scene representations such as NeRFs and 3D Gaussian Splats (3DGS). We maintain that this technical contribution is not only nontrivial, but also enables a new class of **verification and certification tools for safety-critical vision-based autonomous systems**. \n\nYour review raises thoughtful concerns regarding the practical value of abstract rendering, particularly:\n\n(W1) that uncertainty in the scene reconstruction (e.g., from camera poses during capture) might undermine the validity of verification of 3DGS and downstream image processing,\n\n(W2) that simple empirical sampling may be sufficient in most practical settings, and\n\n(W3) that the paper does not demonstrate end-to-end verification at the semantic or decision level.\n\nWe agree that W1 and W2 are important considerations in the broader context of verifying vision-based autonomous systems. However, we respectfully maintain that these concerns **do not undermine the central technical claims and contributions** of the paper. Our work provides a mathematically sound, general-purpose framework for reasoning about uncertainty propagation in photorealistic rendering pipelines—something empirical methods cannot offer. We address W1–W3, Q1-Q3 in detail below.\n\n## **W1**\n\nAs with any model-based verification approach, the guarantees produced by Abstract Rendering (AR) are conditioned on the fidelity of the underlying model. AR provides *formal guarantees about uncertainty propagation* through the rendering and perception pipeline *with respect to a given 3DGS*. Whether the trained 3DGS itself accurately reflects the real-world scene is a separate—but important—consideration, and falls outside the primary technical focus of this paper.\n\nThis distinction is standard in verification: for instance, robustness verification of neural networks assumes a fixed input image, even though the image may itself result from a noisy sensing process. Similarly, AR assumes a fixed 3D scene and computes provable abstract images under bounded camera perturbations. This abstraction is both principled and practical—especially given the increasing fidelity of 3DGS reconstructions enabled by modern multi-view capture and recent advances in scene optimization.\n\nAs a concrete example, a major aerospace company is collaborating with us to apply AR to the **certification of an autonomous formation flight system** and an **automated landing system**. For formation flight, a camera mounted on the follower aircraft captures images of the lead aircraft. A vision-based ML model estimates the relative pose of the leader, which is then used by the follower’s flight controller to maintain formation. The company seeks to **formally certify** that across *all feasible relative positions* between the aircraft—and under modest environmental variation (e.g., lighting)—the vision system produces pose estimates within a specified error bound.\n\nThis verification problem is conceptually identical to the **certified pose estimation** results presented in our paper. AR enables formal guarantees about the output of the pose estimator over the space of rendered images, which can then be integrated into standard system-level verification pipelines. Due to the safety-critical nature of the task, worst-case guarantees are preferred over probabilistic methods, which may be difficult to interpret or insufficient in high-stakes settings.\n\nIn this use case, the certification is carried out on a fixed reconstructed 3DGS scene of the environment—e.g., with clear blue skies. (Our framework also handles scene variations with results provided in the table at the end of the response to reviewer n9Gh.) For the formation flight problem, being able to certify the system under nominal conditions (e.g., fixed lighting, background landscape, etc.) is already considered an important advance, as it ensures that even in idealized aerospace deployments, the vision-based controller behaves reliably and predictably. \n\nAs to the question of accuracy of 3DGS (which is admittedly not addressed in the current paper) their fidelity can be improved through: 1) Increasing the number and quality of capture viewpoints, 2) Using high-precision cameras, 3) Applying advanced, recently developed variants of 3DGS that improve reconstruction under pose uncertainty.\n\nIn view of the above, we respectfully reiterate that our verification setup is *both technically sound and practically motivated*. The ability to *certify downstream models over a range of plausible viewpoints and modest scene variation* is a powerful and timely capability—one we believe AR delivers.\n\n\n## **W2 & Q2**\nEmpirical sampling is a valuable tool for uncovering edge cases—but as Dijkstra famously said, “testing can show the presence of bugs, not their absence.” In contrast, Abstract Rendering (AR) computes conservative over-approximations that enable formal reasoning. For example, AR can prove that, across all approach angles of a follower aircraft toward a leader (see example introduced above), the downstream pose estimator will produce errors within a specified threshold—under the assumption of a given 3DGS scene. A real application of AR is discussed in our response to W1.\n\nWhether such formal guarantees are preferable to extensive empirical testing is context-dependent. In certain domains such as aerospace, chips, or distributed protocols, formal verification is often an essential complement to testing, especially when rare edge cases can cause catastrophic failure. We expect that similar needs will emerge in autonomy and robotics as systems become more capable and more tightly integrated into real-world environments.\n\nIt is also well understood that verification incurs a higher computational cost than testing and is not realtime. For example, verifying the robustness of a neural network on a small perturbation range often takes minutes—far longer than inference over regular inputs. Yet, the community has embraced this tradeoff, as evidenced by the large body of work on neural network verification and the strong participation in benchmarks like *VNN-Comp*. The cost is justified by the value of *soundness*.\n\nIn this broader context, AR provides a new capability: **it allows verification of perception models not under arbitrary pixel-level perturbations, but under structured, physically grounded changes in viewpoint**. Our work is the first to propagate formal uncertainty bounds through the **rendering process**, across advanced photorealistic scene representations like NeRFs and 3DGS—filling a key gap in existing verification pipelines.\n\nWhile our current implementation prioritizes correctness over speed, it serves as a foundation. We are actively exploring optimizations to improve scalability, including 1) parallelization, 2) tighter abstractions, and 3) efficient approximation strategies. We believe this makes AR not just a complement to empirical testing, but a foundational step toward verifiable autonomy.\n\n\n## **W3**\n\nWe would like to point out that our work *does* provide end-to-end correctness guarantees by propagating uncertainty in camera pose (and modest scene variation) through both the rendering process and the downstream image processing models—such as classifiers and pose estimators.\n\nThe overall verification process proceeds in two stages: 1) Rendering-stage verification: Abstract Rendering (AR) computes provable over-approximations of all images that could be generated from a given 3D scene and a bounded set of camera configurations. 2) Perception-stage verification: These image sets are then passed through neural networks, whose outputs are formally verified using mature tools developed by the neural network verification community.\n\nThe second stage has been extensively studied in the literature. State-of-the-art tools such as alpha-beta-CROWN [1], NeuralSAT [2], PRIMA [3], and others from the VNN-Comp competition have demonstrated robust performance across diverse architectures and tasks. Accordingly, our focus in this paper is on the first stage, where there has been *no prior work*: computing formal, structured uncertainty bounds through neural rendering pipelines like NeRFs and 3DGS.\n\nIn Section 5 (Figures 4–5, Tables 2–3), we present experimental results on two concrete end-to-end pipelines: AR + image classifier, and AR + pose estimator. These experiments demonstrate the ability of AR to support complete safety verification pipelines, covering both uncertainty in rendered input and robustness of the perception model’s output. While more complex downstream tasks—such as semantic segmentation or object detection—can be considered in future work, the same pipeline structure applies. As long as the downstream model is a neural network, existing verification tools can be used to extend AR to these settings.\n\nThus, our work represents a key missing component in enabling full end-to-end safety guarantees for vision-based autonomy: the sound propagation of uncertainty from the physical world, through rendering, into perception.\n\n## **Q3**\n\nPlease see our response to W1 of reviewer n9Gh.\n\n## **Reference**\n[1] Wang, Shiqi, et al. \"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.\" Advances in neural information processing systems 34 (2021): 29909-29921.\n \n[2] Duong, Hai, ThanhVu Nguyen, and Matthew Dwyer. \"A dpll (t) framework for verifying deep neural networks.\" arXiv preprint arXiv:2307.10266 (2023).\n \n[3] Müller, Mark Niklas, et al. \"PRIMA: general and precise neural network certification via scalable convex hull approximations.\" Proceedings of the ACM on Programming Languages 6.POPL (2022): 1-33."}, {"review_id": "EbPFmDEaF3", "reviewer": "Reviewer_n9Gh", "summary": "The paper first proposes AbstractRendering, an approximate way to estimate the lower and upper bound of the rendered images from a 3D scene given a linear set of camera poses.\nThe paper studies the math operations used in the 3D-GS and NeRFs, especially the (1) matrix inversion (2) sorting-based summation (3) and cumulative-product-based summation, and proposes better estimation for these operators.\nExperiments are conducted to examine the effectiveness of the proposed method.", "questions": "- Why there are N/A values for PSNR/SSIM in Table 5 of the updated appendix?", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strength:\n- The idea of the rendering bound under the noisy camera pose is novel and insightful.\n- The paper is well-organized and easy to follow.\n- The experiments support the claims well.\n\nWeakness:\nI am not an expert in approximation and have not kept up with recent progress in that field. The motivation, theories, and results look reasonable to me. I have only some questions that are not necessarily the weakness of the paper:\n- The 3D-GS scene model described in Section 3.2 L.137, directly uses the RGB vector $\\mathbf{c}$ to model the color instead of the wide-used SH coefficient. Is there any specific reason that the SH coefficient is not used? To my understanding, similar approximation can be made to estimate the procedure of calculating the color from the SH coefficients.\n- In L.159, the linear set of cameras is easy to understand by flatting the camera parameters into one single vector and applying the definition of linear set in L.116 (or by the spatial distribution of the noisy cameras). However, as both Gaussian and NeRF scenes have lots of parameters, how to properly define a linear set of the Scene $\\mathbf{Sc}$?\n- I am a little confused about Table 1. The paper mentioned in L.282 that *the NeRF can leverage the linear bound relaxation for cumulative product summation* so it shows smaller MPG/XPG than the 3D-GS. Is it the only reason to cause such a difference? Will the intrinsic robustness (to viewpoint changes) of 3D representations affect the MPG/XPG metric? For example, if one representation reconstructs the scene better (e.g. with more dense source views, or with the modeling of viewpoint effect such as the ray direction encoding in NeRF or SH in 3D-GS), will it have a smaller MPG/XGP metric for the same scene, compared to the other 3D representation of the same kind whose reconstruction quality is worse? Furthermore, is there some quantitative comparison between the proposed method and the sampling-based method (as Fig. 3)?", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their positive evaluation and thoughtful questions. We’re glad to see that the novelty and the empirical support of the paper came through clearly. Below, we address each of the reviewer’s points:\n\n## **Response to W1** — Why use RGB, not SH to model GS color:\n\nWe appreciate the reviewer’s thoughtful question. In our current implementation, we chose to use *fixed RGB vectors* to model color rather than *Spherical Harmonic (SH) coefficients*, primarily to keep the abstraction and analysis tractable for this initial study.\n\nWhile SH coefficients are indeed widely used in 3DGS to model *view-dependent appearance*, incorporating them would introduce additional *nonlinear dependencies on the viewing direction*—specifically, trigonometric basis functions and dot products over the camera ray and normal vectors. This would make the rendering process *significantly more nonlinear*, increasing the complexity of the abstract interpretation, especially under camera pose uncertainty.\n\nThat said, we fully agree that SH coefficients offer *greater expressive power*, allowing splats to vary their appearance with camera angle and enabling the modeling of specularities and shading effects. Our current work lays the foundation for bounding color contributions in photorealistic rendering pipelines, and extending our framework to handle *SH-based view-dependent color* is a natural and important direction for future work. The key techniques introduced here—such as bounding composition of nonlinear functions like matrix inversion and sorting—will generalize to that setting.\n\n \n##  **Response to W2** — How to properly define a linear set of the Scene Sc?:\n\nIn 3DGS, scenes are represented by sets of 3D Gaussians parameterized by color, opacity, mean, and covariance. A naive approach flattens these parameters into a vector for interpolation, similar to camera interpolation, but this becomes impractical due to the large number of Gaussians. We are actively exploring a more efficient method that enables physically meaningful scene variations—such as lighting, background, or coordinated object-specific changes. This is a realistic and relevant challenge. Similar to the formation flying scenario discussed in our response to Weakness 1 of reviewer rGhy, we aim to verify whether the target pose estimator remains robust under varying lighting and background conditions. Existing results for some type of scene variations—hue and saturation for NeRF, and brightness and background scenarios for GS, are provided in the table at the end of this rebuttal.\n\n\n## **Response to W3** — What causes lower MPG/XPG for abstract images from NeRF compared to 3DGS? Is it solely due to the use of linear bound relaxation for cumulative product summation? :\n\nThe difference in MPG/XPG between NeRF and 3D-GS is primarily due to the former’s ability to leverage linear bound relaxation over cumulative product summation. However, this is not the only contributing factor. Other aspects such as the density of source views and the inclusion of viewpoint modeling (e.g., ray direction encoding in NeRF or spherical harmonics in 3D-GS) can also influence the bounds.\n\nIn our experiments, we control for these variables by using the same source views and training settings for both methods. Even when 3D-GS achieves better rendering quality than NeRF, it consistently produces looser pixel-level bounds under camera rotation, due to the inapplicability  for linear bound propagation through the depth-based sorting operation. This is because, in a typical 3D-GS scene (with ~50k Gaussians), 500–6000 Gaussians can contribute significantly to a single pixel, even after applying opacity and distance thresholds. Due to the cumulative product over depth ordering, small uncertainties in depth can easily disrupt the correct ordering, leading to substantial over-approximation for provable (worst-case) bound.\n\nIn contrast, NeRF samples a fixed, small number of points (typically 32–128) along each ray, with a clearly defined front-to-back order, enabling linear bound propagation and resulting in much tighter bounds. The visual difference in bound tightness of a simple scene containing only three Gaussians is illustrated in the mid-left (naïve interval bound) and mid-right (linear bound) images in Figure 3. An additional numerical example is provided below for further clarification.\n\n### **Illustrative Example:** \n\nLet us consider the following setup:\n\n1)    Scalars: $a={0.8,0.5}$, $d={x,x+1}$, where $x\\in [-1,1]$, \n\n2)    Goal: Compute a tight and worst-case bound of the following procedure:\n \nStep1: $as=sort(a,d)$;\n\nStep2: $oc[0]=1$;\n\nStep3: $oc[1]=1-as[0]$;\n\nStep4: $pc=oc[0]\\times as[0]+oc[1]\\times as[1]$; \n \n\n*Naïve interval approach*:\n\nBecause sort(a,d) depends on the uncertain ordering of $d[0]=x\\in [-1,1]$, and $d[1]=x+1\\in [0,2]$, we can not determine the correct ordering of a[0] and a[1] in *as*. Thus we must conservatively assume the worst case:\n\n$as[0], as[1] \\in [0.5,0.8]$;\n\n$oc[1] \\in [0.2,0.5]$.\n\nThe resulting interval bound for pc is:\n\n$pc\\in [1⋅0.5+0.2⋅0.5,1⋅0.8+0.5⋅0.8]= [0.6,1.2]$\n\nThis yields a very loose bound.\n \n*Proposed VR-Ind approach*:\n\nUsing our proposed method *VR-Ind*, the same computation is encoded symbolically to account for value-dependent decisions. The control flow is represented using indicator functions (*Ind*), allowing us to keep the dependencies on *d* explicit:\n \nStep 1: $oc[0]=(1-a[0]\\times Ind(d[0]-d[0]))\\times  (1-a[1]\\times Ind(d[0]-d[1]))$\n\nStep 2: $oc[1]= (1-a[0]\\times Ind(d[1]-d[0]))\\times  (1-a[1]\\times Ind(d[1]-d[1]))$\n\nStep 3: $pc=oc[0]\\times a[0]+oc[1]\\times a[1]$; \n \nGiven that \n\n$d[0]-d[1]=x-(x+1)=-1<0 \\rightarrow Ind(-1)=0$;\n\n$d[1]-d[0]=(x+1)-x=1>0 \\rightarrow Ind(1)=1$;\n\n$Ind(0)=0$;\n\nWe obtain that \n\n$oc[0]=(1-0.8\\times 0)(1-0.5\\times 0)=1$;\n\n$oc[1]=( 1-0.8\\times 1)(1-0.5\\times 0)=1-a[0]=0.2$;\n\n$pc= 1\\times 0.8+0.2\\times 0.5=0.9$.\n\nThus, we obtain a precise bound $pc\\in [0.9,0.9]$, which is significantly tighter than the interval-based bound of $[0.6,1.2]$. By the way, in the real verification pipeline, VR-Ind will produce a linear relaxation set instead of a fixed value. Here we consider a simple case for highlighting VR-Ind’s advantage in terms of bound tightness. \n\nThe naïve interval method (used for mid-left image in Figure 2) leads to loose bounds due to loss of dependency information through Sort operation. In contrast, the proposed VR-Ind method (used for the mid-right image of Figure 2) preserves input-dependent flow and yields significantly tighter bounds.\n \n \n## **Response to Q** – Why are there N/A values for PSNR/SSIM in Table 5 of the updated appendix? :\n\nThe complete Table 5 in the updated appendix:\n\n|Scene|GAUSS(GS)|PSNR(GS)|SSIM(GS)|LPIPS(GS)|PSNR(NeRF)|SSIM(NeRF)|LPIPS(NeRF)|\n|------|---------|--------|--------|---------|-----------|-----------|------------|\n|Lego|43,543|25.60|0.95|0.07|21.38|0.81|0.19|\n|Chair|46,108|22.98|0.94|0.08|22.56|0.89|0.11|\n|Drums|50,877|21.19|0.89|0.10|19.46|0.81|0.23|\n|Pinetree|113,368|31.06|0.97|0.06|22.41|0.79|0.20|\n|Airport|617,371|18.83|0.84|0.33|20.83|0.72|0.22|\n|Garden|524,407|18.74|0.37|0.32|22.15|0.80|0.20|\n|Plane|51,316|28.05|0.95|0.11|22.89|0.70|0.26|\n|Truck|47,895|24.70|0.94|0.09|23.53|0.75|0.19|\n|Car|34,699|26.98|0.93|0.10|20.75|0.69|0.27|\n\n\n## **Additional result on AR under scene variation**:\n\nThe table below shows our framework capable of handling scene variation. \n\n|Scene|ε|Dim|Method|res|**Ours**| |**Empirical**| |\n|---|---|---|---|---|---|---|---|---|\n| | | | | |MPG|XPG|MPG|XPG|\n|Lego|0.15|hue|NeRF|80×80|0.17|1.51|0.14|1.45|\n|Lego|0.3|satur|NeRF|80×80|0.10|1.34|0.09|1.33|\n|Chair|0.2|hue|NeRF|80×80|0.65|1.71|0.37|1.71|\n|Chair|0.5|satur|NeRF|80×80|0.76|1.73|0.52|1.73|\n|Drums|0.2|hue|NeRF|80×80|0.63|1.20|0.62|1.20|\n|Drums|0.5|satur|NeRF|80×80|0.96|1.36|0.88|1.36|\n|Street1|0.1|ob-bright|GS|96×96|0.27|1.62|0.11|1.27|\n|Street1|0.2|ob-bright|GS|96×96|0.41|1.73|0.25|1.43|\n|Street2|0.1|ob-bright|GS|96×96|0.29|1.53|0.14|1.25|\n|Street2|0.2|ob-bright|GS|96×96|0.59|1.73|0.27|1.23|\n|Airplane|0.1|bg_sky|GS|160×160|0.49|1.68|0.19|1.52|\n|Airplane|0.1|bg_mt|GS|160×160|0.75|1.73|0.51|1.44|\n\nCaption: Results of Abstract Rendering under various scene perturbations, compared with empirical results. *Scene*: test scene; *Dim*: type of perturbation. *Hue* and *Satur* refer to hue and saturation changes applied to the entire scene. *ob-bright* modifies the brightness of a specific object—two trees in Street1, and one building in Street2. *bg* represents a setting where the airplane (foreground) is trained using GS, and the background is linearly interpolated between standard sky and mountain images. bg\\_sky and bg\\_mt correspond to background regions closer to sky and mountain, respectively. res: output image resolution. *MPG/XPG*: Mean/Max Pixel-Color Gap, as defined in the main paper. The *Ours* and *Empirical* columns report MPG and XPG for our method and the empirical baseline, respectively."}, {"review_id": "VXGYGxT4Wx", "reviewer": "Reviewer_CPny", "summary": "This paper proposes a verification framework that computes provable bounds on all images rendered by neural rendering methods such as NeRF and 3DGS under perturbed camera poses. This is achieved through three approximations of non-linear operations, such as matrix inversion and sorting.", "questions": "- Could the authors clarify in what practical scenarios that the verification of 3D rendering would be effective?\n- Can the authors provide more detailed results for real-world scenes?\n- Can it be possible to provide several results where all settings are kept the same, except for the rendering method (NeRF vs. 3DGS)?", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "### Strength\n- The application of formal verification to neural rendering is novel.\n- The proposed approximations are methodologically and mathematically sound, and clearly written.\n\n### Weakness\n- It is unclear whether the verification, which is essential for assessing the robustness of general neural networks, is also meaningful for 3D rendering models. In rendering, pixel-level differences caused by camera perturbation are expected and do not indicate a failure or lack of robustness. Moreover, the practical use of rendered images from an already trained model for downstream tasks remains unclear.\n- Despite using small, object-centric scenes, the verification runtime is reported to take hours for downstream evaluations, raising concerns about scalability.\n- The evaluation setup appears inconsistent. For example, comparisons across methods (NeRF vs. 3DGS) are not controlled under the same configuration.\n- Adding the perS to the main paper, rather than only the appendix, would help clarify the extent of over-approximation introduced by the method.", "was_revised": true, "final_justification": "After the rebuttal, many of my concerns were addressed. Although some points remain unclear regarding practicality, I understand that abstract rendering can be useful in certain contexts. I believe this can facilitate further research, and therefore I raise my rating to 4.", "rebuttal": "We thank the reviewer for recognizing the novelty of applying formal verification to neural rendering and for appreciating the mathematical soundness of our Abstract Rendering (AR) method. We maintain that this contribution is not only technically nontrivial, but also enables a new class of verification and certification tools for safety-critical vision-based autonomous systems. Below, we address the reviewer’s two primary concerns:\n\n**W1**: The reviewer questions the practical value of verifying 3D rendering models, noting that (1) pixel-level differences caused by camera perturbations are expected and may not indicate failure, and (2) it is unclear whether verifying rendered images from a pre-trained model is useful for downstream tasks.\n\n**W2**: Verification takes a long time and may not be practical.\n\nWe agree that W1 and W2 are important considerations for real-world deployment and end-to-end certification. However, we respectfully maintain that these concerns *do not undermine the central technical contributions of the paper*.\n\n## **W1**：\n \nWe would like to clarify that pixel-level variation due to camera pose changes can in fact lead to significant downstream effects in safety-critical systems such as autonomous driving and robotic manipulation. Seemingly minor rendering differences can alter object detection outcomes or control decisions, particularly when models are sensitive to input shifts.\n\nOur Abstract Rendering (AR) method does not aim to eliminate image variation under camera pose shifts; rather, it allows us to verify that a downstream perception module behaves **consistently and safely** across the set of rendered images bounded by camera uncertainty. \n\nWe demonstrate this explicitly in Section 5 through two end-to-end pipelines: 1) AR + image classifier; 2) AR + pose estimator. These experiments show that Abstract Rendering can support **concrete downstream verification tasks**, not just pixel-level reasoning. \n\nAs another example, we are currently collaborating with a major aerospace company to apply AR to the **certification of autonomous formation flight** and **landing systems**. In formation flight, a camera on the follower aircraft captures images of the leader. A vision-based ML model estimates the leader’s relative pose, which is used by the flight controller to maintain formation. The company’s goal is to formally certify that, across all feasible relative positions—and under modest environmental variation (e.g., lighting)—the vision system produces pose estimates within a specified error bound.\n\nIn this use case, the certification is carried out on a fixed reconstructed 3DGS scene of the environment—e.g., with clear blue skies. (Our framework also handles scene variations with results provided in the table at the end of the response to reviewer n9Gh.) For the formation flight problem, being able to certify the system under nominal conditions (e.g., fixed lighting, background landscape, etc.) is already considered an important advance, as it ensures that even in idealized aerospace deployments, the vision-based controller behaves reliably and predictably. \n \n\n## **W2**:\n\nWe appreciate the reviewer’s concern regarding verification runtime. **Provable, worst-case verification is inherently more computationally demanding than empirical testing**, as it guarantees correctness over entire input regions—not just sampled instances. In this regard, AR is aligned with the broader formal methods community, where high runtime is an accepted tradeoff for soundness.\n\nFor comparison, leading neural network verification methods such as **β-CROWN** [1], **NeuralSAT** [2], and **PRIMA** [3] routinely require **hundreds to thousands of seconds per instance**. Our reported runtime—ranging from **minutes to a few hours** depending on scene complexity and perturbation bounds—is well within the standard range for safety verification tasks. This is particularly reasonable given that our work is the **first to provide provable bounds through differentiable 3D rendering models** such as NeRFs and 3DGS.\nWe emphasize that **our current implementation prioritizes tightness and correctness of bounds**. As in the early stages of many verification tools (e.g., CROWN [4]), we begin with small, controlled settings to develop foundational techniques. Over time, tools like CROWN scaled up to handle larger networks and more complex tasks—culminating in competitive results on VGG-16 and ResNet benchmarks in VNN-Comp 2024. We are following a similar path and are actively developing optimizations, including: 1) Parallelization of bound computation, 2) GPU acceleration for abstraction steps, and 3) Tighter approximations for nonlinear operations.\n\n## **W3 & Q3**\n\nWe agree that using consistent configurations is essential when comparing a novel method against a baseline, as it ensures fairness and highlights the true contribution of the proposed work. However, in this case, **both abstract rendering pipelines over NeRF and 3DGS are contributions of our own framework**. Therefore, a direct performance comparison between the two is not the **primary objective** of our experiments setup.\n\nInstead, the purpose of our experiment setup (e.g. Table 1) is to demonstrate that our verification framework is compatible with multiple rendering backbones and can operate under a variety of configurations. Given the page limit, we aimed to showcase this breadth rather than perform controlled comparisons. \n\nAlthough our goal is not to directly compare the verification pipeline on NeRF and 3DGS, given your interest in a shared configuration, we updated Table 1 to include both rendering methods under the same setup, as shown below.\n\n|Scene|ε|Dim|Res|**GS**|||**Nerf**|||**Empirical**||\n|---|---|---|---|---|---|---|---|---|---|---|---|\n||| | |Rt|MPG|XPG|Rt|MPG|XPG|MPG|XPG|\n|Lego|0.1(rad)|yaw|80×80|22|0.51|1.73|25|0.40|1.73|0.22|1.57|\n|Chair|0.1(rad)|yaw|50×50|17|0.46|1.73|20|0.40|1.73|0.40|1.72|\n|Drums|0.1(m)|x|50×50|5.3|0.19|1.62|5.8|0.16|1.55|0.13|1.54|\n|PineTree|2(m)|x|72×72|4.1|0.27|1.73|4.9|0.23|1.73|0.06|1.37|\n|PineTree|10(m)|x|72×72|24|0.47|1.73|28|0.36|1.73|0.18|1.37|\n|Airport|0.027(rad)|roll|160×160|27|0.56|1.69|35|0.42|1.63|0.21|1.38|\n|Garden|0.5(m)|x|100×100|20|0.53|1.59|11|0.37|1.53|0.34|1.21|\n\n \n## **W4**\n\n*perS* will be moved to the main paper in the final version.\n\n \n## **Q1**\n\nOur verification framework is particularly well-suited to **vision-based, safety-critical applications** where the environment is structured, the number of relevant objects is limited, and high reliability is essential. Examples include:\n\n**Autonomous formation flight** (as discussed above), where a follower aircraft must maintain precise positioning relative to a lead aircraft using camera input.\n\n\n**Vision-based automated landing**, where a drone or aircraft must visually identify and align with a landing site based on onboard perception.\n\n\n\n**Autonomous vehicle docking or payload transfer**, where AR ensures that visual pose estimators remain accurate across approach angles during close-range maneuvers.\n\n\n**Warehouse inventory robotics**, where AR verifies that a robot navigating structured aisles can reliably detect and classify labeled bins or packages from varying camera angles under fixed lighting.\n\n\nIn all of these scenarios, **modest environmental variability** (e.g., fixed lighting, sky backgrounds, known landmarks) makes it feasible to reconstruct a high-fidelity 3D scene (e.g., via 3DGS), and it is crucial to certify perception behavior over a **bounded set of viewpoints**. AR enables **provable safety guarantees** in these settings—where failures can have high consequences and formal correctness is preferred over empirical coverage.\n\n## **Q2**\nWe provide additional results on more realistic scenes featuring large, complex backgrounds. The evaluation includes four scenes: Garden and Bicycle from the Mip-NeRF 360 dataset, as well as Airport and Airplane with Mountain View Background from our own benchmark. These new scenes are chosen to test the robustness of our framework under varied and realistic conditions. \n\n|Scene|ε|Dim|res|**GS**|||**NeRF**|||**Empirical**||\n|------------|-----------|-------|-------------|--------------|---------|---------|-------------|---------|---------|--------------|---------|\n||| | |Rt|MPG|XPG|Rt|MPG|XPG|MPG|XPG|\n|Garden|0.5(m)|x|100×100|20|0.53|1.59|33|0.37|1.53|0.34|1.21|\n|Bicycle|0.2(m)|x|100×100|23|0.72|1.68|31|0.58|1.60|0.37|1.35|\n|Airport|0.03(rad)|roll|160×160|30|0.59|1.70|43|0.51|1.68|0.22|1.41|\n|Airplane|2(m)|x|80×80|16|0.41|1.68|19|0.33|1.61|0.15|1.39|\n \n \n## **Reference**\n\n[1] Wang, Shiqi, et al. \"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.\" Advances in neural information processing systems 34 (2021): 29909-29921.\n \n[2] Duong, Hai, ThanhVu Nguyen, and Matthew Dwyer. \"A dpll (t) framework for verifying deep neural networks.\" arXiv preprint arXiv:2307.10266 (2023).\n \n[3] Müller, Mark Niklas, et al. \"PRIMA: general and precise neural network certification via scalable convex hull approximations.\" Proceedings of the ACM on Programming Languages 6.POPL (2022): 1-33.\n\n[4] Zhang, Huan, et al. \"Efficient neural network robustness certification with general activation functions.\" Advances in neural information processing systems 31 (2018)."}, {"review_id": "frsNQt5cUA", "reviewer": "Reviewer_ukG3", "summary": "This paper proposed Abstract Rendering, which is a framework that abstracts NeRF or 3DGS as a collection of operations, where most operations are linearly over-approximable and can be provably bounded. The paper also designs techniques to handle nonlinear operations (Matrix inverse, sort, cumulative product) by designing equivalent boundable algorithms. The paper verifies the soundness of the framework by comparing the results with empirical sampling, and further conducts experiments to demonstrate various applications of this certification framework.", "questions": "1. Can you explain whether the framework is dependent on a certain certification framework (CROWN) or can be generalized?\n2. Can you refine your examples in Sec. 4 by adding more explanations?\n3. Can you compare the uncertainty obtained by the certified bounds with Bayesian uncertainty from a probabilistic perspective, and, if possible, provide experimental comparisons?\n4. In Fig. 4, it is surprising that the results of the car and the truck are asymmetric. Intuitively, the result should be symmetric about the axis of $\\frac{3\\pi}{2}$.\n5. In Fig. 5, I can't infer anything from simply looking at the red-green axis. Can you provide some explanations about why this result makes sense?", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "# Strengths\nThe proposed method is generally novel. It is the first work that interprets the NeRF and 3DGS algorithms using basic operations, provides provable bounds for them, and correctly handles nonlinear operations by further designing tailored techniques to bound them. The soundness of the proposed method is well-validated by experiments, and application-side experiments are conducted to demonstrate the potential of the proposed method.\n\n# Weaknesses\n1. Dependent on existing frameworks: After decomposing the rendering algorithm into operations, it requires an existing framework (CROWN) to provide the certification, which is not the paper's contribution.\n2. Possible refinements in the examples in Sec. 4: In Example 1 in Sec. 4.1, the original matrix $X$ is not given; is this a mistake? In Example 2 and Fig. 2, it is unclear how the mid-left image's (\"via GaussianSplat\") upper bound is generated, since the \"Sort\" operation in GaussianSplat is not linearly over-approximable.\n3. Missing comparisons: The experimental results look good, but there is no comparison or verification for these results. A possible line of work that is worth comparing to is the Bayesian uncertainty quantification in NeRFs (e.g., [1, 2, 3]). How does the uncertainty obtained by the certified bounds (via CROWN) compare to the Bayesian uncertainty? Are they similar or different in purpose or applications?\n\n```\n[1] Goli, Lily, et al. \"Bayes' rays: Uncertainty quantification for neural radiance fields.\" Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. 2024.\n[2] Jiang, Wen, Boshu Lei, and Kostas Daniilidis. \"Fisherrf: Active view selection and mapping with radiance fields using fisher information.\" European Conference on Computer Vision. Cham: Springer Nature Switzerland, 2024.\n[3] Lyu, Linjie, et al. \"Manifold Sampling for Differentiable Uncertainty in Radiance Fields.\" SIGGRAPH Asia 2024 Conference Papers. 2024.\n```", "was_revised": true, "final_justification": "The rebuttal has addressed most of my concerns, I'll raise my rating toward acceptance.", "rebuttal": "We thank the reviewer for recognizing the novelty of our approach in decomposing neural rendering pipelines into basic operations and computing provable bounds, as well as for highlighting our tailored techniques for bounding nonlinear components. We emphasize that this contribution is both technically nontrivial and foundational, as it enables a new class of formal verification and certification tools for vision-based autonomous systems in safety-critical settings. Below, we address the reviewer’s three primary concerns:\n\n**W1**: Dependence on existing verification tool, CROWN.\n\n**W2**: Unclear explanation of examples in Section 4.\n\n**W3**: Lack of experimental comparison; Bayesian uncertainty quantification in NeRFs is suggested as a baseline.\n\n## **Response to W1** — Our work is built on CROWN, which is not our contribution. :\n\nOur abstract rendering method is implemented using CROWN but, importantly, it does not depend on CROWN specifically. Any tool or library for computing and propagating piece-wise linear bounds can be used to implement our approach. For example, tools like AI^2[1], ERAN[2], convex_adversarial[3] could in principle be used to implement abstract rendering provided they support the operations in Table 4 in the appendix. That said, we note that we *did not* have to extend CROWN with 1) providing linear bound for common operations and 2) propagating linear bound operation by operation for our current implementation. The contribution of our work is in recognizing how the nonlinear functions involved in rendering Gsplat and NeRF can be soundly and compositionally approximated so that the scheme can then be implemented using a library like CROWN.\n\nWe are failing to see why using an existing framework (CROWN) for building abstract rendering is a weakness of our work. In the updated paper, we will make the exposition clearer on (a) the current dependence on CROWN and (b) the implementation work needed to build AR on a different framework.\n \n## **Response to W2** — Confusions on Example 1&2 in Section 4:\n\nWe acknowledge that the explanation of the examples in Section 4, was insufficiently detailed due to space limitations. We appreciate the opportunity to clarify the settings and rationale behind our design.\n\nIn Example 1, the matrix X is not explicitly provided because the intention is to illustrate how to compute bounds on the inverse of a matrix over *a range of input*, rather than a single instance. While the MatrixInv computes bounds for a fixed matrix X relative to a reference matrix X0, in practical verification pipeline, we work on bounding the inverse over a set of possible matrices, described by element-wise lower and upper bound $\\underline{X}$ and $\\overline{X}$, respectively. \n\nGiven that all operations within MatrixInv support linear bound propagation (as enabled by CROWN), we propagate bound through those operations and obtain element-wise lower and upper bounds of lXinv and uXinv. Then the lower bound of lXinv and upper bound of uXinv form the guaranteed bounds for $X^{-1}$.\n \nThe further example is provided in case you are not familiar with linear bound propagation. To illustrate the general approach of this technology, consider a simple function:\n\n$f(x)=(ReLU(x))^2, for x \\in [-1,1]$\n\nWe decompose this into two functions:  h(x)=ReLU(x) and g(y)=y^2. For h(x), we can linearly bound the output within:\n\n$0\\leq h(x)\\leq x/2+1/2, for all x \\in [-1,1]$\n\nGiven $y=h(x)\\in [0,1]$, we then bound g(y) with:\n\n$0\\leq g(y)\\leq y$\n\nBy composing the two bounds, we obtain a valid linear bound for f(x) over the range $[-1,1]$:\n\n$0\\leq f(x)\\leq x/2+1/2$\n\nThe resulting interval for f(x) is therefore $[0,1]$. \n\nThis example demonstrates the core idea of **linear relaxation-based bound propagation**, which is central to our method. For a complete and rigorous treatment of how linear bounds are computed and propagated across various operations, we refer you to the CROWN series of papers.\n \n\nIn Example2, we acknowledge that the baseline approach for generating the mid-left image of Figure 2 (“via GaussianSplat”) is not explicitly explained. It’s true that the *Sort* operation is not supported by linear approximation. To handle this, we concretize all linear bounds into interval bounds by computing their minimum and maximum values over the input domain before the *Sort* operation. The rest of the computation is then conducted using interval bounds. We will clearly explain this in the revision. This transformation inherently loses precision, as interval bounds are typically looser than their linear counterparts. We provide a simple, numerical example in response to W3 of reviewer n9Gh for better illustration..\n\n## **Response to W3** — Missing comparison with potential baselines (e.g. Bayesian uncertainty quantification in NeRF). :\n\nThank you for highlighting related work on Bayesian uncertainty quantification in NeRFs . While these approaches are valuable, they address a fundamentally different problem and are not directly comparable to our setting. We clarify the distinction below.\n\nBayesian uncertainty methods aim to estimate confidence at the *3D point level* in the scene or at the *pixel-color level* in rendered images. Their goal is to indicate which parts of the NeRF reconstruction are reliable or uncertain, which is useful for assessing reconstruction quality or guiding further training.\n\nIn contrast, our framework—*abstract rendering*—operates under the assumption that the reconstructed 3D scene is fixed and reasonably represents the underlying real-world structure. We compute an *abstract image set* that is guaranteed to enclose all images rendered from a specified region of camera poses. This set is used to provide *certified input bounds* to downstream ML models (e.g., classifiers or pose estimators), enabling *provable guarantees* on the model’s output across the entire range of physically realizable viewpoints.\n\nBecause the Bayesian approach provides **point-wise or pixel-wise confidence** based on **scene reconstruction-relevent camera poses**, while our method yields a **set-valued output** over **a range of camera poses covering the operational domain where the downstream ML model is deployed**, the two outputs are inherently different in form and purpose. As such, a direct comparison is not meaningful.\n\nThat said, Bayesian uncertainty quantification is still relevant to our setting, as it informs the reliability of the underlying scene reconstruction—an assumption on which our framework relies. We will add the following statement to the discussion section of the paper:\n\nOur framework assumes the reconstructed 3D scene accurately reflects the real-world environment. Although all model-based analyses involve approximation, understanding the uncertainty in 3D scene reconstruction (e.g., [1, 2, 3]) is meaningful. Incorporating such uncertainty into our framework is a promising direction for future research.\n\n\n## **Response to Q1** — Please explain whether our framework is dependent CROWN or can be generalized:\n\nAs we discussed in the response to W1, our framework can be generalized to other verification tools, as long as they support linear bound propagation among all operations listed in Table 4 in the appendix, except for the three custom operations in our main paper.\n \n## **Response to Q2** — Please provide more explanations on examples in Sec. 4. :\n\nYes, thanks for pointing out the insufficient explanation. Please read our response to W2. We will put these explanations in the appendix in the final version.\n \n \n## **Response to Q3** — Is it reasonable to compare our results with the uncertainty obtained by the certified bounds with Bayesian uncertainty? If so, provide some experimental comparisons.:\n\nPlease see our response to W3.\n \n## **Response to Q4** — Why are the results of the car and the truck in Fig 4 asymmetric? :\n\nThe observed asymmetry primarily arises from the behavior of the downstream machine learning models (e.g., the image classifier or pose estimator). Although the objects themselves may exhibit geometric symmetry, these downstream models are not inherently equivariant to symmetric transformations in the input space. As a result, symmetric input images can lead to different outputs.\n \n## **Response to Q5** — Please provide some explanations on Fig 5 about why this result makes sense. :\n\n\nFigure 5 visualizes which subregions within a continuous 3D camera pose interval can be formally verified to ensure the downstream pose estimator (GateNet) maintains a bounded error. We model the full pipeline—rendering (Gaussian Splatting or NeRF) followed by pose estimation—and apply linear bound propagation using abstract rendering and CROWN.\nEach camera subregion is marked *green* if the upper bound of the pose error remains below a predefined safety threshold (e.g., 10 feet per axis); otherwise, it is marked *red*, indicating unverifiable or potentially unsafe predictions.\n\nAlthough difficult to fully interpret black-box model behavior, we observe consistent patterns in unverifiable (red) regions, which often correspond to: 1) Unfavorable viewpoints, 2) Occlusion or dominant object features (e.g., a large logo), or 3) Insufficient visual information (e.g., only part of the object visible).\n\nThese results highlight the importance of viewpoint diversity and geometric coverage—factors our verification method captures effectively.\n\n\n ## **Reference**\n\n[1] Gehr, Timon, et al. \"Ai2: Safety and robustness certification of neural networks with abstract interpretation.\" 2018 IEEE symposium on security and privacy (SP). IEEE, 2018.\n\n[2] Müller, Mark Niklas, et al. \"ERAN: ETH robustness analyzer for neural networks.\" URL https://github. com/eth-sri/eran (2022).\n\n[3] Wong, Eric, and Zico Kolter. \"Provable defenses against adversarial examples via the convex outer adversarial polytope.\" International conference on machine learning. PMLR, 2018."}]

Author rebuttal:

Meta-review: This paper proposes an abstract rendering, an approximate method to estimate the lower and upper bounds of the rendered images from a 3D scene, given over a continuous range of camera poses. The paper presents algorithms for propagating input uncertainty through the rendering pipeline, constructing conservative bounds on the output images for verification.

The reviewers highly value the novelty of this work. In particular, the paper discusses the *abstract* rendering using noisy camera poses (bounded by some range) in Gaussian splatting (GS) and NeRF. The method would also be interesting from the viewpoint of Bayesian optimization.

During the reviewer discussions, all authors' opinions converged on the acceptance of the paper.
Decision: Accept (spotlight)