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:

W1: Dependence on existing verification tool, CROWN.

W2: Unclear explanation of examples in Section 4.

W3: Lack of experimental comparison; Bayesian uncertainty quantification in NeRFs is suggested as a baseline.

Response to W1 — Our work is built on CROWN, which is not our contribution. :

Our 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.

We 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.

Response to W2 — Confusions on Example 1&2 in Section 4:

We 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.

In 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.

Given 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}$.

The 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:

$f(x)=(ReLU(x))^2, for x \in [-1,1]$

We decompose this into two functions: h(x)=ReLU(x) and g(y)=y^2. For h(x), we can linearly bound the output within:

$0\leq h(x)\leq x/2+1/2, for all x \in [-1,1]$

Given $y=h(x)\in [0,1]$, we then bound g(y) with:

$0\leq g(y)\leq y$

By composing the two bounds, we obtain a valid linear bound for f(x) over the range $[-1,1]$:

$0\leq f(x)\leq x/2+1/2$

The resulting interval for f(x) is therefore $[0,1]$.

This 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.

In 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..

Response to W3 — Missing comparison with potential baselines (e.g. Bayesian uncertainty quantification in NeRF). :

Thank 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.

Bayesian 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.

In 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.

Because 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.

That 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:

Our 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.

Response to Q1 — Please explain whether our framework is dependent CROWN or can be generalized:

As 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.

Response to Q2 — Please provide more explanations on examples in Sec. 4. :

Yes, 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.

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.:

Please see our response to W3.

Response to Q4 — Why are the results of the car and the truck in Fig 4 asymmetric? :

The 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.

Response to Q5 — Please provide some explanations on Fig 5 about why this result makes sense. :

Figure 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. Each 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.

Although 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).

These results highlight the importance of viewpoint diversity and geometric coverage—factors our verification method captures effectively.

Reference

[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.

[2] Müller, Mark Niklas, et al. "ERAN: ETH robustness analyzer for neural networks." URL https://github. com/eth-sri/eran (2022).

[3] Wong, Eric, and Zico Kolter. "Provable defenses against adversarial examples via the convex outer adversarial polytope." International conference on machine learning. PMLR, 2018.

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:

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.

W2: Verification takes a long time and may not be practical.

We 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.

W1：

We 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.

Our 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.

We 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.

As 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.

In 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.

W2:

We 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.

For 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. We 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.

W3 & Q3

We 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.

Instead, 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.

Although 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.

W4

perS will be moved to the main paper in the final version.

Q1

Our 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:

Autonomous formation flight (as discussed above), where a follower aircraft must maintain precise positioning relative to a lead aircraft using camera input.

Vision-based automated landing, where a drone or aircraft must visually identify and align with a landing site based on onboard perception.

Autonomous vehicle docking or payload transfer, where AR ensures that visual pose estimators remain accurate across approach angles during close-range maneuvers.

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.

In 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.

Q2

We 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.

Reference

[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.

[2] Duong, Hai, ThanhVu Nguyen, and Matthew Dwyer. "A dpll (t) framework for verifying deep neural networks." arXiv preprint arXiv:2307.10266 (2023).

[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.

[4] Zhang, Huan, et al. "Efficient neural network robustness certification with general activation functions." Advances in neural information processing systems 31 (2018).

Thank you for your thoughtful follow-up and for recognizing the novelty and technical grounding of Abstract Rendering (AR). We appreciate your continued engagement and the opportunity to clarify the practical role of AR, particularly in the formation flight example.

Kindly see our response to Reviewer fGys, where we address broader concerns about the practicality of AR, provide new experimental results, and clarify how modest scene variations are handled (e.g., S2). Here, we elaborate specifically on how AR fits into the certification pipeline for visual autonomy.

Your understanding of the formation flight use case is broadly accurate. The pipeline involves:

• Scene reconstruction: We assume a high-fidelity 3DGS model of the scene including its variations. (This step is valuable even beyond verification—for example, to train perception or control policies.) In the S2 experiments, to model simple background variation, we generate a foreground 3DGS for the airplane and interpolate the background separately. This construction of the 3DGS is tailored to the specific variation being studied.

• Uncertainty propagation via AR: AR propagates camera pose and scene uncertainty through the 3DGS model to generate an abstract image—a conservative over-approximation of all rendered images that could arise under bounded pose and scene perturbations.

• Downstream verification: This abstract image is then passed to a neural verification tool to certify that the downstream classifier or pose estimator remains within acceptable error bounds across the entire range of camera motions (and scene variations).

In the context of formation flight, AR enables formal end-to-end reasoning about the vision pipeline. It verifies that, under all feasible approach angles and modest scene variations, the downstream system behaves predictably. The bounds produced by AR define a region of guaranteed correct behavior over the space of (camera and scene) variations.

What happens after certification?

Successfully verifying the pipeline produces certification artifacts for the system and the ML models—the reconstructed scene, region of correct behavior (often called the operating design domain or ODD), and verification results. These artifacts can be used as part of a broader safety case—e.g., internal within an organization or for FAA or EASA—just as test results and formal proofs are used today in DO-178C workflows for airborne systems.

Beyond certification, AR supports design iteration:

• If verification fails, the counterexample region highlights scenarios where perception is fragile, guiding data augmentation or retraining. See exemplary results below.

• If verification is inconclusive, it flags regions requiring tighter abstractions or further analysis.

• If verification succeeds, it provides provable guarantees over a space of structured inputs—something empirical testing cannot offer.

Thus, AR is both a certification tool and a development aid, similar to how SMT solvers (e.g., CBMC) are used in safety-critical software. While modest in scope today, AR introduces a new formal capability that can scale with increasing regulatory demands on vision-based autonomy.

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:

Response to W1 — Why use RGB, not SH to model GS color:

We 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.

While 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.

That 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.

Response to W2 — How to properly define a linear set of the Scene Sc?:

In 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.

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? :

The 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.

In 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.

In 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.

Illustrative Example:

Let us consider the following setup:

1. Scalars: $a={0.8,0.5}$, $d={x,x+1}$, where $x\in [-1,1]$,

2. Goal: Compute a tight and worst-case bound of the following procedure:

Step1: $as=sort(a,d)$;

Step2: $oc[0]=1$;

Step3: $oc[1]=1-as[0]$;

Step4: $pc=oc[0]\times as[0]+oc[1]\times as[1]$;

Naïve interval approach:

Because 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:

$as[0], as[1] \in [0.5,0.8]$;

$oc[1] \in [0.2,0.5]$.

The resulting interval bound for pc is:

$pc\in [1⋅0.5+0.2⋅0.5,1⋅0.8+0.5⋅0.8]= [0.6,1.2]$

This yields a very loose bound.

Proposed VR-Ind approach:

Using 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:

Step 1: $oc[0]=(1-a[0]\times Ind(d[0]-d[0]))\times (1-a[1]\times Ind(d[0]-d[1]))$

Step 2: $oc[1]= (1-a[0]\times Ind(d[1]-d[0]))\times (1-a[1]\times Ind(d[1]-d[1]))$

Step 3: $pc=oc[0]\times a[0]+oc[1]\times a[1]$;

Given that

$d[0]-d[1]=x-(x+1)=-1<0 \rightarrow Ind(-1)=0$;

$d[1]-d[0]=(x+1)-x=1>0 \rightarrow Ind(1)=1$;

$Ind(0)=0$;

We obtain that

$oc[0]=(1-0.8\times 0)(1-0.5\times 0)=1$;

$oc[1]=( 1-0.8\times 1)(1-0.5\times 0)=1-a[0]=0.2$;

$pc= 1\times 0.8+0.2\times 0.5=0.9$.

Thus, 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.

The 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.

Response to Q – Why are there N/A values for PSNR/SSIM in Table 5 of the updated appendix? :

The complete Table 5 in the updated appendix:

Additional result on AR under scene variation:

The table below shows our framework capable of handling scene variation.

Caption: 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.

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.

Your review raises thoughtful concerns regarding the practical value of abstract rendering, particularly:

(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,

(W2) that simple empirical sampling may be sufficient in most practical settings, and

(W3) that the paper does not demonstrate end-to-end verification at the semantic or decision level.

We 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.

W1

As 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.

This 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.

As 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.

This 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.

In 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.

As 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.

In 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.

W2 & Q2

Empirical 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.

Whether 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.

It 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.

In 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.

While 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.

W3

We 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.

The 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.

The 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.

In 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.

Thus, 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.

Q3

Please see our response to W1 of reviewer n9Gh.

Reference

[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.

[2] Duong, Hai, ThanhVu Nguyen, and Matthew Dwyer. "A dpll (t) framework for verifying deep neural networks." arXiv preprint arXiv:2307.10266 (2023).

[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.

Dear reviewers, Thanks so much for reviewing the paper. The discussion period ends soon. To ensure enough time to discuss this with the authors, please actively engage in the discussions with them if you have not done so.