arXiv subjects

Xu Miao

Publications and source records attributed to Xu Miao.

5 recordsLinked to original sources

arXiv2026

Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications

Finite model finders cannot witness an Austin law: an identity whose finite models are all trivial but which has a nontrivial infinite model. We introduce rank-decreasing sparse trace-tree magmas, finitely presented total operations on a countably infinite constructor-tree carrier. The default product pairs its arguments; finitely many positive Horn clauses define exceptions. Our main procedure derives clauses from symbolic evaluation traces. For every model found, it proves functionality of the exceptional relation by descent on constructor size, proves the identity by exhaustive symbolic case analysis, and emits a self-contained Lean 4 certificate. A least simultaneous fixed point gives an implementation-independent semantics, so bounded search may miss models but cannot invalidate certified results. On ETP's 96 order-five Austin candidates, we discover and Lean-verify infinite countermodels for 28 identities with no prior public classification in our audit. They form 14 duality classes and establish 28 new Austin classifications. Four ALPS-known cases bring the total to 32 certified candidates. On Canonical-4187, the deduplicated union of Order5-130 and the 4,141-row ALPS pool, a fresh trace run produces 636 certificates, all accepted by Judge v3. At equal resource limits, Vampire 5.0.1, E 3.5.1, and complete Twee 2.6.1 jointly prove implications in 94 canonical classes. Only Twee returns trusted counter-satisfiable outcomes, for 18 classes; independent finite-side certificates force 16 to be infinite. None of these ATPs emits an explicit model or Lean certificate, and none decides the 28 new classifications. To the best of our audit, this is the first automated system to synthesize this trace-tree model family, generate well-founded inversion proofs, and emit self-contained Lean 4 certificates.

cs.LO↗

arXiv2026

World Narrative Model for Highly Controllable Video Generation: A Paradigm Shift from Pixel Sampling to Physical World Orchestration

The fundamental obstacle to industrial grade video generation is the lack of controllability: existing models treat video as a pixel distribution sampling problem, bypassing the explicit, instance level $4D$ $(3D + T)$ physical world. Consequently, content creators cannot specify geometry, motion, camera parameters, or lighting in a deterministic, quantitative way, leading to the infamous ''gacha'' loop that makes professional content creation prohibitively inefficient and expensive. To address this, we introduce the World Narrative Model (WNM), a paradigm that decouples what to render -- the structured physical narrative -- from how to render -- the pixel generation process. WNM replaces end-to-end black-box sampling with orchestrated $4D$ pre-visualization for media generation. Collaborative agents translate sparse multimodal inputs, including text, reference videos, and sketches, into a fully editable world representation with scene geometry, object layouts, character/animal skeleton motion, trajectories, camera motion, and lighting at quantitative, physically meaningful granularity. This representation acts as a deterministic structural blueprint that drives existing video foundation models, either frozen or lightly adapted, to render final footage, turning the base model into a faithful neural shader. Built on this engine, our human-AI platform supports automatic world generation and pre-visualization aligned with professional filmmaking pipelines, while director consoles enable seamless human refinement. Experiments show that WNM greatly reduces probabilistic ``gacha'' calls and produces videos whose layout, motion, and cinematography closely follow creator intent. The framework is open and modular, allowing each component, such as world representation, control agents, and adapters, to be independently improved. Project website: https://glassroom.sjtu.edu.cn/WNM/.

cs.CV↗

arXiv2025

FlowMesh: A Service Fabric for Composable LLM Workflows

AI deployment increasingly resembles a pipeline of data transformation, fine-tuning, and agent interactions rather than a monolithic LLM job; recent examples include RLHF/RLAIF training and agentic workflows. To cope with this shift, we propose FlowMesh, a multi-tenant service fabric that executes and optimizes these workloads as one shared service instead of isolated pipelines. It decomposes workflows into fine-grained operators with recorded lineage, enabling de-duplication of work across users and batching requests on the same hardware while preserving per-workflow provenance. A global control plane maintains a cluster-wide pool of ready operators and uses a single utility function to pick both the batch and the worker, balancing throughput, cost, and data locality on heterogeneous GPUs. The data plane is an elastic fleet of stateless workers backed by a content-addressable store, enabling rapid, automatic scale-out, safe retry after preemption, and portability across managed clusters such as Kubernetes and geo-distributed GPU marketplaces such as Vast.ai. Compared with baseline solutions, FlowMesh achieves up to 3.8x cost reduction and 2.0x lower energy usage, provides a similar or better latency profile, and remains efficient under dynamic and failure-prone conditions.

cs.DC↗

arXiv2025

An Empirical Study on Eliciting and Improving R1-like Reasoning Models

In this report, we present the third technical report on the development of slow-thinking models as part of the STILL project. As the technical pathway becomes clearer, scaling RL training has become a central technique for implementing such reasoning models. We systematically experiment with and document the effects of various factors influencing RL training, conducting experiments on both base models and fine-tuned models. Specifically, we demonstrate that our RL training approach consistently improves the Qwen2.5-32B base models, enhancing both response length and test accuracy. Furthermore, we show that even when a model like DeepSeek-R1-Distill-Qwen-1.5B has already achieved a high performance level, it can be further refined through RL training, reaching an accuracy of 39.33% on AIME 2024. Beyond RL training, we also explore the use of tool manipulation, finding that it significantly boosts the reasoning performance of large reasoning models. This approach achieves a remarkable accuracy of 86.67% with greedy search on AIME 2024, underscoring its effectiveness in enhancing model capabilities. We release our resources at the STILL project website: https://github.com/RUCAIBox/Slow_Thinking_with_LLMs.

cs.CL↗

arXiv2010

Large Margin Boltzmann Machines and Large Margin Sigmoid Belief Networks

Current statistical models for structured prediction make simplifying assumptions about the underlying output graph structure, such as assuming a low-order Markov chain, because exact inference becomes intractable as the tree-width of the underlying graph increases. Approximate inference algorithms, on the other hand, force one to trade off representational power with computational efficiency. In this paper, we propose two new types of probabilistic graphical models, large margin Boltzmann machines (LMBMs) and large margin sigmoid belief networks (LMSBNs), for structured prediction. LMSBNs in particular allow a very fast inference algorithm for arbitrary graph structures that runs in polynomial time with a high probability. This probability is data-distribution dependent and is maximized in learning. The new approach overcomes the representation-efficiency trade-off in previous models and allows fast structured prediction with complicated graph structures. We present results from applying a fully connected model to multi-label scene classification and demonstrate that the proposed approach can yield significant performance gains over current state-of-the-art methods.

cs.LG↗