FMitF: Track I: Visual Computing Meets Formal Verification: Certified Rendering, Geometry, and Video Generation

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

When one watches a movie with computer-generated special effects, plays a video game, or sees a robot assemble parts in a factory, one is witnessing visual computing in action. The technology allows computers to create, analyze, and interact with images and videos. Despite their widespread use, these technologies currently lack rigorous quality guarantees. This means that a medical imaging system might produce misleading visualizations, a digital twin used for industrial simulation might fail to detect collisions, or a robot arm might misjudge the position of objects it needs to grasp. This project addresses this critical gap by applying formal methods, the mathematical techniques that prove computer systems behave correctly, to visual computing systems. The project's novelties are the development of mathematical frameworks that can provide assurance about the quality and correctness of visual computing systems. The project's impacts include creating foundations for visual systems that can be mathematically proven to work correctly in autonomous vehicles, augmented reality and virtual reality (AR/VR) environments, and industrial control, while making these advanced techniques accessible to developers and students through education programs and open-source tools. The research establishes connections between two previously separate communities, formal methods researchers who develop mathematical techniques for proving system correctness and visual computing specialists who create graphics, vision, and simulation systems, through three integrated thrusts. First, the investigators develop abstract rendering algorithms that propagate uncertainties through neural scene representations to compute guaranteed pixel-level error bounds, enabling verification of perception-based controllers in simulation environments. Second, they handle neural signed distance functions using neural network verification techniques, allowing for provable geometric reasoning. Third, they develop certifiable physics simulation and video generation techniques to create end-to-end guarantees for video synthesis. These advances support the inclusion of visual systems in formal verification pipelines, addressing a significant limitation in current safety verification approaches. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.