arXiv:2603.19464v3 Announce Type: replace
Abstract: Robotic path planning problems are often NP-hard, and practical solutions typically rely on approximation algorithms with provable performance guarantees for general cases. While designing such algorithms is challenging, formally proving their approximation optimality is even more demanding, which requires domain-specific geometric insights and multi-step mathematical reasoning over complex operational constraints. Recent Large Language Models (LLMs) have demonstrated strong performance on mathematical reasoning benchmarks, yet their ability to assist with research-level optimality proofs in robotic path planning remains under-explored. In this work, we introduce the first benchmark for evaluating LLMs on approximation-ratio proofs of robotic path planning algorithms. The benchmark consists of 34 research-grade proof tasks spanning diverse planning problem types and complexity levels, each requiring structured reasoning over algorithm descriptions, problem constraints, and theoretical guarantees. Our evaluation of state-of-the-art proprietary and open-source LLMs reveals that even the strongest models struggle to produce fully valid proofs without external domain knowledge. However, providing LLMs with task-specific in-context lemmas substantially improves reasoning quality, a factor that is more effective than generic chain-of-thought prompting or supplying the ground-truth approximation ratio as posterior knowledge. We further provide fine-grained error analysis to characterize common logical failures and hallucinations, and demonstrate how each error type can be mitigated through targeted context augmentation.
Science Journals
arXiv:2603.22507v2 Announce Type: replace
Abstract: We present an energy-aware collaborative exploration framework for a UAV-UGV team operating in unknown environments, where the UAV's energy constraint is modeled as a maximum flight-time limit. The UAV executes a sequence of energy-bounded exploration tours, while the UGV simultaneously explores on the ground and serves as a mobile charging station. Rendezvous is enforced under a shared time budget so that the vehicles meet at the end of each tour before the UAV reaches its flight-time limit. We construct a sparsely coupled air-ground roadmap using a density-aware layered probabilistic roadmap (PRM) and formulate tour selection over the roadmap as coupled orienteering problems (OPs) to maximize information gain subject to the rendezvous constraint. The resulting tours are constructed over collision-validated roadmap edges. We validate our method through simulation studies, benchmark comparisons, and real-world experiments.
arXiv:2603.26556v2 Announce Type: replace
Abstract: Converting a pretrained Transformer into a more efficient hybrid model through distillation offers a promising approach to reducing inference costs. However, achieving high-quality generation in distilled models requires careful joint design of both the student architecture and the distillation process. Many prior distillation works evaluate downstream multiple-choice benchmarks by ranking candidate answers with log-likelihood rather than requiring autoregressive generation, which can obscure important differences in model quality. For example, on overlapping benchmarks, we show that a 7B distilled model that nearly matches its teacher to within 0.2 pp under log-likelihood scoring falls behind by 20.8 pp when it must generate answers autoregressively.
We investigate this phenomenon with GenDistill, a multi-stage pipeline we designed for distilling a pretrained Transformer into an efficient Hybrid Kimi Delta Attention (Hybrid-KDA) student. Using it as a controlled testbed on Qwen3-0.6B, we systematically ablate six design axes (training objective, loss masking, training duration, dataset selection, parameter freezing, and architecture choice) and evaluate every choice under both log-likelihood and generation-based protocols. We find that log-likelihood-based evaluation consistently underestimates the gap between teacher and student, and can in some cases reverse the ranking of design choices, so conclusions drawn from perplexity-only evaluation may be misleading. Among the factors we study, dataset selection, completion-only masking, and freezing attention layers during post-training have the largest impact on generation quality.
Our best distillation recipe, using a Hybrid-KDA model as the student, retains 86-90% of teacher accuracy on knowledge benchmarks while reducing KV cache memory by up to 75% and improving time-to-first-token by 2-4x at 128K-token contexts.
arXiv:2603.27556v2 Announce Type: replace
Abstract: Open-Vocabulary Object Detection (OVOD) has achieved remarkable success in generalizing to novel categories. However, this success often rests on the implicit assumption of domain stationarity. In this work, we revisit the OVOD paradigm and study a key vulnerability: the fragile coupling between visual manifolds and textual embeddings under distribution shifts. We first formulate Domain-Generalized Open-Vocabulary Object Detection (DG-OVOD) as an evaluation protocol for open-vocabulary recognition under visual shifts. Through empirical analysis, we observe that visual shifts can destabilize the latent cross-modal space, causing novel-category visual signals to drift away from their semantic anchors. Motivated by these observations, we propose Progressive Domain-invariant Cross-modal Alignment (PICA). PICA departs from uniform training by introducing a multi-level curriculum based on ambiguity and signal strength. It constructs a quality-adjusted curriculum over pseudo-word prototypes, refined by sample reliability and visual consistency, to encourage more stable cross-domain modality alignment. Our findings suggest that OVOD robustness under domain shifts is closely linked to the stability of the latent cross-modal alignment space. Our work provides a DG-OVOD evaluation protocol and a practical perspective on building more generalizable open-vocabulary systems beyond static laboratory conditions.
arXiv:2603.29139v3 Announce Type: replace
Abstract: Recent advances in large language models (LLMs) have enabled agentic systems to translate natural-language intent into executable scientific visualization (SciVis) tasks. Despite rapid progress, the community lacks a principled and reproducible benchmark for evaluating these emerging SciVis agents in realistic, multi-step analysis settings. We present SciVisAgentBench, a comprehensive and extensible benchmark for evaluating scientific data analysis and visualization agents. Our benchmark is grounded in a structured taxonomy spanning four dimensions: application domain, data type, complexity level, and visualization operation. It currently comprises 108 expert-crafted cases covering diverse SciVis scenarios. To enable reliable assessment, we introduce a multimodal outcome-centric evaluation pipeline that combines LLM-based judging with deterministic evaluators, including image-based metrics, code checkers, rule-based verifiers, and case-specific evaluators. We also conduct a validity study with 12 SciVis experts to examine the agreement between human and LLM judges. Using this framework, we evaluate representative SciVis agents and general-purpose coding agents to establish initial baselines and reveal capability gaps. SciVisAgentBench is designed as a living benchmark to support systematic comparison, diagnose failure modes, and drive progress in agentic SciVis. The benchmark is available at https://scivisagentbench.github.io/.
arXiv:2507.21873v2 Announce Type: replace
Abstract: Graph neural networks (GNNs) excel at predictive tasks on graph-structured data but often lack the ability to incorporate symbolic domain knowledge and perform general reasoning. Relational Bayesian Networks (RBNs), in contrast, enable fully generative probabilistic modeling over graph-like structures and support rich symbolic knowledge and probabilistic inference. This paper presents a neuro-symbolic framework that seamlessly integrates GNNs into RBNs, combining the learning strength of GNNs with the flexible reasoning capabilities of RBNs. We develop two implementations of this integration: one compiles GNNs directly into the native RBN language, while the other maintains the GNN as an external component. Both approaches preserve the semantics and computational properties of GNNs while fully aligning with the RBN modeling paradigm. We also propose a maximum a posteriori (MAP) inference method for these neuro-symbolic models. To demonstrate the framework's versatility, we apply it to two distinct problems. First, we transform a GNN for node classification into a collective classification model that explicitly models homo- and heterophilic label patterns, substantially improving accuracy on both synthetic and real-world datasets. Second, we introduce a multi-objective network optimization problem in environmental planning, where MAP inference and continuous numeric relaxation support a complex decision-making task. Both applications include new publicly available benchmark datasets. This work introduces a powerful and coherent neuro-symbolic approach to graph data, bridging learning and reasoning in ways that enable novel applications and improved performance across diverse tasks.
arXiv:2604.03701v4 Announce Type: replace
Abstract: Video-based numerical reasoning provides a premier arena for testing whether Vision-Language Models (VLMs) truly "understand" real-world dynamics, as accurate numerical deduction necessitates a profound grasp of temporal events, object permanence, and compositional logic beyond superficial pattern matching. However, existing benchmarks are often confined to narrow domains, such as repetitive athletic motions, or treat simple counting merely as a superficial regression task, failing to assess multi-step numerical logic within the inherent complexity of real-world multimedia content. We introduce VidNum-1.4K, a comprehensive VideoQA benchmark comprising 1,379 strictly human-annotated video-question pairs designed to evaluate genuine numerical reasoning across highly diverse environments, encompassing object, action, and event quantification. The VidNum-1.4K is uniquely structured into a three-level hierarchy that evolves from direct visual perception to video-based compositional numerical reasoning, requiring models to perform arithmetic operations, comparisons, and logical deductions grounded in temporal evidence. Our evaluations across a diverse suite of state-of-the-art VLMs reveal a striking reasoning gap: while the Gemini-3.1-pro barely reaches a 60% accuracy threshold, representative open-source families struggle heavily in the 25%--45% range. These findings demonstrate that current VLMs still lack a stable "internal world model", positioning VidNum-1.4K as a demanding diagnostic testbed for the next generation of numerical video intelligence.
arXiv:2604.03873v4 Announce Type: replace
Abstract: Black-box knowledge distillation for large language models presents a strict trade-off. Simple off-policy methods (e.g., sequence-level knowledge distillation) struggle to correct the student's inherent errors. Fully on-policy methods (e.g., Generative Adversarial Distillation) solve this via adversarial training but introduce well-known training instability and crippling computational overhead. To address this dilemma, we propose SODA (Semi On-policy Distillation with Alignment), a highly efficient alternative motivated by the inherent capability gap between frontier teachers and much smaller base models. Because a compact student model's natural, zero-shot responses are almost strictly inferior to the powerful teacher's targets, we can construct a highly effective contrastive signal simply by pairing the teacher's optimal response with a one-time static snapshot of the student's outputs. This demonstrates that exposing the small student to its own static inferior behaviors is sufficient for high-quality distribution alignment, eliminating the need for costly dynamic rollouts and fragile adversarial balancing. Extensive evaluations across four compact Qwen2.5 and Llama-3 models validate this semi on-policy paradigm. SODA matches or outperforms the state-of-the-art methods on 15 out of 16 benchmark results. More importantly, it achieves this superior distillation quality while training 10 times faster, consuming 27% less peak GPU memory, and completely eliminating adversarial instability.
arXiv:2604.05782v3 Announce Type: replace
Abstract: Large language models (LLMs) have rapidly evolved from general-purpose systems to multimodal models capable of processing text, images, and audio. As both general-purpose LLMs (GLLMs) and multimodal LLMs (MLLMs) gain widespread adoption, understanding user perceptions in real-world settings becomes increasingly important. However, existing studies often rely on surveys or platform-specific data (e.g., Reddit or GitHub issues), which either constrain user feedback through predefined questions or overemphasize failure-driven, debugging-oriented discussions, thus failing to capture diverse, experience-driven, and cross-model user perspectives in practice. To address this issue, we conduct an empirical study of user discussions on Hugging Face, a major model hub with diverse models and active communities. We collect and manually annotate 662 discussion threads from 38 representative models (21 GLLMs and 17 MLLMs), and develop a three-level taxonomy to systematically characterize user concerns. Our analysis reveals that LLM access barriers, generation quality, and deployment and invocation complexity are the most prominent concerns, alongside issues such as documentation limitations and resource constraints. Based on these findings, we derive actionable implications for improving LLM ecosystem.
arXiv:2604.06381v2 Announce Type: replace
Abstract: This paper examines artificial intelligence (AI) companionship as a site where intimate relations are simultaneously produced, extracted from, and governed through datafied systems. Drawing on critical data studies and platform studies, we challenge prevailing narratives that locate harm in user psychology rather than platform architecture. Through in-depth interviews with 20 individuals who have AI companions, we address three questions: what harms do users identify, how do they make sense of those harms, and what do their accounts reveal about the perceived distribution of responsibility among users, platforms, and regulators? Participants identified design-based harms, including unsolicited content generation and safety mechanisms that stigmatized the users they intended to protect, alongside use-based harms centered on emotional dependency they could recognize but not resolve. Users deployed individualized sensemaking strategies, including self-regulation, stigma navigation, and privacy rationalization, bearing the full burden of harm mitigation without platform support. On governance, participants described an accountability vacuum in which platforms deflected blame while users articulated conditional preferences that rejected both prohibition and deregulation. The findings extend responsibilization theory by demonstrating how platform-produced vulnerability becomes self-sustaining through the interpretive labor of users who lack structural alternatives.
arXiv:2604.06419v2 Announce Type: replace
Abstract: Drawing on 20 qualitative interviews with users of AI companion platforms and general-purpose chatbots, this study examines what users seek from AI companionship and how gratifications develop through sustained interaction. Through abductive qualitative content analysis, we find that familiar Uses and Gratifications categories, including emotional release, self-expression, social presence, and identity affirmation, are generated through interpersonalized affordances: availability, memory, personalization, and responsiveness interpreted as relational qualities. The study extends the Uses and Gratifications framework by showing that AI companionship gratifications are relationally produced and recursively reorganized as users' needs and expectations change over time.
arXiv:2604.10024v2 Announce Type: replace
Abstract: Long video summarization presents significant challenges for multimodal large language models (MLLMs), particularly in maintaining temporal fidelity over extended durations and producing summaries that are both semantically and temporally grounded. We introduce LVSum, a human-annotated benchmark for evaluating long-form video summarization with fine-grained temporal alignment. LVSum comprises 72 diverse videos spanning 13 domains with an average duration of 16 minutes, each annotated with up to 10 human-generated summaries containing temporal references. We conduct a comprehensive evaluation of leading proprietary and open-source MLLMs using newly introduced LLM-based metrics for content relevance and modality coherence, alongside standard automatic metrics. Our experiments reveal three key findings: (1) transcripts contribute substantially more to summarization quality than visual frames alone, (2) a significant performance gap persists between model-generated and human-written summaries, and (3) current MLLMs exhibit systematic weaknesses in temporal grounding, instruction adherence, and cross-modal coherence. We release the dataset and code.
arXiv:2604.12431v2 Announce Type: replace
Abstract: Organisations increasingly outsource privacy-sensitive data transformations to cloud providers, yet no practical mechanism lets the data owner verify that the contracted algorithm was faithfully executed. VeriX-Anon is a multi-layered verification framework for outsourced Target-Driven k-anonymization combining three orthogonal mechanisms: deterministic verification via Merkle-style hashing of an Authenticated Decision Tree, probabilistic verification via Boundary Sentinels and exact-duplicate Twins with cryptographic identifiers, and utility-based verification via Explainable AI fingerprinting that compares SHAP value distributions before and after anonymization using the Wasserstein distance. Across seven cross-domain datasets and four cloud profiles (28 scenarios), against Lazy (drops records), Dumb (fake hash), and Approximate (valid hash) adversaries, VeriX-Anon detects 25 of 28 deviations under a fixed threshold and 27 of 28 once the threshold is calibrated per dataset, with no false alarms. No single layer achieved this alone. The XAI layer was the only mechanism that caught the Approximate adversary, succeeding on six of seven datasets and missing only a high-dimensional case where honest generalization shifts SHAP as much as the attack. Target-Driven anonymization preserved significantly more utility than blind splitting, with mean F1 gaps of +0.058 to +0.362 and Wilcoxon p <= 0.001 on six of seven datasets. Client-side verification completes under one second at one million rows. The threat model covers three empirically evaluated profiles and one theoretical Informed Attacker unable to defeat the cryptographic salt. Sentinel evasion probability ranges from near-zero to 0.82 for the most imbalanced data, which the twin layer offsets in every scenario.
arXiv:2604.13780v2 Announce Type: replace
Abstract: Soft Q-learning has emerged as a versatile model-free method for entropy-regularised reinforcement learning, optimising for returns augmented with a penalty on the divergence from a reference policy. Despite its success, the multi-step extensions of soft Q-learning remain relatively unexplored and limited to on-policy action sampling under the Boltzmann policy. In this brief research note, we first present a formal $n$-step formulation for soft Q-learning and then extend this framework to the fully off-policy case by introducing a novel Soft Tree Backup operator. Finally, we unify these developments into Soft $Q(\lambda)$, an elegant online, off-policy, eligibility trace framework that allows for efficient credit assignment under arbitrary behaviour policies. Our derivations propose a model-free method for learning entropy-regularised value functions that can be utilised in future empirical experiments.
arXiv:2604.15010v2 Announce Type: replace
Abstract: When do transformers commit to a decision, and what prevents them from correcting it? We introduce prolepsis: a transformer commits early, task-specific attention heads sustain the commitment, and no layer corrects it. Replicating Lindsey et al.'s (2025) planning-site finding on open models (Gemma 2 2B, Llama 3.2 1B), we ask five questions. (Q1) Planning is invisible to six residual-stream methods; among those tested, only CLT-based steering succeeds. (Q2) The single-site spike replicates in shape, at the final prompt token (Anthropic's site is the newline; see the Note added). (Q3) Specific attention heads route the decision to the output, filling a gap flagged as invisible to attribution graphs. (Q4) The evidence is consistent with search within at most 16 layers and commitment beyond, a two-model hypothesis. (Q5) Factual recall shows the same motif at a different network depth, with zero overlap between recurring planning heads and the factual top-10. Prolepsis recurs across tasks in the decoder-only models tested: the template is shared, the routing substrates differ. All experiments run on a single consumer GPU (16 GB VRAM).
arXiv:2604.16370v3 Announce Type: replace
Abstract: Decoding natural language from non-invasive electroencephalography (EEG) remains constrained by low signal-to-noise ratio and limited information bandwidth. This raises a central question: can sentence-level language be reliably recovered from such signals? Under realistic information constraints, this direct-recovery assumption may be too strong. We introduce a semantic compression hypothesis: non-invasive EEG may preserve recoverable semantic anchors rather than the full lexical--syntactic form of a sentence. From this perspective, direct sentence reconstruction is overly fine-grained relative to the recoverable information scale of EEG. To address this mismatch, we propose Brain-CLIPLM, a two-stage framework that decomposes EEG-to-text decoding into semantic-anchor recovery and anchor-guided sentence reconstruction. Stage 1 uses contrastive learning to align word-level EEG evidence with a fixed keyword vocabulary and recover ordered semantic anchors. Stage 2 uses a retrieval-grounded large language model with chain-of-thought reasoning prompts to reconstruct sentence meaning from these anchors, following a granularity matching principle that aligns decoding complexity with the recoverable neural information scale. On the combined Zurich Cognitive Language Processing (ZuCo) benchmark, Brain-CLIPLM achieves 67.6\% Top-5 and 85.0\% Top-25 sentence retrieval accuracy, with the strongest performance at intermediate anchor granularity. Control analyses show that EEG-derived anchors carry sentence-specific information beyond language-model priors. Within the constrained ZuCo sentence pool and fixed keyword-vocabulary settings, these findings suggest that EEG-to-text decoding is better framed as recovering compressed semantic content before anchor-guided sentence reconstruction.
arXiv:2604.19248v2 Announce Type: replace
Abstract: This paper presents a robust path following control method for vehicles that explicitly incorporates steering torque dynamics into the control model. Unlike conventional approaches that treat the steering angle as a direct control input, this study models the steering angle as a state variable driven by a torque-proportional steering command against a speed- and angle-dependent resistance term. Since the resistance coefficient depends on road surface properties and is difficult to determine precisely, it is treated as an uncertain parameter. To compensate for the resulting model error, a Model Error Compensator (MEC) is employed as an add-on compensator that feeds back the discrepancy between the actual plant and a nominal model running in parallel, without requiring an explicit plant inverse or a specific canonical form. The zero dynamics arising from the path following formulation are formally analyzed, and it is shown that they are stable for any positive rear cornering power. Numerical simulations under systematic parameter mismatch conditions (C/C_M=0.5 to 2.0) demonstrate that the proposed method reduces the maximum following error by more than 90\% compared to the conventional method without MEC throughout the tested mismatch range, and maintains practical tracking performance within a mismatch range of 0.75 <= C/C_M <= 1.25. These results confirm that MEC effectively suppresses the influence of steering torque uncertainty, significantly enhancing path following robustness.
arXiv:2604.19834v2 Announce Type: replace
Abstract: Functional fitness movements are widely used in training, competition, and health-oriented exercise programs, yet consistently enforcing repetition (rep) standards remains challenging due to subjective human judgment, time constraints, and evolving rules. Existing AI-based approaches mainly rely on learned scoring or reference-based comparisons and lack explicit rule-based approaches, limiting transparency and deterministic rep-level validation. To address these limitations, we propose KD-Judge, a novel knowledge-driven automated judging framework for functional fitness movements. It converts unstructured rulebook standards into executable, machine-readable representations using an LLM-based retrieval-augmented generation and chain-of-thought rule-structuring pipeline. The structured rules are then incorporated by a deterministic rule-based judging system with pose-guided kinematic reasoning to assess rep validity and temporal boundaries. To improve efficiency on edge devices, including a high-performance desktop and the resource-constrained Jetson AGX Xavier, we introduce a dual strategy caching mechanism that can be selectively applied to reduce redundant and unnecessary computation. Experiments demonstrate reliable rule-structuring performance and accurate rep-level assessment, with judgment evaluation conducted on the CFRep dataset, achieving faster-than-real-time execution (real-time factor (RTF) < 1). When the proposed caching strategy is enabled, the system achieves up to 3.36x and 15.91x speedups on resource-constrained edge device compared to the non-caching baseline for pre-recorded and live-streaming scenarios, respectively. These results show that KD-Judge enables transparent, efficient, and scalable rule-grounded rep-level analysis that can complement human judging in practice.
arXiv:2604.21173v3 Announce Type: replace
Abstract: PsSource is an installable Geant4 extension for configurable positronium-aware terminal positron annihilation. Geant4 transports the positron normally, after which PsSource replaces only terminal at-rest annihilation, preserves the terminal position and global time, resolves a fixed or host-defined environment, samples the annihilation class and delay, and returns ordinary two- or three-photon secondaries. Supported outcomes are direct two-photon, para-positronium two-photon, ortho-positronium two-photon, and ortho-positronium three-photon annihilation. Fixed and exponential delays and approximate phase-space, Geant4 Ore-Powell, and polarized Geant4 Ore-Powell backends are available. Regression tests verified terminal-state preservation, timing decomposition, all four classes, photon multiplicity and parentage, equivalent environment pathways, and unchanged photon physics when PsSource-specific truth recording was disabled. The Ore-Powell backend was evaluated using 100,000 three-photon events. Comparison with an analytic joint-energy distribution yielded chi-square = 1236.91 for 1274 degrees of freedom, a standardized score of -0.735, and a maximum marginal empirical CDF difference of 0.00208. Ordered photon-energy spectra agreed with native Geant4 and GATE references, with no pairwise empirical CDF difference greater than 0.00452. Photon directions and event-plane normals were isotropic with no detectable Cartesian-axis bias. The polarized backend satisfied normalization and transversality to within 1.5 x 10^-12 and preserved the ordinary Ore-Powell energy spectrum. PsSource provides a validated integration layer for positronium-aware terminal annihilation in Geant4.
arXiv:2604.21466v2 Announce Type: replace
Abstract: Theory was formulated for scattering by a coated chiral sphere of a plane wave of arbitrary polarization state with amplitude modulated by a Gaussian pulse. The spherical core and the concentric shell of the sphere were composed of two different homogeneous materials, both isotropic chiral. Calculations of energy efficiencies for extinction, total scattering, and absorption were carried out for the shell material with experimentally determined constitutive parameters, the core being vacuous. All three energy efficiencies depend on the relative thickness of the shell and the circular polarization state of the carrier plane wave.
arXiv:2604.23226v2 Announce Type: replace
Abstract: Temporal graphs are graphs whose edges are present only at certain points in time. Reachability in these graphs is defined via temporal paths, in which edges are traversed in chronological order. A temporal graph is temporally connected (or TC) if every ordered pair of vertices is connected by a temporal path. When the graph itself is not TC, a natural question is whether it admits a TC subgraph (a.k.a.~closed temporal component) of a given size $k$. This question was one of the earliest and most studied in the field, shown to be NP-hard by Bhadra and Ferreira in 2003.
We strengthen this result dramatically, showing that deciding if a temporal graph admits a TC subgraph \emph{of any size} (beyond the trivial case of a single vertex in the directed and a single edge in the undirected case) is already NP-hard. Our result holds for all standard temporal graph settings, answering a series of open questions in the field and strengthening several existing results. This sharply separates closed components from open ones (where temporal paths can travel outside the component), for which the analogous problem is trivially solvable in polynomial time.
More precisely, our reductions imply that the size of the largest TC subgraph cannot even be approximated within a factor of~$(1-\epsilon)n$ in directed graphs, and within a factor of~$(1-\epsilon)\frac{n}{2}$ in undirected graphs.
They also complete the complexity landscape for TC subgraphs of size exactly $k$ when parameterized by $k$ (answering the missing ``non-strict'' case). Our results also have structural implications. In particular, they imply that there exist arbitrarily large TC graphs without nontrivial TC subgraphs, and that there exist TC graphs of arbitrary girth, both facts being of independent interest.
arXiv:2605.02790v4 Announce Type: replace
Abstract: Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the "cyber" and "physical" behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model. In this paper we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort. First, we describe how Vehicle's standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle's functional interface.
arXiv:2605.04539v4 Announce Type: replace
Abstract: Direct Preference Optimization (DPO), the efficient alternative to PPO-based RLHF, falls short on knowledge-intensive generation: standard preference signals from human annotators or LLM judges exhibit a systematic verbosity bias that rewards fluency over logical correctness. This blindspot leaves a logical alignment gap -- SFT models reach NLI entailment of only 0.05-0.22 despite producing fluent text. We propose RLearner-LLM with Hybrid-DPO: an automated preference pipeline that fuses a DeBERTa-v3 NLI signal with a verifier LLM score, removing human annotation while overcoming the "alignment tax" of single-signal optimization. Evaluated across five academic domains (Biology, Medicine, Law) with three base architectures (LLaMA-2-13B, Qwen3-8B, Gemma 4 E4B-it), RLearner-LLM yields up to 6x NLI improvement over SFT, with NLI gains in 11 of 15 cells and consistent answer-coverage gains. On Gemma 4 E4B-it (4.5B effective params), Hybrid-DPO lifts NLI in four of five domains (+11.9% to +2.4x) with faster inference across all five, scaling down to compact base models without losing the alignment-tax mitigation. Our Qwen3-8B RLearner-LLM wins 95% of pairwise comparisons against its own SFT baseline; GPT-4o-mini in turn wins 95% against our concise output -- alongside the 69% win the same judge gives a verbose SFT over our DPO model, this replicates verbosity bias on a frontier comparator and motivates logic-aware metrics (NLI, ACR) over LLM-as-a-judge for knowledge-intensive generation.
arXiv:2605.04893v3 Announce Type: replace
Abstract: Every attention head defines a degree-normalized transport operator, and a growing family of diagnostics reads model behavior (hallucination among them) from its spectrum. We ask what such diagnostics can and cannot infer. The operator splits orthogonally into a symmetric part governing transport \emph{capacity} and an antisymmetric part encoding \emph{orientation}. We prove an identifiability limit: every transpose-invariant spectral diagnostic is \emph{orientation-blind} (unable to distinguish an operator from its transpose, hence blind to the orientation of information flow), with a transpose-stability bound limiting any Lipschitz diagnostic's transpose sensitivity by the asymmetry coefficient $G$. This bounds what spectral diagnostics of the attention operator can resolve (e.g.\ LapEigvals and the attention-spectral branch of LLM-Check). On the surviving axis, a closed-form bipartite-Cheeger landscape shows uniform causal attention obeys an $n$-independent \emph{temporal-cut} floor $\phi \ge 1/5$ while window attention pierces it as $O(w/n)$; the floor is an idealized benchmark, not an empirical attractor, and the fraction of real heads falling below it is itself an empirically stable architectural descriptor. The two-axis diagnostic ($\phi$ for capacity, $G$ for asymmetry magnitude) yields a falsifiable polarity prediction, borne out \emph{in sign} under length-controlled, forced-scoring evaluation across decoder-only, encoder-only, and encoder--decoder models (capacity-axis signal 0.62--0.84 LC-AUROC): polarity reverses between HaluEval and MedHallu, directionally as predicted though asymmetric in strength, with decision polarity calibrated per regime.
arXiv:2605.05441v3 Announce Type: replace
Abstract: Advanced radiotherapy approaches such as FLASH irradiation and spatially fractionated radiotherapy (SFRT) show potential to improve the therapeutic ratio, yet their biological mechanisms and optimal delivery parameters remain uncertain. Progress requires accessible proton research platforms with flexible temporal and spatial dose delivery. We report on the adaptation of the Beam Transfer Line (BTL) of the Bern Medical Cyclotron (BMC) for radiobiology research with FLASH and proton minibeam capabilities. The BMC is optimized for the production of radionuclides for medical imaging, and is able to extract currents up to 150 $ \mathrm{\mu A}$. The 18 MeV proton beam was passively shaped using collimators, scattering foils, and extended drift space to generate irradiation fields. A dosimetric framework was implemented using an in-beam ionization chamber and radiochromic film with LET-dependent corrections. Beam uniformity and SFRT profiles with various grid spacings were evaluated at realistic target distances. The developed beamline enables stable delivery under controlled conditions in both conventional and FLASH regimes, spanning dose rates from 0.01 to 100 Gy/s. Dose uniformity within a 20 mm radius was below 8\%. Film measurements confirmed the need for LET-dependent corrections and indicated that quantitative dosimetry in in-vitro setups is achievable with appropriate LET corrections. The low proton energy (15.54(12) MeV extracted into air, 8.14(28) MeV delivered to cells in flask) facilitates compact SFRT implementation with well-resolved minibeams. The adapted BMC provides a flexible and accessible platform for systematic pre-clinical proton radiobiology studies under varied dose-rate and spatial delivery conditions. This supports optimization of emerging modalities such as proton FLASH and SFRT and helps bridge accelerator technology and radiobiology.