arXiv subjects

Chuxiao Zeng

Publications and source records attributed to Chuxiao Zeng.

3 recordsLinked to original sources

arXiv2026

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited insight into models' step-level formal reasoning. Evaluating this capability separately enables finer-grained diagnosis of model limitations than theorem-level evaluation alone. To fill this evaluation gap, we introduce ProofGap, a fine-grained benchmark for step-level formal reasoning. ProofGap is constructed through a natural-language proof-processing pipeline that decomposes each reasoning step into one or more aligned proof gaps. Applying this pipeline to natural-language solutions to 3,015 exercises in B. P. Demidovich's Problems in Mathematical Analysis yields 26,116 gaps. The benchmark focuses on mathematical analysis, a domain that remains challenging for current models. By supplying the local context and target explicitly, gap completion isolates local formal proof construction from end-to-end proof composition, enabling more precise localization of model failures. Natural-language solutions serve as the provenance of these obligations, while the benchmark task itself starts from an already formalized local context and goal. Beyond benchmarking, the same pipeline may support future proof-verification systems, provided that semantic translation and sequential proof composition are handled reliably.

cs.PL↗

arXiv2024

Implicit Swept Volume SDF: Enabling Continuous Collision-Free Trajectory Generation for Arbitrary Shapes

In the field of trajectory generation for objects, ensuring continuous collision-free motion remains a huge challenge, especially for non-convex geometries and complex environments. Previous methods either oversimplify object shapes, which results in a sacrifice of feasible space or rely on discrete sampling, which suffers from the "tunnel effect". To address these limitations, we propose a novel hierarchical trajectory generation pipeline, which utilizes the Swept Volume Signed Distance Field (SVSDF) to guide trajectory optimization for Continuous Collision Avoidance (CCA). Our interdisciplinary approach, blending techniques from graphics and robotics, exhibits outstanding effectiveness in solving this problem. We formulate the computation of the SVSDF as a Generalized Semi-Infinite Programming model, and we solve for the numerical solutions at query points implicitly, thereby eliminating the need for explicit reconstruction of the surface. Our algorithm has been validated in a variety of complex scenarios and applies to robots of various dynamics, including both rigid and deformable shapes. It demonstrates exceptional universality and superior CCA performance compared to typical algorithms. The code will be released at https://github.com/ZJU-FAST-Lab/Implicit-SVSDF-Planner for the benefit of the community.

cs.RO↗

arXiv2022

Video-driven Neural Physically-based Facial Asset for Production

Production-level workflows for producing convincing 3D dynamic human faces have long relied on an assortment of labor-intensive tools for geometry and texture generation, motion capture and rigging, and expression synthesis. Recent neural approaches automate individual components but the corresponding latent representations cannot provide artists with explicit controls as in conventional tools. In this paper, we present a new learning-based, video-driven approach for generating dynamic facial geometries with high-quality physically-based assets. For data collection, we construct a hybrid multiview-photometric capture stage, coupling with ultra-fast video cameras to obtain raw 3D facial assets. We then set out to model the facial expression, geometry and physically-based textures using separate VAEs where we impose a global MLP based expression mapping across the latent spaces of respective networks, to preserve characteristics across respective attributes. We also model the delta information as wrinkle maps for the physically-based textures, achieving high-quality 4K dynamic textures. We demonstrate our approach in high-fidelity performer-specific facial capture and cross-identity facial motion retargeting. In addition, our multi-VAE-based neural asset, along with the fast adaptation schemes, can also be deployed to handle in-the-wild videos. Besides, we motivate the utility of our explicit facial disentangling strategy by providing various promising physically-based editing results with high realism. Comprehensive experiments show that our technique provides higher accuracy and visual fidelity than previous video-driven facial reconstruction and animation methods.

cs.CV↗