OpenRaiser/Intern-Atlas huggingface dataset:
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL (Extended Version)
Venue: arXiv cs.PL 2025
Year: 2025

This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP's intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable. To make verification tractable, we develop a number of big-step rules that combine BIL's existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.
MOOSComp: Improving Lightweight Long-Context Compressor via Mitigating Over-Smoothing and Incorporating Outlier Scores
Venue: arXiv cs.CL 2025
Year: 2025

Recent advances in large language models have significantly improved their ability to process long-context input, but practical applications are challenged by increased inference time and resource consumption, particularly in resource-constrained environments. To address these challenges, we propose MOOSComp, a token-classification-based long-context compression method that enhances the performance of a BERT-based compressor by mitigating the over-smoothing problem and incorporating outlier scores. In the training phase, we add an inter-class cosine similarity loss term to penalize excessively similar token representations, thereby improving the token classification accuracy. During the compression phase, we introduce outlier scores to preserve rare but critical tokens that are prone to be discarded in task-agnostic compression. These scores are integrated with the classifier's output, making the compressor more generalizable to various tasks. Superior performance is achieved at various compression ratios on long-context understanding and reasoning benchmarks. Moreover, our method obtains a speedup of 3.3x at a 4x compression ratio on a resource-constrained mobile device.
From Diverse Origins to a DEI Crisis: The Pushback Against Equity, Diversity, and Inclusion in Software Engineering
Venue: arXiv cs.SE 2025
Year: 2025

Background: Diversity, equity, and inclusion are rooted in the very origins of software engineering, shaped by the contributions from many individuals from underrepresented groups to the field. Yet today, DEI efforts in the industry face growing resistance. As companies retreat from visible commitments, and pushback initiatives started only a few years ago. Aims: This study explores how the DEI backlash is unfolding in the software industry by investigating institutional changes, lived experiences, and the strategies used to sustain DEI practices. Method: We conducted an exploratory case study using 59 publicly available Reddit posts authored by self-identified software professionals. Data were analyzed using reflexive thematic analysis. Results: Our findings show that software companies are responding to the DEI backlash in varied ways, including re-structuring programs, scaling back investments, or quietly continuing efforts under new labels. Professionals reported a wide range of emotional responses, from anxiety and frustration to relief and happiness, shaped by identity, role, and organizational culture. Yet, despite the backlash, multiple forms of resistance and adaptation have emerged to protect inclusive practices in software engineering. Conclusions: The DEI backlash is reshaping DEI in software engineering. While public messaging may soften or disappear, core DEI values persist in adapted forms. This study offers a new perspective into how inclusion is evolving under pressure and highlights the resilience of DEI in software environments.
SMART: Tuning a symbolic music generation system with an audio domain aesthetic reward
Venue: arXiv cs.SD 2025
Year: 2025

Recent work has proposed training machine learning models to predict aesthetic ratings for music audio. Our work explores whether such models can be used to finetune a symbolic music generation system with reinforcement learning, and what effect this has on the system outputs. To test this, we use group relative policy optimization to finetune a piano MIDI model with Meta Audiobox Aesthetics ratings of audio-rendered outputs as the reward. We find that this optimization has effects on multiple low-level features of the generated outputs, and improves the average subjective ratings in a preliminary listening study with $14$ participants. We also find that over-optimization dramatically reduces diversity of model outputs.
Physically Consistent Humanoid Loco-Manipulation using Latent Diffusion Models
Venue: arXiv cs.RO 2025
Year: 2025

This paper uses the capabilities of latent diffusion models (LDMs) to generate realistic RGB human-object interaction scenes to guide humanoid loco-manipulation planning. To do so, we extract from the generated images both the contact locations and robot configurations that are then used inside a whole-body trajectory optimization (TO) formulation to generate physically consistent trajectories for humanoids. We validate our full pipeline in simulation for different long-horizon loco-manipulation scenarios and perform an extensive analysis of the proposed contact and robot configuration extraction pipeline. Our results show that using the information extracted from LDMs, we can generate physically consistent trajectories that require long-horizon reasoning.
DreamO: A Unified Framework for Image Customization
Venue: arXiv cs.CV 2025
Year: 2025

Recently, extensive research on image customization (e.g., identity, subject, style, background, etc.) demonstrates strong customization capabilities in large-scale generative models. However, most approaches are designed for specific tasks, restricting their generalizability to combine different types of condition. Developing a unified framework for image customization remains an open challenge. In this paper, we present DreamO, an image customization framework designed to support a wide range of tasks while facilitating seamless integration of multiple conditions. Specifically, DreamO utilizes a diffusion transformer (DiT) framework to uniformly process input of different types. During training, we construct a large-scale training dataset that includes various customization tasks, and we introduce a feature routing constraint to facilitate the precise querying of relevant information from reference images. Additionally, we design a placeholder strategy that associates specific placeholders with conditions at particular positions, enabling control over the placement of conditions in the generated results. Moreover, we employ a progressive training strategy consisting of three stages: an initial stage focused on simple tasks with limited data to establish baseline consistency, a full-scale training stage to comprehensively enhance the customization capabilities, and a final quality alignment stage to correct quality biases introduced by low-quality data. Extensive experiments demonstrate that the proposed DreamO can effectively perform various image customization tasks with high quality and flexibly integrate different types of control conditions.
Finding Important Stack Frames in Large Systems
Venue: arXiv cs.SE 2025
Year: 2025

In this work, we developed, integrated, and tested a feature that automatically highlights potentially important frames in stack traces. The feature was implemented in the internal bug-processing tool at JetBrains that processes tens of millions of stack traces. We surveyed 18 developers at JetBrains who provided valuable feedback on the idea and the implementation.
SCRAG: Social Computing-Based Retrieval Augmented Generation for Community Response Forecasting in Social Media Environments
Venue: arXiv cs.SI 2025
Year: 2025

This paper introduces SCRAG, a prediction framework inspired by social computing, designed to forecast community responses to real or hypothetical social media posts. SCRAG can be used by public relations specialists (e.g., to craft messaging in ways that avoid unintended misinterpretations) or public figures and influencers (e.g., to anticipate social responses), among other applications related to public sentiment prediction, crisis management, and social what-if analysis. While large language models (LLMs) have achieved remarkable success in generating coherent and contextually rich text, their reliance on static training data and susceptibility to hallucinations limit their effectiveness at response forecasting in dynamic social media environments. SCRAG overcomes these challenges by integrating LLMs with a Retrieval-Augmented Generation (RAG) technique rooted in social computing. Specifically, our framework retrieves (i) historical responses from the target community to capture their ideological, semantic, and emotional makeup, and (ii) external knowledge from sources such as news articles to inject time-sensitive context. This information is then jointly used to forecast the responses of the target community to new posts or narratives. Extensive experiments across six scenarios on the X platform (formerly Twitter), tested with various embedding models and LLMs, demonstrate over 10% improvements on average in key evaluation metrics. A concrete example further shows its effectiveness in capturing diverse ideologies and nuances. Our work provides a social computing tool for applications where accurate and concrete insights into community responses are crucial.
Can Knowledge Improve Security? A Coding-Enhanced Jamming Approach for Semantic Communication
Venue: arXiv cs.IT 2025
Year: 2025

As semantic communication (SemCom) attracts growing attention as a novel communication paradigm, ensuring the security of transmitted semantic information over open wireless channels has become a critical issue. However, traditional encryption methods often introduce significant additional communication overhead to maintain reliability, and conventional learning-based secure SemCom methods typically rely on a channel capacity advantage for the legitimate receiver, which is challenging to guarantee in real-world scenarios. In this paper, we propose a coding-enhanced jamming method that eliminates the need to transmit a secret key by utilizing shared knowledge, which may be part of the training set of the SemCom system, between the legitimate receiver and the transmitter. Specifically, we leverage the shared private knowledge base to generate a set of private digital codebooks in advance using neural network (NN)-based encoders. For each transmission, we encode the transmitted data into a digital sequence Y1 and associate Y1 with a sequence randomly picked from the private codebook, denoted as Y2, through superposition coding. Here, Y1 serves as the outer code and Y2 as the inner code. By optimizing the power allocation between the inner and outer codes, the legitimate receiver can reconstruct the transmitted data using successive decoding based on the shared index of Y2, while the eavesdropper's decoding performance is severely degraded, potentially to the point of random guessing. Experimental results demonstrate that our method achieves security comparable to state-of-the-art approaches while significantly improving the reconstruction performance of the legitimate receiver by more than 1 dB across varying channel signal-to-noise ratios (SNRs) and compression ratios.
LLM impact on BLV programming
Venue: arXiv cs.HC 2025
Year: 2025

Large Language Models (LLMs) are rapidly becoming integral to a wide range of tools, tasks, and problem-solving processes, especially in software development. Originally designed for natural language processing tasks such as text generation, LLMs are increasingly being used to assist both professionals and students in writing code. This growing reliance on LLM-based tools is reshaping programming workflows and task execution. In this study, we explore the impact of these technologies on blind and low-vision (BLV) developers. Our review of existing literature indicates that while LLMs help mitigate some of the challenges faced by BLV programmers, they also introduce new forms of inaccessibility. We conducted an evaluation of five popular LLM-powered integrated development environments (IDEs), assessing their performance across a comprehensive set of programming tasks. Our findings highlight several unsupported scenarios, instances of incorrect model output, and notable limitations in interaction support for specific tasks. Through observing BLV developers as they engaged in coding activities, we uncovered key interaction barriers that go beyond model accuracy or code generation quality. This paper outlines the challenges and corresponding opportunities for improving accessibility in the context of generative AI-assisted programming. Addressing these issues can meaningfully enhance the programming experience for BLV developers. As the generative AI revolution continues to unfold, it must also address the unique burdens faced by this community.
Analyzing Value Functions of States in Parametric Markov Chains
Venue: arXiv cs.LO 2025
Year: 2025

Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability properties is known to be coETR-complete, there have been efforts to approach it using potentially easier-to-check properties such as asking whether the pMC is monotonic in certain parameters. In this paper, we first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state. Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes, which in turn preserves verification results and monotonicity. We implement our algorithm to collapse "trivial" equivalence classes in the pMC and show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks; Second, the collapse speeds up existing algorithms to check monotonicity and parameter lifting, and hence can be used as a fast pre-processing step in practice.
SCALAR: A Part-of-speech Tagger for Identifiers
Venue: arXiv cs.SE 2025
Year: 2025

The paper presents the Source Code Analysis and Lexical Annotation Runtime (SCALAR), a tool specialized for mapping (annotating) source code identifier names to their corresponding part-of-speech tag sequence (grammar pattern). SCALAR's internal model is trained using scikit-learn's GradientBoostingClassifier in conjunction with a manually-curated oracle of identifier names and their grammar patterns. This specializes the tagger to recognize the unique structure of the natural language used by developers to create all types of identifiers (e.g., function names, variable names etc.). SCALAR's output is compared with a previous version of the tagger, as well as a modern off-the-shelf part-of-speech tagger to show how it improves upon other taggers' output for annotating identifiers. The code is available on Github
Evaluating energy inefficiency in energy-poor households in India: A frontier analysis approach
Venue: arXiv cs.CY 2025
Year: 2025

Energy-poor households often compromise their thermal comfort and refrain from operating mechanical cooling devices to avoid high electricity bills. This is compounded by certain behavioral practices like retention of older, less efficient appliances, resulting in missed energy savings. Thus, the need to enhance efficiency becomes critical in these households. However, due to a lack of comprehensive data in India, little is understood about their electricity consumption patterns and usage efficiency. Estimating inefficiency and assessing its determinants is crucial for improving their quality of life. This study measures the inefficiency in electricity consumption due to household practices and appliances in social housing in Mumbai, India. It considers technological determinants in addition to socio-economic variables. The study employs primary data collected from rehabilitation housing and slums in Mumbai. Stochastic frontier analysis, a parametric approach, is applied to estimate indicators of electricity consumption and inefficiency. While household size and workforce participation significantly affect consumption behavior in rehabilitation housing, it is limited to the workforce in slums. The ownership of appliances, except for washing machines in slums, also exhibits considerable impacts. The mean efficiency scores of 83% and 91% for rehabilitation housing and slums, respectively, empirically quantify the potential savings achievable. Factors that positively influence inefficiency include the duration of operating refrigerators, washing machines, iron, and AC. These results hold implications for enhancing the uptake of efficient appliances in addition to accelerating energy efficiency retrofits in the region. Policies should focus on awareness and the development of appliance markets through incentives.
Steering the CensorShip: Uncovering Representation Vectors for LLM "Thought" Control
Venue: arXiv cs.CL 2025
Year: 2025

Large language models (LLMs) have transformed the way we access information. These models are often tuned to refuse to comply with requests that are considered harmful and to produce responses that better align with the preferences of those who control the models. To understand how this "censorship" works. We use representation engineering techniques to study open-weights safety-tuned models. We present a method for finding a refusal--compliance vector that detects and controls the level of censorship in model outputs. We also analyze recent reasoning LLMs, distilled from DeepSeek-R1, and uncover an additional dimension of censorship through "thought suppression". We show a similar approach can be used to find a vector that suppresses the model's reasoning process, allowing us to remove censorship by applying the negative multiples of this vector. Our code is publicly available at: https://github.com/hannahxchen/llm-censorship-steering
MASR: Self-Reflective Reasoning through Multimodal Hierarchical Attention Focusing for Agent-based Video Understanding
Venue: arXiv cs.CV 2025
Year: 2025

Even in the era of rapid advances in large models, video understanding remains a highly challenging task. Compared to texts or images, videos commonly contain more information with redundancy, requiring large models to properly allocate attention at a global level for comprehensive and accurate understanding. To address this, we propose a Multimodal hierarchical Attention focusing Self-reflective Reasoning (MASR) framework for agent-based video understanding. The key innovation lies in its ability to detect and prioritize segments of videos that are highly relevant to the query. Firstly, MASR realizes Multimodal Coarse-to-fine Relevance Sensing (MCRS) which enhances the correlation between the acquired contextual information and the query. Secondly, MASR employs Dilated Temporal Expansion (DTE) to mitigate the risk of missing crucial details when extracting semantic information from the focused frames selected through MCRS. By iteratively applying MCRS and DTE in the self-reflective reasoning process, MASR is able to adaptively adjust the attention to extract highly query-relevant context and therefore improve the response accuracy. In the EgoSchema dataset, MASR achieves a remarkable 5% performance gain over previous leading approaches. In the Next-QA and IntentQA datasets, it outperforms the state-of-the-art standards by 0.2% and 0.3% respectively. In the Video-MME dataset that contains long-term videos, MASR also performs better than other agent-based methods.
How Jungian Cognitive Functions Explain MBTI Type Prevalence in Computer Industry Careers
Venue: arXiv cs.CY 2025
Year: 2025

This study investigates the relationship between Carl Jung's cognitive functions and success in computer industry careers by analyzing the distribution of Myers-Briggs Type Indicator (MBTI) types among professionals in the field. Building on Carl Jung's theory of psychological types, which categorizes human cognition into four primary functions, Sensing, Intuition, Thinking, and Feeling, this study investigates how these functions, when combined with the attitudes of Extraversion and Introversion, influence personality types and career choices in the tech sector. Through a comprehensive analysis of data from 30 studies spanning multiple countries and decades, encompassing 18,264 individuals in computer-related professions, we identified the most prevalent cognitive functions and their combinations. After normalizing the data against general population distributions, our findings showed that individual Jungian functions (Te, Ni, Ti, Ne), dual function combinations (Ni-Te, Ti-Ne, Si-Te, Ni-Fe), and MBTI types (INTJ, ENTJ, INTP, ENTP, ISTJ, INFJ, ESTJ, ESTP) had significantly higher representation compared to general population norms. The paper addresses gaps in the existing literature by providing a more nuanced understanding of how cognitive functions impact job performance and team dynamics, offering insights for career guidance, team composition, and professional development in the computer industry, and a deeper understanding of how cognitive preferences influence career success in technology-related fields.
Precision Neural Network Quantization via Learnable Adaptive Modules
Venue: arXiv cs.CV 2025
Year: 2025

Quantization Aware Training (QAT) is a neural network quantization technique that compresses model size and improves operational efficiency while effectively maintaining model performance. The paradigm of QAT is to introduce fake quantization operators during the training process, allowing the model to autonomously compensate for information loss caused by quantization. Making quantization parameters trainable can significantly improve the performance of QAT, but at the cost of compromising the flexibility during inference, especially when dealing with activation values with substantially different distributions. In this paper, we propose an effective learnable adaptive neural network quantization method, called Adaptive Step Size Quantization (ASQ), to resolve this conflict. Specifically, the proposed ASQ method first dynamically adjusts quantization scaling factors through a trained module capable of accommodating different activations. Then, to address the rigid resolution issue inherent in Power of Two (POT) quantization, we propose an efficient non-uniform quantization scheme. We utilize the Power Of Square root of Two (POST) as the basis for exponential quantization, effectively handling the bell-shaped distribution of neural network weights across various bit-widths while maintaining computational efficiency through a Look-Up Table method (LUT). Extensive experimental results demonstrate that the proposed ASQ method is superior to the state-of-the-art QAT approaches. Notably that the ASQ is even competitive compared to full precision baselines, with its 4-bit quantized ResNet34 model improving accuracy by 1.2\% on ImageNet.