Yunsong Yang

Yunsong Yang, Genji Yuan, Jinjiang Li

In order to fully utilize spatial information for segmentation and address the challenge of handling areas with significant grayscale variations in remote sensing segmentation, we propose the SFFNet (Spatial and Frequency Domain Fusion Network) framework. This framework employs a two-stage network design: the first stage extracts features using spatial methods to obtain features with sufficient spatial details and semantic information; the second stage maps these features in both spatial and frequency domains. In the frequency domain mapping, we introduce the Wavelet Transform Feature Decomposer (WTFD) structure, which decomposes features into low-frequency and high-frequency components using the Haar wavelet transform and integrates them with spatial features. To bridge the semantic gap between frequency and spatial features, and facilitate significant feature selection to promote the combination of features from different representation domains, we design the Multiscale Dual-Representation Alignment Filter (MDAF). This structure utilizes multiscale convolutions and dual-cross attentions. Comprehensive experimental results demonstrate that, compared to existing methods, SFFNet achieves superior performance in terms of mIoU, reaching 84.80% and 87.73% respectively.The code is located at https://github.com/yysdck/SFFNet.

Yunsong Yang, Simon Guilloud, Viktor Kunčak

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, with axiom schemas of Tarski-Grothendieck set theory. We carry this embedding in the Lisa proof assistant. On top of this foundation, we implement a proof-producing bidirectional type-checking tactic to compute proofs for typing judgements, with partial support for subtyping. We present examples showing how our approach enables automated reasoning for dependent types that is fully verified from set-theoretic axioms and deduction rules for schematic first-order logic with equality. Because types are merely sets, the resulting formalism supports equality that applies to all types and values and permits the usual substitution rules.