Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib’s definitional framework. However, frontier mathematics is often exploratory and prototype-heavy, relying on bespoke constructions that deviate from standard libraries. In this work, we evaluate the robustness of current ATP systems when applied to a novel definitional framework. We introduce TaoAnalysisBench, an undergraduate-level benchmark derived from the exercises and definitional frameworks given in Terence Tao’s Analysis I, which formalizes analysis by constructing core mathematical concepts from scratch, without relying on standard Mathlib definitions, as well as by mixing from-scratch and MathLib constructions. For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem. To isolate the effect of definitional frameworks, we additionally translate every problem into a mathematically equivalent Mathlib formulation, yielding paired TaoAnalysisBench-Mathlib statements for direct comparison. While state-of-the-art ATP models perform capably within the MathLib framework, performance drops by an average of 2.18x on the definitionally equivalent Tao formulation. This indicates that the main bottleneck is limited generalization across definitional frameworks rather than task difficulty. TaoAnalysisBench thus highlights a gap between benchmark performance and applicability, and provides a concrete foundation for developing and testing provers better aligned with research mathematics.

Large language models (LLMs) have demonstrated strong reasoning ability when given additional compute at inference time. However, existing inference-time scaling methods are fundamentally limited by their design. On the one hand, goal-oriented approaches, such as Line or Tree Search, refine candidate solutions using previous feedback but are vulnerable to sequential dependence, often collapsing into suboptimal reasoning trajectories. On the other hand, process-oriented approaches such as Best-of-N sampling encourage diversity through random exploration but lack feedback mechanisms, leading to inefficient computation allocation and unguided search. In this work, we propose EvoMo, a novel inference-time scaling approach that unifies both paradigms by embedding a globally evolving strategy pool into MCTS, where each node expansion selects reasoning strategies under an -soft policy. To further avoid stagnation in familiar strategies, we introduce a momentum-based optimization mechanism that monitors similarity among generated solutions and encourages the exploration of underutilized strategies. We also present a theoretical analysis of the effectiveness of the proposed momentum mechanism by modeling it as a self-evolving pool of actions. Across benchmarks, EvoMo reveals significant performance gains over SOTA inference scaling methods. We observe competitive performance, like in APPS and CodeContests, with up to a 4.5% and 3.63% relative gain in Pass@K compared to the leading baseline within 40 search-budget, highlighting the potential of hybrid evolutionary search as a general paradigm for test-time scaling.

Taxonomy Expansion, which relies on modeling concepts and concept relations, can be formulated as a set representation learning task. The generalization of set, fuzzy set, incorporates uncertainty and measures the information within a semantic concept, making it suitable for concept modeling. Existing works usually model sets as vectors or geometric objects such as boxes, which are not closed under set operations. In this work, we propose a sound and efficient formulation of set representation learning based on its volume approximation as a fuzzy set. The resulting embedding framework, Fuzzy Set Embedding, satisfies all set operations and compactly approximates the underlying fuzzy set, hence preserving information while being efficient to learn, relying on minimum neural architecture. We empirically demonstrate the power of FUSE on the task of taxonomy expansion, where FUSE achieves remarkable improvements up to 23% compared with existing baselines. Our work marks the first attempt to understand and efficiently compute the embeddings of fuzzy sets.