arXiv:2510.25015v4 Announce Type: replace-cross Abstract: We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.

arXiv:2405.14504v2 Announce Type: replace-cross Abstract: Spatiotemporal prediction is important in solving natural problems and processing video frames, especially in weather forecasting and human action recognition. Recent advances attempt to incorporate prior physical knowledge into the deep learning framework to estimate the unknown governing partial differential equations (PDEs) in complex dynamics, which have shown promising results in spatiotemporal prediction tasks. However, previous approaches only restrict neural network architectures or loss functions to acquire physical or PDE features, which decreases the representative capacity of a neural network. Meanwhile, the updating process of the physical state cannot be effectively estimated. To solve the problems mentioned above, we introduce a physical-guided neural network, which utilizes an adaptive second-order Runge-Kutta method with physical constraints to model the physical states more precisely. Furthermore, we propose a frequency-enhanced Fourier module to strengthen the model's ability to estimate the spatiotemporal dynamics. We evaluate our model on both spatiotemporal and video prediction tasks. The experimental results show that our model outperforms several state-of-the-art methods and performs the best in several spatiotemporal scenarios with a much smaller parameter count.