OpenRaiser/Intern-Atlas huggingface dataset:
CUTHERMO: Understanding GPU Memory Inefficiencies with Heat Map Profiling
Venue: arXiv cs.DC 2025
Year: 2025

GPUs have become indispensable in high-performance computing, machine learning, and many other domains. Efficiently utilizing the memory subsystem on GPUs is critical for maximizing computing power through massive parallelism. Analyzing memory access patterns has proven to be an effective method for understanding memory bottlenecks in applications. However, comprehensive runtime and fine-grained memory profiling support is lacking on GPU architectures. In this work, we introduce cuThermo, a lightweight and practical profiling tool for GPU memory analysis. It operates on GPU binaries without requiring any modifications to hardware, operating system, or application source code. Given a CUDA application, cuThermo identifies memory inefficiencies at runtime via a heat map based on distinct visited warp counts to represent word-sector-level data sharing and provides optimization guidance in performance tuning iterations. Through our experiments on six applications, we identified five memory access patterns that are portable across different GPU architectures. By evaluating optimization on two GPUs, cuThermo achieves up to $721.79\%$ performance improvement.
Bridging Cloud Convenience and Protocol Transparency: A Hybrid Architecture for Ethereum Node Operations on Amazon Managed Blockchain
Venue: arXiv cs.CR 2025
Year: 2025

As blockchain technologies are increasingly adopted in enterprise and research domains, the need for secure, scalable, and performance-transparent node infrastructure has become critical. While self-hosted Ethereum nodes offer operational control, they often lack elasticity and require complex maintenance. This paper presents a hybrid, service-oriented architecture for deploying and monitoring Ethereum full nodes using Amazon Managed Blockchain (AMB), integrated with EC2-based observability, IAM-enforced security policies, and reproducible automation via the AWS Cloud Development Kit. Our architecture supports end-to-end observability through custom EC2 scripts leveraging Web3.py and JSON-RPC, collecting over 1,000 real-time data points-including gas utilization, transaction inclusion latency, and mempool dynamics. These metrics are visualized and monitored through AWS CloudWatch, enabling service-level performance tracking and anomaly detection. This cloud-native framework restores low-level observability lost in managed environments while maintaining the operational simplicity of managed services. By bridging the simplicity of AMB with the transparency required for protocol research and enterprise monitoring, this work delivers one of the first reproducible, performance-instrumented Ethereum deployments on AMB. The proposed hybrid architecture enables secure, observable, and reproducible Ethereum node operations in cloud environments, suitable for both research and production use.
Initial Steps in Integrating Large Reasoning and Action Models for Service Composition
Venue: arXiv cs.AI 2025
Year: 2025

Service composition remains a central challenge in building adaptive and intelligent software systems, often constrained by limited reasoning capabilities or brittle execution mechanisms. This paper explores the integration of two emerging paradigms enabled by large language models: Large Reasoning Models (LRMs) and Large Action Models (LAMs). We argue that LRMs address the challenges of semantic reasoning and ecosystem complexity while LAMs excel in dynamic action execution and system interoperability. However, each paradigm has complementary limitations - LRMs lack grounded action capabilities, and LAMs often struggle with deep reasoning. We propose an integrated LRM-LAM architectural framework as a promising direction for advancing automated service composition. Such a system can reason about service requirements and constraints while dynamically executing workflows, thus bridging the gap between intention and execution. This integration has the potential to transform service composition into a fully automated, user-friendly process driven by high-level natural language intent.
When Better Eyes Lead to Blindness: A Diagnostic Study of the Information Bottleneck in CNN-LSTM Image Captioning Models
Venue: arXiv cs.CV 2025
Year: 2025

Image captioning, situated at the intersection of computer vision and natural language processing, requires a sophisticated understanding of both visual scenes and linguistic structure. While modern approaches are dominated by large-scale Transformer architectures, this paper documents a systematic, iterative development of foundational image captioning models, progressing from a simple CNN-LSTM encoder-decoder to a competitive attention-based system. This paper presents a series of five models, beginning with Genesis and concluding with Nexus, an advanced model featuring an EfficientNetV2B3 backbone and a dynamic attention mechanism. The experiments chart the impact of architectural enhancements and demonstrate a key finding within the classic CNN-LSTM paradigm: merely upgrading the visual backbone without a corresponding attention mechanism can degrade performance, as the single-vector bottleneck cannot transmit the richer visual detail. This insight validates the architectural shift to attention. Trained on the MS COCO 2017 dataset, the final model, Nexus, achieves a BLEU-4 score of 31.4, surpassing several foundational benchmarks and validating the iterative design process. This work provides a clear, replicable blueprint for understanding the core architectural principles that underpin modern vision-language tasks.
Even Faster Simulations with Flow Matching: A Study of Zero Degree Calorimeter Responses
Venue: arXiv cs.LG 2025
Year: 2025

Recent advances in generative neural networks, particularly flow matching (FM), have enabled the generation of high-fidelity samples while significantly reducing computational costs. A promising application of these models is accelerating simulations in high-energy physics (HEP), helping research institutions meet their increasing computational demands. In this work, we leverage FM to develop surrogate models for fast simulations of zero degree calorimeters in the ALICE experiment. We present an effective training strategy that enables the training of fast generative models with an exceptionally low number of parameters. This approach achieves state-of-the-art simulation fidelity for both neutron (ZN) and proton (ZP) detectors, while offering substantial reductions in computational costs compared to existing methods. Our FM model achieves a Wasserstein distance of 1.27 for the ZN simulation with an inference time of 0.46 ms per sample, compared to the current best of 1.20 with an inference time of approximately 109 ms. The latent FM model further improves the inference speed, reducing the sampling time to 0.026 ms per sample, with a minimal trade-off in accuracy. Similarly, our approach achieves a Wasserstein distance of 1.30 for the ZP simulation, outperforming the current best of 2.08. The source code is available at https://github.com/m-wojnar/faster_zdc.
Improving the State of the Art for Training Human-AI Teams: Technical Report #5 -- Individual Differences and Team Qualities to Measure in a Human-AI Teaming Testbed
Venue: arXiv cs.HC 2025
Year: 2025

Sonalysts, Inc. (Sonalysts) is working on an initiative to expand our expertise in teaming to include Human-Artificial Intelligence (AI) teams. The first step of this process is to develop a Synthetic Task Environment (STE) to support our original research. Prior knowledge elicitation efforts within the Human-AI teaming research stakeholder community revealed a desire to support data collection using pre- and post-performance surveys. In this technical report, we review a number of constructs that capture meaningful individual differences and teaming qualities. Additionally, we explore methods of measuring those constructs within the STE.
Perspective from a Higher Dimension: Can 3D Geometric Priors Help Visual Floorplan Localization?
Venue: arXiv cs.CV 2025
Year: 2025

Since a building's floorplans are easily accessible, consistent over time, and inherently robust to changes in visual appearance, self-localization within the floorplan has attracted researchers' interest. However, since floorplans are minimalist representations of a building's structure, modal and geometric differences between visual perceptions and floorplans pose challenges to this task. While existing methods cleverly utilize 2D geometric features and pose filters to achieve promising performance, they fail to address the localization errors caused by frequent visual changes and view occlusions due to variously shaped 3D objects. To tackle these issues, this paper views the 2D Floorplan Localization (FLoc) problem from a higher dimension by injecting 3D geometric priors into the visual FLoc algorithm. For the 3D geometric prior modeling, we first model geometrically aware view invariance using multi-view constraints, i.e., leveraging imaging geometric principles to provide matching constraints between multiple images that see the same points. Then, we further model the view-scene aligned geometric priors, enhancing the cross-modal geometry-color correspondences by associating the scene's surface reconstruction with the RGB frames of the sequence. Both 3D priors are modeled through self-supervised contrastive learning, thus no additional geometric or semantic annotations are required. These 3D priors summarized in extensive realistic scenes bridge the modal gap while improving localization success without increasing the computational burden on the FLoc algorithm. Sufficient comparative studies demonstrate that our method significantly outperforms state-of-the-art methods and substantially boosts the FLoc accuracy. All data and code will be released after the anonymous review.
A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
Venue: arXiv cs.PL 2025
Year: 2025

Neural Theorem Proving (NTP) employs LLMs to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using natural languages, the transition to mechanized formal theorem proving presents persistent challenges. Mechanized proof languages often contain many syntactic constructs and diverse, specialized proof tactics, which facilitate expert use but have no direct counterpart in informal mathematical proofs. These prover-specific idioms represent an additional burden for LLM-based NTPs that might be otherwise successful in generating informal proofs. Seeking to bridge this gap between formal proof construction and informal reasoning, in order to better facilitate NTP, this work approaches these challenges from a language design perspective. We look at common reasoning patterns in informal proofs and in existing mechanized proofs, and design Minilang -- a minimalist proof language that captures these reasoning patterns. In contrast to proof languages (informal and formal) that often feature a large collection of operations with unclear semantic boundaries, Minilang is deliberately kept minimalist -- its core design comprises only 10 operations, each with clear semantic distinctions. We further develop a rule-based translator from Isabelle's language (Isar) to Minilang, translating ~340K existing proofs with an ~85% success rate. Using this translated corpus, we finetune two LLMs to compare machine learning performance on Minilang versus the original Isar. Experiments show Minilang benefits the two LLMs by improving the pass@1 success rate on the PISA benchmark by up to 20/29 percentage points in comparison to the Isar-based LLMs w/wo Sledgehammer. The pass@1 rate reaches 69.1%, exceeding the prior work Baldur's pass@64 (65.7%); the pass@8 rate reaches 79.2%, exceeding the SOTA on PISA (71.0%) achieved by Magnushammer.
Large language models provide unsafe answers to patient-posed medical questions
Venue: arXiv cs.CL 2025
Year: 2025

Millions of patients are already using large language model (LLM) chatbots for medical advice on a regular basis, raising patient safety concerns. This physician-led red-teaming study compares the safety of four publicly available chatbots--Claude by Anthropic, Gemini by Google, GPT-4o by OpenAI, and Llama3-70B by Meta--on a new dataset, HealthAdvice, using an evaluation framework that enables quantitative and qualitative analysis. In total, 888 chatbot responses are evaluated for 222 patient-posed advice-seeking medical questions on primary care topics spanning internal medicine, women's health, and pediatrics. We find statistically significant differences between chatbots. The rate of problematic responses varies from 21.6 percent (Claude) to 43.2 percent (Llama), with unsafe responses varying from 5 percent (Claude) to 13 percent (GPT-4o, Llama). Qualitative results reveal chatbot responses with the potential to lead to serious patient harm. This study suggests that millions of patients could be receiving unsafe medical advice from publicly available chatbots, and further work is needed to improve the clinical safety of these powerful tools.
WiSE-OD: Benchmarking Robustness in Infrared Object Detection
Venue: arXiv cs.CV 2025
Year: 2025

Object detection (OD) in infrared (IR) imagery is critical for low-light and nighttime applications. However, the scarcity of large-scale IR datasets forces models to rely on weights pre-trained on RGB images. While fine-tuning on IR improves accuracy, it often compromises robustness under distribution shifts due to the inherent modality gap between RGB and IR. To address this, we introduce LLVIP-C and FLIR-C, two cross-modality out-of-distribution (OOD) benchmarks built by applying corruptions to standard IR datasets. Additionally, to fully leverage the complementary knowledge from RGB and infrared-trained models, we propose WiSE-OD, a weight-space ensembling method with two variants: WiSE-OD$_{ZS}$, which combines RGB zero-shot and IR fine-tuned weights, and WiSE-OD$_{LP}$, which blends zero-shot and linear probing. Evaluated using four RGB-pretrained detectors and two robust baselines on our benchmark and in the real-world out-of-distribution M3FD dataset, our WiSE-OD improves robustness across modalities and to corruption in synthetic and real-world distribution shifts without any additional training or inference costs. Our code is available at: https://github.com/heitorrapela/wiseod.
Geometric Multi-color Message Passing Graph Neural Networks for Blood-brain Barrier Permeability Prediction
Venue: arXiv cs.LG 2025
Year: 2025

Accurate prediction of blood-brain barrier permeability (BBBP) is essential for central nervous system (CNS) drug development. While graph neural networks (GNNs) have advanced molecular property prediction, they often rely on molecular topology and neglect the three-dimensional geometric information crucial for modeling transport mechanisms. This paper introduces the geometric multi-color message-passing graph neural network (GMC-MPNN), a novel framework that enhances standard message-passing architectures by explicitly incorporating atomic-level geometric features and long-range interactions. Our model constructs weighted colored subgraphs based on atom types to capture the spatial relationships and chemical context that govern BBB permeability. We evaluated GMC-MPNN on three benchmark datasets for both classification and regression tasks, using rigorous scaffold-based splitting to ensure a robust assessment of generalization. The results demonstrate that GMC-MPNN consistently outperforms existing state-of-the-art models, achieving superior performance in both classifying compounds as permeable/non-permeable (AUC-ROC of 0.947 and 0.9212) and in regressing continuous permeability values (RMSE of 0.5628, Pearson correlation of 0.6947). An ablation study further quantified the impact of specific atom-pair interactions, revealing that the model's predictive power derives from its ability to learn from both common and rare, but chemically significant, functional motifs. By integrating spatial geometry into the graph representation, GMC-MPNN sets a new performance benchmark and offers a more accurate and generalizable tool for drug discovery pipelines.
Edge-coloring problems with forbidden patterns and planted colors
Venue: arXiv cs.CC 2025
Year: 2025

Edge-coloring problems with forbidden patterns refer to decision problems whose input is a graph $\mathbb G$ and where the goal is to determine whether the edges of $\mathbb G$ can be colored (with a fixed finite set of colors) in a way that in the resulting colored graph $(\mathbb G, ξ)$, none of a fixed set of edge-colored obstructions admits a homomorphism to $(\mathbb G, ξ)$. In the coloring extension setting, some of the edges of $\mathbb G$ are already colored and the goal is to find an extension of this coloring omitting the obstructions. We show that for certain sets of obstructions, there is a polynomial-time equivalence between the coloring problem and the extension problem. We also show that for natural sets of obstructions, such coloring problems exhibit a P vs. NP-complete complexity dichotomy.
On Automating Proofs of Multiplier Adder Trees using the RTL Books
Venue: arXiv cs.LO 2025
Year: 2025

We present an experimental, verified clause processor ctv-cp that fits into the framework used at Arm for formal verification of arithmetic hardware designs. This largely automates the ACL2 proof development effort for integer multiplier modules that exist in designs ranging from floating-point division to matrix multiplication.
A Formalization of the Yul Language and Some Verified Yul Code Transformations
Venue: arXiv cs.LO 2025
Year: 2025

Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations.
An Enumerative Embedding of the Python Type System in ACL2s
Venue: arXiv cs.PL 2025
Year: 2025

Python is a high-level interpreted language that has become an industry standard in a wide variety of applications. In this paper, we take a first step towards using ACL2s to reason about Python code by developing an embedding of a subset of the Python type system in ACL2s. The subset of Python types we support includes many of the most commonly used type annotations as well as user-defined types comprised of supported types. We provide ACL2s definitions of these types, as well as defdata enumerators that are customized to provide code coverage and identify errors in Python programs. Using the ACL2s embedding, we can generate instances of types that can then be used as inputs to fuzz Python programs, which allows us to identify bugs in Python code that are not detected by state-of-the-art Python type checkers. We evaluate our work against four open-source repositories, extracting their type information and generating inputs for fuzzing functions with type signatures that are in the supported subset of Python types. Note that we only use the type signatures of functions to generate inputs and treat the bodies of functions as black boxes. We measure code coverage, which ranges from about 68% to more than 80%, and identify code patterns that hinder coverage such as complex branch conditions and external file system dependencies. We conclude with a discussion of the results and recommendations for future work.
How to Copy-Protect Malleable-Puncturable Cryptographic Functionalities Under Arbitrary Challenge Distributions
Venue: arXiv cs.CR 2025
Year: 2025

A quantum copy-protection scheme (Aaronson, CCC 2009) encodes a functionality into a quantum state such that given this state, no efficient adversary can create two (possibly entangled) quantum states that are both capable of running the functionality. There has been a recent line of works on constructing provably-secure copy-protection schemes for general classes of schemes in the plain model, and most recently the recent work of Çakan and Goyal (IACR Eprint, 2025) showed how to copy-protect all cryptographically puncturable schemes with pseudorandom puncturing points. In this work, we show how to copy-protect even a larger class of schemes. We define a class of cryptographic schemes called malleable-puncturable schemes where the only requirement is that one can create a circuit that is capable of answering inputs at points that are unrelated to the challenge in the security game but does not help the adversary answer inputs related to the challenge. This is a flexible generalization of puncturable schemes, and can capture a wide range of primitives that was not known how to copy-protect prior to our work. Going further, we show that our scheme is secure against arbitrary high min-entropy challenge distributions whereas previous work has only considered schemes that are punctured at pseudorandom points.
Probing Multimodal Fusion in the Brain: The Dominance of Audiovisual Streams in Naturalistic Encoding
Venue: arXiv cs.CV 2025
Year: 2025

Predicting brain activity in response to naturalistic, multimodal stimuli is a key challenge in computational neuroscience. While encoding models are becoming more powerful, their ability to generalize to truly novel contexts remains a critical, often untested, question. In this work, we developed brain encoding models using state-of-the-art visual (X-CLIP) and auditory (Whisper) feature extractors and rigorously evaluated them on both in-distribution (ID) and diverse out-of-distribution (OOD) data. Our results reveal a fundamental trade-off between model complexity and generalization: a higher-capacity attention-based model excelled on ID data, but a simpler linear model was more robust, outperforming a competitive baseline by 18\% on the OOD set. Intriguingly, we found that linguistic features did not improve predictive accuracy, suggesting that for familiar languages, neural encoding may be dominated by the continuous visual and auditory streams over redundant textual information. Spatially, our approach showed marked performance gains in the auditory cortex, underscoring the benefit of high-fidelity speech representations. Collectively, our findings demonstrate that rigorous OOD testing is essential for building robust neuro-AI models and provides nuanced insights into how model architecture, stimulus characteristics, and sensory hierarchies shape the neural encoding of our rich, multimodal world.
Exploring post-neoliberal futures for managing commercial heating and cooling through speculative praxis
Venue: arXiv cs.HC 2025
Year: 2025

What could designing for carbon reduction of heating and cooling in commercial settings look like in the near future? How can we challenge dominant mindsets and paradigms of efficiency and behaviour change? How can we help build worlds through our practice that can become future realities? This paper introduces the fictional consultancy ANCSTRL.LAB to explore opportunities for making space in research projects that can encourage more systems-oriented interventions. We present a design fiction that asks `what if energy management and reduction practice embraced systems thinking?'. Our design fiction explores how future energy consultancies could utilise systems thinking, and (more than) human centred design to re-imagine energy management practice and change systems in ways that are currently unfathomable. We finish by discussing how LIMITS research can utilise design fiction and speculative praxis to help build new material realities where more holistic perspectives, the leveraging of systems change, and the imagining of post-neoliberal futures is the norm.