Da Wei Zheng

Hsien-Chih Chang, Jonathan Conroy, Zihan Tan et al.

In this paper we construct distance sketches for intersection graphs of arbitrary path-connected regions in the plane (known as the string graphs) in the constant and $1+\varepsilon$ distortion regimes. Furthermore, the distance sketches themselves are planar graphs. First, we show that every unweighted string graph $G$ has an $O(1)$-distortion planar emulator: that is, there exists an edge-weighted planar graph $H$ containing every vertex in $G$, such that every pair of vertices $(u,v)$ satisfies $δ_G(u,v) \le δ_H(u,v) \le O(1) \cdot δ_G(u,v)$. Furthermore, we show that for any constant $\varepsilon > 0$, there is an edge-weighted planar graph $H'$ such that every pair of vertices $(u,v)$ satisfies $δ_G(u,v) \le δ_{H'}(u,v) \le (1+\varepsilon) \cdot δ_G(u,v) + O(\varepsilon^{-4}\textrm{poly}\log n)$. No previous constructions of sparse distance sketches were known even for intersection graphs of simple shapes like axis-parallel rectangles or fat convex polygons. As applications, we construct the first $(1+\varepsilon, +O(1))$ mixed-distortion tree cover and distance oracle for arbitrary string graphs, as well as the first additive $+(\varepsilonΔ+O(1))$-distortion embedding of string graphs $G$ with diameter $Δ$ into graphs of constant treewidth $O(\varepsilon^{-4})$.

Jack Spalding-Jamieson, Eliot Wong Robson, Da Wei Zheng

For very large values of $k$, we consider methods for fast $k$-means clustering of massive datasets with $10^7\sim10^9$ points in high-dimensions ($d\geq100$). All current practical methods for this problem have runtimes at least $Ω(k^2)$. We find that initialization routines are not a bottleneck for this case. Instead, it is critical to improve the speed of Lloyd's local-search algorithm, particularly the step that reassigns points to their closest center. Attempting to improve this step naturally leads us to leverage approximate nearest-neighbor search methods, although this alone is not enough to be practical. Instead, we propose a family of problems we call "Seeded Approximate Nearest-Neighbor Search", for which we propose "Seeded Search-Graph" methods as a solution.

Yuchen Tian, Ruiyuan Huang, Xuanwu Wang et al.

Large Language Models (LLMs) for formal theorem proving have shown significant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: EvolAST, an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and EvolDomain, which leverages LLMs to address semantic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose EvolDifficulty, which uses carefully designed evolutionary instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data to train EvolProver, a 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state-of-the-art (SOTA) on FormalMATH-Lite with a 53.8% pass@32 rate, surpassing all models of comparable size, including reasoning-based models. It also sets new SOTA records for non-reasoning models on MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32), and Ineq-Comp-Transformed (34.0% pass@32). Ablation studies further confirm our data augmentation pipeline's effectiveness across multiple benchmarks.

Paul Liu, Jack Spalding-Jamieson, Brandon Zhang et al.

This paper examines the approach taken by team gitastrophe in the CG:SHOP 2021 challenge. The challenge was to find a sequence of simultaneous moves of square robots between two given configurations that minimized either total distance travelled or makespan (total time). Our winning approach has two main components: an initialization phase that finds a good initial solution, and a $k$-opt local search phase which optimizes this solution. This led to a first place finish in the distance category and a third place finish in the makespan category.