Search arXiv⌕ Search

arXiv subjects

Zichen Wang

Publications and source records attributed to Zichen Wang.

At least 19 recordsLinked to original sources
arXiv2026

From Watching to Steering: Enabling Human-Coding Agent Collaboration through Execution Traces

Recent advances in large language models (LLMs) have enabled coding agents to autonomously perform complex software development tasks, yet their long-running execution remains difficult for users to inspect, understand, and steer. We present Vibetrace, an interactive trace visualization and intervention system for agentic programming built upon OpenCode. Vibetrace introduces a human-agent collaboration paradigm of Observe, Understand, Intervene, and Evolve. It (1) visualizes agent workflows as interactive execution traces for inspecting actions, intermediate states, and failures; (2) enables users to fork execution from prior steps and provide targeted corrections without restarting validated progress; and (3) distills traces and human feedback into reusable skills for continual agent evolution. On SWE-bench Verified, distilled skills reduce input tokens by 23.0% and cost by 15.5%, while improving pass rate from 65.0% to 68.0%. User studies further demonstrate improved accuracy and efficiency over conventional log-based interaction.

cs.HC↗
arXiv2026

remage: a Geant4-based simulation framework for low-background experiments

Monte Carlo simulations are an essential tool for data modeling and experimental design in low-background physics. These simulations typically demand a considerable effort, with each collaboration developing and maintaining its own complex Geant4 application. In this paper we present the design and validation of remage, which is an open-source framework designed to standardize these simulations and significantly reduce this effort. Its design separates the geometry, built with dedicated Python tools, from the compiled application. It provides a physics list and event generators tuned to radiogenic and cosmogenic backgrounds, output tailored to the most common detector types, and robust validation backed by modern software development practices. The software is distributed ready to use and scales efficiently with the computing resources that demanding simulations require. remage has been primarily developed for the LEGEND experiment, but is applicable to a wide variety of experiments.

physics.ins-det↗
arXiv2026

Learning from Unverified Peers via Shared Residual Distillation

A language model can generate several solutions to the same problem, some leading to correct answers and others to incorrect ones. Many post-training methods turn these trajectories into learning signals using supervision from reference answers, verifiable feedback, or external teachers. Without such supervision, learning from the model's own generations becomes less straightforward, as their correctness cannot be reliably assessed. An incorrect solution may nevertheless contain useful intermediate reasoning, so its value as supervision need not be determined solely by its final answer. Can a model improve by learning from its unverified peer solutions without first determining which are correct? We propose Shared Residual Distillation (SRD), an on-policy self-distillation method that learns from the model's own unverified peer trajectories. SRD compares how peers change the prediction distribution relative to a control, retaining adjustments that agree in direction and are conservative in magnitude. This yields supervision without treating any complete solution as correct, and the trained model requires no peers at inference time. Starting from the corresponding base models, SRD raises mean AIME24--26 avg@12 from 11.02 to 16.20 on Qwen3-1.7B, from 19.07 to 45.46 on Qwen3-4B, and from 21.39 to 54.44 on Qwen3-8B. Controlled ablations support the value of the shared-residual construction, and we observe no degradation relative to the base models on two general-capability benchmarks.

cs.AI↗
arXiv2026

Constraining Particle Stiffness in Asteroid Regolith from Early-Time High-Speed Penetrator Dynamics under Local Granular Variability

Mechanical properties of rubble-pile asteroid regolith remain poorly constrained because contact responses depend on both material properties and local particle configuration. This study examines whether early-time high-speed penetrator dynamics can constrain particle stiffness, represented by the particle Young's modulus E, within a controlled discrete-element model. A bidirectionally coupled EDEM-Adams discrete-element-multibody model is used to screen six parameters: Young's modulus, Poisson's ratio, coefficient of restitution, static friction coefficient, rolling friction coefficient, and adhesion strength. Five Young's-modulus levels are then tested at the same 17 spatial locations in one settled granular bed, giving 85 simulations with location-matched comparisons across modulus levels. Within the 75-90 m s^-1 speed range, varying Young's modulus yields the clearest and most systematic differences in probe deceleration, whereas the other parameters have weaker effects over the tested ranges. Validation by withholding all modulus cases at one location in turn indicates that the early response is more informative for distinguishing broad modulus ranges than adjacent modulus levels. Mesoscale analysis links the response differences to concentrated interface load sharing and spatially extended three-dimensional high-capacity contact paths as Young's modulus increases. The results provide a numerical basis for narrowing the particle Young's-modulus range from high-speed penetration responses despite local granular variability. Quantitative application to real asteroid regolith requires further experimental validation.

astro-ph.EP↗
arXiv2026

Causal Influence Maximization with Steady-State Guarantees

Classical influence maximization optimizes expected reach, which can be misaligned with welfare when exposures have heterogeneous, saturating, or adverse effects. We study seed selection for steady-state causal welfare under network interference. Under our exposure-separable outcome model and weak independent live-edge propagation, a deterministic surrogate built from expected activations and exposure counts approximates welfare with uniform $O(\varepsilon^2)$ error for a fixed graph and seed budget, where $\varepsilon$ bounds edge activation probabilities. Building on this reduction, our two-stage method, CIM, learns shape-constrained exposure-response functions from logged diffusion-outcome data and estimates expected activations and exposures by Monte Carlo simulation. For unregularized fits on a design that covers the evaluated exposures, and under noise and simulation conditions, we bound the welfare-estimation error uniformly over seed sets, separating structural, statistical, and simulation errors; with an approximation guarantee for the optimizer, the bound transfers to the selected seeds. Experiments on real network topologies with simulated outcomes and a synthetic benchmark show that CIM attains the highest mean welfare among the compared methods.

stat.ME↗
arXiv2026

When Greedy Sampling Explores: KL-Regularized Contextual Bandits without Eluder-Dimension Dependence

We study KL-regularized contextual bandits under both reward and preference feedback. While existing regret guarantees typically depend on the eluder dimension, we show that simple greedy sampling can achieve polylogarithmic regret without explicit dependence on this complexity measure. For reward feedback, we analyze a greedy algorithm that samples directly from the Gibbs policy induced by the estimated reward. We extend the result to preference feedback under both general preference and Bradley--Terry models, while also sharpening existing dimension-dependent guarantees. Our analysis reveals a trade-off between greedy sampling and upper confidence bound-style exploration: greedy sampling enjoys stronger regret guarantees when KL regularization is sufficiently strong, whereas additional exploration yields sharper bounds as the regularization weakens.

cs.LG↗
arXiv2026

Scalable Incremental Robustness Analysis of Neural Network Feedback Systems

Semidefinite programming (SDP) certificates for feedback systems containing deep neural networks (NNs) typically scale with the total number of neurons, whereas small-gain tests are scalable but can be highly conservative. This paper develops a unified and scalable framework for incremental robust stability and performance analysis of feedback interconnections involving high-dimensional NNs and unmodeled dynamics. By combining a structured decomposition of the full-order SDP condition with scalable Lipschitz constant estimation algorithms, we derive reduced verification conditions that certify incremental convergence and incremental $\ell_2$-gain bounds. The dimensions of the resulting control-analysis linear matrix inequalities (LMIs) depend only on the widths of the last two network layers and are \textit{independent of network depth}. The framework preserves the coupling between the plant and the NN, with the incremental small-gain condition recovered as a special case. To further reduce conservatism, we develop a multi-round alternating update scheme that iteratively refines the coupling variables while preserving scalability. Numerical experiments show that the proposed framework achieves state-of-the-art incremental $\ell_2$-gain bounds for large-scale NN feedback systems.

math.OC↗
arXiv2026

Training Large Language Models for Small-Molecule Design with Synthetic Task Scaling

Designing viable drug candidates requires searching a combinatorially large and rugged chemical space for molecules that satisfy multiple, often competing, objectives. Large language models (LLMs) provide a useful generative prior for this problem because of their representational capacity, reasoning ability, and flexibility when incorporating information from the external environment. While reinforcement learning from verifiable rewards (RLVR) can be used to improve the capabilities of LLMs, many chemically relevant scoring functions require hours or even days per evaluation, making them prohibitively expensive to use directly during online training. Here, we investigate whether LLMs can learn molecular design strategies from cheaper synthetic tasks that generalize to expensive molecular lead optimization settings. We find that curriculum-based training recipes that gradually incorporate more challenging synthetic design tasks enable strong performance that surpasses that of much larger frontier models on structure-based lead optimization. Our results suggest that scaling post-training using synthetic tasks is an effective strategy for adapting LLMs to high-cost experimental scenarios that are too expensive to directly train on.

cs.LG↗
arXiv2026

Blending Concepts: Benchmarking Visual Metaphor Generation in Text-to-Image Models

Text-to-image (T2I) models have achieved remarkable success at faithfully rendering specified objects and attributes, yet their ability to produce visual metaphors, images that convey abstract ideas by combining elements from two distinct domains, remains largely unexamined. To bridge this gap, we introduce VMetaphor-Bench, the first benchmark for evaluating visual metaphor generation in T2I models. It comprises 1,500 visual metaphors curated from real-world creative imagery, organized into three levels and ten categories, with each sample paired with two prompts of differing specificity. For evaluation, we develop a hybrid framework within an MLLM-as-judge paradigm, combining a multiple-choice question (MCQ) based protocol of 9,594 questions across four levels of metaphorical fidelity with a dimension-based scoring protocol along three perceptual dimensions. Extensive evaluation of 11 representative T2I models reveals that even the strongest proprietary models struggle with compositional structuring and cross-domain mapping, key aspects of metaphorical expression, highlighting visual metaphor generation as an important frontier for future T2I research.

cs.CV↗
arXiv2026

A counterexample to global convergence of classical DFP under the standard strong Wolfe conditions

A long-standing open question in quasi-Newton optimization asks whether the classical Davidon--Fletcher--Powell (DFP) method converges globally on uniformly convex objectives when all accepted steps satisfy the standard weak Wolfe conditions. We show that the answer is no, even under the standard strong Wolfe conditions. Fix $0<c_1<2/3$ and $2/3\le c_2<1$. We construct a function $f\in C^2(\mathbb{R}^2)$ such that $\frac{1}{2}I\preceq\nabla^2 f(x)\preceq\frac{3}{2}I$ for all $x\in\mathbb{R}^2$. We also choose a fixed positive definite initial inverse Hessian approximation and a sequence of positive step lengths. The classical DFP iteration is well defined, and all accepted steps satisfy the standard strong Wolfe conditions, but $|\nabla f(x_k)|$ converges to a positive constant. The global Hessian condition number is at most three. The construction uses an alternating two-step DFP sequence near a one-dimensional invariant center manifold. Along this sequence, the smaller eigenvalue of the inverse Hessian approximation tends to zero. The changes in the gradient norm between cycle starts are summable, but the total rotation of the associated eigenvectors is unbounded. The accumulation points of the DFP sequence form a circle. A uniform separation bound allows us to interpolate the prescribed function values and gradients. We add smooth functions with pairwise disjoint supports to a quadratic and keep the global Hessian bounds. An affine change of variables gives an identity-initialized example with problem-dependent Hessian bounds. An orthogonal direct sum extends the result to every dimension $n\ge 2$.

math.OC↗
arXiv2026

A Fixed-Penalty Linearized Augmented Lagrangian Method with Classical Multiplier Updates

Augmented Lagrangian methods are effective for nonlinear equality-constrained optimization, but solving their nonlinear primal subproblems can be expensive. For smooth nonconvex problems with deterministic or stochastic objectives, we propose a nonlinear-residual linearized augmented Lagrangian method (NR-LALM) that replaces this subproblem by a regularized Gauss-Newton-type step while retaining the classical multiplier update based on the nonlinear constraint residual. The resulting step is computed from one symmetric positive-definite linear system, but the mismatch between the linearized primal model and the nonlinear-residual update produces a quadratic constraint-linearization error in the multiplier identity. We show that this error can be controlled under local regularity; multiplier boundedness and trajectory localization are derived rather than assumed. With fixed, accuracy-independent parameters, deterministic NR-LALM finds an $\varepsilon$-approximate Karush-Kuhn-Tucker (KKT) pair in $O(\varepsilon^{-2})$ iterations and first-order oracle evaluations. For stochastic objectives, a projected stochastic path-integrated differential estimator with safeguarded restarts requires, in expectation, $O(\varepsilon^{-3})$ stochastic-gradient evaluations and $O(\varepsilon^{-2})$ constraint and Jacobian evaluations. Compactness and a Kurdyka-Lojasiewicz condition further yield finite-length convergence of the deterministic primal-dual sequence. An optional minimum-norm second-order correction reduces the constraint-linearization error from second to fourth order without changing the complexity orders. All theoretical results are formalized in Lean 4. Numerical experiments confirm the predicted error orders and show favorable performance on high-dimensional deterministic and stochastic problems.

math.OC↗
arXiv2026

Antigen-specific Antibody Multi-modal Foundation Model for Functional Antibody Design

Antibodies are essential proteins that play a central role in immune recognition by binding specific antigen molecules. Although recent protein language models have enabled progress in single-chain protein modeling and generation, they often fall short in antigen-specific antibody design, where effective modeling requires explicit pairing between antibody and antigen, particularly at the epitope level. To address these limitations, we introduce AAMFM, an Antigen-specific Antibody Multimodal Foundation Model that learns unified representations of antibody sequences and structures conditioned on antigen context. AAMFM incorporates rich antigen information including geometric interfaces and epitope annotations via a cross-modal adapter, enabling joint modeling of antibody-antigen interactions in a shared latent space. To further guide the model toward functional relevance, we fine-tune AAMFM using Calibrated Direct Preference Optimization (Cal-DPO), leveraging preference signals extracted from a strong structural prior to align learning with binding-specific objectives. Extensive experiments demonstrate that AAMFM achieves state-of-the-art performance in functional antibody design, revealing its potential for antigen-specific antibody engineering. Our code is available at https://github.com/XL-S224/AAMFM.

q-bio.BM↗
arXiv2026

Online KL-Regularized Reinforcement Learning with Function Approximation under Misspecification

We study KL-regularized contextual bandits and episodic reinforcement learning (RL) under general function approximation with model misspecification. Existing guarantees rely on realizability and therefore do not extend to misspecified models, where classical regret bounds may fail. This work introduces KL misspecification formulations for contextual bandits and episodic RL and analyzes regression-based algorithms with Gibbs policy updates. High-probability KL-regret guarantees with explicit misspecification terms are established, recovering the standard realizable KL-regularized setting as a special case.

cs.LG↗
arXiv2026

A Unified Framework for Formalizing Matrix Decomposition Proofs

Existence proofs for many matrix decompositions share a recursive routine: a local transformation prepares the matrix, a slice is selected, a recursive solution is obtained, and the result is lifted and transported back. Formalizing this routine uniformly in dependent type theory is difficult because recursive subproblems may change index types, and reconstruction must preserve structural predicates across block embeddings and reindexings. We develop a Lean~4 framework that separates decomposition schemas, transformations, reduction strategies, measures, lifting, transport, and subtype induction. The framework uses general index types, packages square and rectangular matrices in universe types, and provides a decomposition driver that assembles strategy data into subtype-induction instances. It has been instantiated across PLU, LU, LDL/Cholesky, QR variants, Gauss rank normal form, Hessenberg reductions, Schur variants, normal spectral decomposition, SVD, bidiagonalization, tridiagonalization, UTV, Smith normal form, rational canonical form, and Jordan-type forms at varying levels of statement strength. Across these instances, repeated decomposition proofs are best treated not as separate tasks but as instances of a more general inductive statement whose interface records a certified proof path compatible with the chosen decomposition statement.

math.NA↗
arXiv2026

Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries. We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines, which encourages monolithic or ad hoc proof scripts rather than library-quality artifacts. Existing approaches to proof-quality improvement often rely on explicit, computable optimization objectives. In practice, however, the most tractable and experimentally validated objectives are largely length-based, while higher-level qualities such as readability, modularity, maintainability, and reusability are difficult to reduce to reliable automatic metrics. Instead of optimizing proof improvement against a single proxy metric, we take a process-guided approach inspired by human proof-refactoring workflows. We propose an agentic framework $\textbf{Proof-Refactor}$ that decomposes proof refactoring into four phases: extracting candidate proof fragments, designing helper declarations, formally proving the extracted and designed components, and repairing the original proof using the verified components. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves rubric-based refactoring scores over a strong Claude Code refactoring baseline, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve proof structure without treating proof length as the primary objective.

cs.AI↗
arXiv2026

Automated Conjecture Resolution with Formal Verification

Recent advances in large language models have significantly improved their ability to perform mathematical reasoning, extending from elementary problem solving to increasingly capable performance on research-level problems. However, reliably solving and verifying such problems remains challenging due to the inherent ambiguity of natural language reasoning. In this paper, we propose an automated framework that integrates natural language reasoning with formal verification to tackle research-level mathematical problems. Our framework consists of two components: an informal reasoning agent, Rethlas, and a formal verification agent, Archon. Rethlas combines reasoning primitives with our theorem search engine, Matlas, to explore solution strategies and construct candidate proofs. Archon, equipped with LeanSearch, translates informal arguments into formalized Lean 4 projects through task decomposition, iterative refinement, and automated proof synthesis, ensuring machine-checkable correctness. Using this framework, we resolve an open problem in commutative algebra and formally verify the resulting proof in Lean 4 with essentially no human involvement. Additional case studies illustrate the capabilities of Rethlas in informal mathematical reasoning and discovery, as well as the ability of Archon to formalize research-level proofs in Lean 4. Our experiments demonstrate that strong theorem retrieval tools enable the discovery and application of cross-domain mathematical techniques, while the formal agent can autonomously fill nontrivial gaps in informal arguments. More broadly, our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, reduce human effort, and support human-AI collaborative mathematical research.

cs.LG↗
arXiv2026

VCWorld: A Biological World Model for Virtual Cell Simulation

Virtual cell modeling aims to predict cellular responses to perturbations. Existing virtual cell models rely heavily on large-scale single-cell datasets, learning explicit mappings between gene expression and perturbations. Although recent models attempt to incorporate multi-source biological information, their generalization remains constrained by data quality, coverage, and batch effects. More critically, these models often function as black boxes, offering predictions without interpretability or consistency with biological principles, which undermines their credibility in scientific research. To address these challenges, we present VCWorld, a cell-level white-box simulator that integrates structured biological knowledge with the iterative reasoning capabilities of large language models to instantiate a biological world model. VCWorld operates in a data-efficient manner to reproduce perturbation-induced signaling cascades and generates interpretable, stepwise predictions alongside explicit mechanistic hypotheses. In drug perturbation benchmarks, VCWorld achieves state-of-the-art predictive performance, and the inferred mechanistic pathways are consistent with publicly available biological evidence.

q-bio.CB↗
arXiv2026

M2F: Automated Formalization of Mathematical Literature at Scale

Automated formalization of mathematics enables mechanical verification but remains limited to isolated theorems and short snippets. Scaling to textbooks and research papers is largely unaddressed, as it requires managing cross-file dependencies, resolving imports, and ensuring that entire projects compile end-to-end. We present M2F (Math-to-Formal), the first agentic framework for end-to-end, project-scale autoformalization in Lean. The framework operates in two stages. The statement compilation stage splits the document into atomic blocks, orders them via inferred dependencies, and repairs declaration skeletons until the project compiles, allowing placeholders in proofs. The proof repair stage closes these holes under fixed signatures using goal-conditioned local edits. Throughout both stages, M2F keeps the verifier in the loop, committing edits only when toolchain feedback confirms improvement. In approximately three weeks, M2F converts long-form mathematical sources into a project-scale Lean library of 153,853 lines from 479 pages textbooks on real analysis and convex analysis, fully formalized as Lean declarations with accompanying proofs. This represents textbook-scale formalization at a pace that would typically require months or years of expert effort. On FATE-H, we achieve $96\%$ proof success (vs.\ $80\%$ for a strong baseline). Together, these results demonstrate that practical, large-scale automated formalization of mathematical literature is within reach. The full generated Lean code from our runs is available at https://github.com/optsuite/ReasBook.git.

cs.AI↗