Understanding information-dense documents like recipes and scientific papers requires readers to find, interpret, and connect details scattered across text, figures, tables, and other visual elements. These documents are often long and filled with specialized terminology, hindering the ability to locate relevant information or piece together related ideas. Existing tools offer limited support for synthesizing information across media types. As a result, understanding complex material remains cognitively demanding. This paper presents a framework for fine-grained integration of information in complex documents. We instantiate the framework in an augmented reading interface, which populates a scientific paper with clickable points on figures, interactive highlights in the body text, and a persistent reference panel for accessing consolidated details without manual scrolling. In a controlled between-subjects study, we find that participants who read the paper with our tool achieved significantly higher scores on a reading quiz without evidence of increased time to completion or cognitive load. Fine-grained integration provides a systematic way of revealing relationships within a document, supporting engagement with complex, information-dense materials.

Users of feature-rich tools like Excel often miss more efficient workflows, repeating tedious steps and making avoidable errors. Current approaches to helping them require either manual prompting, which is effortful for users, or automated logging, which is limiting for developers. We present InvisibleMentor, a system inspired by over-the-shoulder learning: it observes what users do, then shows them how to do it better. To do this, InvisibleMentor analyzes screen recordings with a vision-language model to reconstruct actions and context, then uses a large language model to generate vision-grounded task reflection, structured suggestions grounded in observed behavior. In a user study, participants found InvisibleMentor’s suggestions more clear, more relevant, and more useful than those from a prompt-based assistant, demonstrating that AI can do more than automate away work—it can help users master it.

The landscape of technology for consuming information is changing rapidly. One mode of information consumption, reading, stands to see profound changes due to its ubiquity and frequency as a cognitive task. Better reading technology could transform texts on demand so that they are easier to read, surface hard-to-find information, support synthesis, and better engage readers. The possibilities have been considerably expanded with the maturation of AI. The purpose of this workshop is to provide a platform for the growing cohort of HCI and AI researchers interested in augmented reading interfaces to define high-impact areas of development and standards of success. This platform will arise from two components of our workshop. The first is a brief and engaging format of introductions among community members through lightning talks. The second is a set of affinity group activities that will identify fresh opportunities for augmenting reading against the backdrop of reading theories, evaluation practices, and emerging technology.

Developing a novel research idea is hard. It must be distinct enough from prior work to claim a contribution while also building on it. This requires iteratively reviewing literature and refining an idea based on what a researcher reads; yet when an idea changes, the literature that matters often changes with it. Most tools offer limited support for this interplay: literature tools help researchers understand a fixed body of work, while ideation tools evaluate ideas against a static, pre-curated set of papers. We introduce literature-initiated pivots, a mechanism where engagement with literature prompts revision to a developing idea, and where that revision changes which literature is relevant. We operationalize this in LitPivot, where researchers concurrently draft and vet an idea. LitPivot dynamically retrieves clusters of papers relevant to a selected part of the idea and proposes literature-informed critiques for how to revise it. A lab study (n=17) shows researchers produced higher-rated ideas with stronger self-reported understanding of the literature space; an open-ended study (n=5) reveals how researchers use LitPivot to iteratively evolve their own ideas.

LLM-generated explanations can make technical content more accessible, but there is a ceiling on what they can support interactively. Because LLM outputs are static text, they cannot be executed or stepped through. We argue that grounding explanations in a formalized representation enables interactive affordances beyond what static text supports. We instantiate this idea for mathematical proof comprehension with explorable theorems, a system that uses LLMs to translate a theorem and its written proof into Lean, a programming language for machine-checked proofs, and links the written proof with the Lean code. Readers can work through the proof at a step-level granularity, test custom examples or counterexamples, and trace the logical dependencies bridging each step. Each worked-out step is produced by executing the Lean proof on that example and extracting its intermediate state. A user study (n = 16) shows potential advantages of this approach: in a proof-reading task, participants who had access to the provided explorability features gave better, more correct, and more detailed answers to comprehension questions, demonstrating a stronger overall understanding of the underlying mathematics.

This work serves to inform the design of better health information technology for intricate care scenarios. We focus on a situation involving a severe condition, child patients, rich know-how, and complex caregiver networks—childhood asthma in our local urban community. Conducting design investigations with 23 caregivers who are predominantly Black and single across 14 interviews and 2 workshop sessions, we offer the following observations. First, caregivers draw on rich knowledge about triggers, mitigations, and medication, which often reflect medical consensus, but occasionally conflict. Second, asthma care involves acute, highly stressful episodes, exemplified by caregivers’ nighttime monitoring and management. Third, care systems are distributed among parent, child, broader family, and schools. This leads to decentralized information and responsibility, communication needs, and concerns around reliability of care. We conclude if health technology is to support this situation, it will mind community knowledge, intense acute episodes, and the decentralized and heterogeneous nature of care.

As AI-generated texts proliferate, how can people better understand the veracity of these texts? One increasingly common solution is linking AI-generated text to the sources from which they were derived. We call this design pattern traceable text. In this paper, we present a usability study of the effects of a traceable text on reading an AI-generated summary alongside a source document. We focus on a variant of traceable text that we expect to be increasingly common and general: phrase-level links from summary to source texts. With the traceable text, readers answered questions about the source text more quickly and more accurately when generated summaries contained hallucinations. In an open-ended task, participants used traceable text to aid understanding and to index into the texts. We define a broader design space of traceable text informed by examples in the literature.

AI question answering systems increasingly generate responses with attributions to sources. However, the task of verifying the actual content of these attributions is in most cases impractical. In this paper, we present attribution gradients as a solution. Attribution gradients provide integrated, incremental affordances for diving into an attributed passage. A user can decompose a sentence of an answer into its claims. For each claim, the user can view supporting and contradictory excerpts mined from sources. Those excerpts serve as clickable conduits into the source (in our application, scientific papers). When evidence itself contains more citations, the UI unpacks the evidence into excerpts from the cited sources. These features of attribution gradients facilitate concurrent interconnections among answer, claim, excerpt, and context. In a usability study, we observed greater engagement with sources and richer revision in a task where participants revised an attributed AI answer with attribution gradients and a baseline.

Today's most advanced vision-language models (VLMs) remain proprietary. The strongest open-weight models rely heavily on synthetic data from proprietary VLMs to achieve good performance, effectively distilling these closed VLMs into open ones. As a result, the community has been missing foundational knowledge about how to build performant VLMs from scratch. We present Molmo, a new family of VLMs that are state-of-the-art in their class of openness. Our key contribution is a collection of new datasets called PixMo, including a dataset of highly detailed image captions for pre-training, a free-form image Q A dataset for fine-tuning, and an innovative 2D pointing dataset, all collected without the use of external VLMs. The success of our approach relies on careful modeling choices, a well-tuned training pipeline, and, most critically, the quality of our newly collected datasets. Our best-in-class 72B model not only outperforms others in the class of open weight and data models, but also outperforms larger proprietary models including Claude 3.5 Sonnet, and Gemini 1.5 Pro and Flash, second only to GPT-4o based on both academic benchmarks and on a large human evaluation. Our model weights, new datasets, and source code are available at https://molmo.allenai.org/blog.

Interactive theorem provers, or proof assistants, are important tools across many areas of computer science and mathematics, but even experts find them challenging to use effectively. To improve their design, we need a deeper, user-centric understanding of proof assistant usage. We present the results of an observation study of proof assistant users. We use contextual inquiry methodology, observing 30 participants doing their everyday work in Rocq and Lean. We qualitatively analyze their experiences to surface four observations: that proof writers iterate on their proofs by reacting to and incorporating feedback from the proof assistant; that proof progress often involves challenging conversations with the proof assistant; that proofs are constructed in consultation with a wide array of external resources; and that proof writers are guided by design considerations that go beyond "getting to QED." Our documentation of these themes clarifies what proof assistant usage looks like currently and identifies potential opportunities that researchers should consider when working to improve the usability of proof assistants.

Developers often find themselves asking questions that cut across a code base. Answering these questions requires gathering relevant facts and tracing flow through the program. Yet today’s tools offer limited support for answering these questions. Developers can either use imprecise AI tools that ignore flow or flow-tracing tools that impose a great number of choices. In this paper, we introduce a new kind of tool that answers questions better by bringing together elements of both AI and flow. We instantiate this idea in Trailblazer, a system underpinned by an AI agent that simulates an information forager, iteratively tracing program dependencies in search of answers. Then, Trailblazer packages information it found into an answer digest, which includes interactive, annotated traces of exploration. These traces can be stepped through to help developers orient to the code and find where the answer is distributed within it. In a lab study, Trailblazer helped participants answer questions more efficiently and gain greater familiarity with program flow than an AI question answering baseline. This shows how AI agents can leverage program flow to bring additional structure and clarity to its answers.

Authors of typeset formulas augment those formulas to make them easier to understand. When they do so, they trade off between using markup tools like LaTeX and formula-unaware graphical editors. In this paper, we explore how editing tools could combine the best affordances of both kinds of tools. We develop FreeForm, a projectional editor wherein authors can augment formulas—with color, labels, spacing, and more—across multiple synchronized representations. Augmentations are created graphically using direct selections and compact menus. Those augmentations propagate to LaTeX markup, which can itself be edited and easily exported. In two lab studies, we observe the value of our editor versus baselines of a widely-used LaTeX document editor and a state-of-the-art formula augmentation tool. Finally, we make recommendations for the design of projectional markup augmentation editors.

Reasoning about images with rich text, such as charts and documents, is a critical application of vision-language models (VLMs). However, VLMs often struggle in these domains due to the scarcity of diverse text-rich vision-language data. To address this challenge, we present CoSyn, a framework that leverages the coding capabilities of text-only large language models (LLMs) to automatically create synthetic text-rich multimodal data. Given input text describing a target domain (e.g., "nutrition fact labels"), CoSyn prompts an LLM to generate code (Python, HTML, LaTeX, etc.) for rendering synthetic images. With the underlying code as textual representations of the synthetic images, CoSyn can generate high-quality instruction-tuning data, again relying on a text-only LLM. Using CoSyn, we constructed a dataset comprising 400K images and 2.7M rows of vision-language instruction-tuning data. Comprehensive experiments on seven benchmarks demonstrate that models trained on our synthetic data achieve state-of-the-art performance among competitive open-source models, including Llama 3.2, and surpass proprietary models such as GPT-4V and Gemini 1.5 Flash. Furthermore, CoSyn can produce synthetic pointing data, enabling VLMs to ground information within input images, showcasing its potential for developing multimodal agents capable of acting in real-world environments.

Software developers increasingly rely on automated methods to assess the correctness of their code. One such method is property-based testing (PBT), wherein a test harness generates hundreds or thousands of inputs and checks the outputs of the program on those inputs using parametric properties. Though powerful, PBT induces a sizable gulf of evaluation: developers need to put in nontrivial effort to understand how well the different test inputs exercise the software under test. To bridge this gulf, we propose Tyche, a user interface that supports sensemaking around the effectiveness of property-based tests. Guided by a formative design exploration, our design of Tyche supports developers with interactive, configurable views of test behavior with tight integrations into modern developer testing workflow. These views help developers explore global testing behavior and individual test inputs alike. To accelerate the development of powerful, interactive PBT tools, we define a standard for PBT test reporting and integrate it with a widely used PBT library. A self-guided online usability study revealed that Tyche’s visualizations help developers to more accurately assess software testing effectiveness.

As AI-generated summaries proliferate, how can we help people understand the veracity of those summaries? In this short paper, we design a simple interaction primitive, traceable text, to support critical examination of generated summaries and the source texts they were derived from. In a traceable text, passages of a generated summary link to passages of the source text that informed them. A traceable text can be generated with a straightforward prompt chaining approach, and optionally adjusted by human authors depending on application. In a usability study, we examined the impact of traceable texts on reading and understanding patient medical records. Traceable text helped readers answer questions about the content of the source text more quickly and markedly improved correctness of answers in cases where there were hallucinations in the summaries. When asked to read a text of personal importance with traceable text, readers employed traceable text as an understanding aid and as an index into the source note.

Property-based testing (PBT) is a testing methodology where users write executable formal specifications of software components and an automated harness checks these specifications against many automatically generated inputs. From its roots in the QuickCheck library in Haskell, PBT has made significant inroads in mainstream languages and industrial practice at companies such as Amazon, Volvo, and Stripe. As PBT extends its reach, it is important to understand how developers are using it in practice, where they see its strengths and weaknesses, and what innovations are needed to make it more effective. We address these questions using data from 30 in-depth interviews with experienced users of PBT at Jane Street, a financial technology company making heavy and sophisticated use of PBT. These interviews provide empirical evidence that PBT's main strengths lie in testing complex code and in increasing confidence beyond what is available through conventional testing methodologies, and, moreover, that most uses fall into a relatively small number of high- leverage idioms. Its main weaknesses, on the other hand, lie in the relative complexity of writing properties and random data generators and in the difficulty of evaluating their effectiveness. From these observations, we identify a number of potentially high-impact areas for future exploration, including performance improvements, differential testing, additional high-leverage testing scenarios, better techniques for generating random input data, test-case reduction, and methods for evaluating the effectiveness of tests.

Software developers increasingly rely on automated methods to assess the correctness of their code. One such method is property-based testing (PBT), wherein a test harness generates hundreds or thousands of inputs and checks the outputs of the program on those inputs using parametric properties. Though powerful, PBT induces a sizable gulf of evaluation: developers need to put in nontrivial effort to understand how well the different test inputs exercise the software under test. To bridge this gulf, we propose TYCHE, a user interface that supports sensemaking around the effectiveness of property-based tests. Guided by a formative design exploration, our design of TYCHE supports developers with interactive, configurable views of test behavior with tight integrations into modern developer testing workflow. These views help developers explore global testing behavior and individual test inputs alike. To accelerate the development of powerful, interactive PBT tools, we define a standard for PBT test reporting and integrate it with a widely used PBT library. A self-guided online usability study revealed that TYCHE's visualizations help developers to more accurately assess software testing effectiveness.

Medical progress notes have recently become available to patients at an unprecedented scale. Progress notes offer patients insight into their care that they cannot find elsewhere. That said, reading a note requires patients to contend with the language, unspoken assumptions, and clutter common to clinical documentation. As the health system reinvents many of its interfaces to incorporate AI assistance, this paper examines what intelligent interfaces could do to help patients read their progress notes. In a qualitative study, we examine the needs of patients as they read a progress note. We then formulate a vision for the explainable note, an augmented progress note that provides support for directing attention, phrase-level understanding, and tracing lines of reasoning. This vision manifests in a set of patient-inspired opportunities for advancing intelligent interfaces for writing and reading progress notes.

Scholars need to keep up with an exponentially increasing flood of scientific papers. To aid this challenge, we introduce Scim , a novel intelligent interface that helps scholars skim papers to rapidly review and gain a cursory understanding of its contents. Scim supports the skimming process by highlighting salient content within a paper, directing a scholar’s attention. These automatically-extracted highlights are faceted by content type, evenly-distributed across a paper, and have a density configurable by scholars. We evaluate Scim with an in-lab usability study and a longitudinal diary study, revealing how its highlights facilitate the more efficient construction of a conceptualization of a paper. Finally, we describe the process of scaling highlights from their conception within Scim , a research prototype, to production on over 521,000 papers within the Semantic Reader, a publicly-available augmented reading interface for scientific papers. We conclude by discussing design considerations and tensions for the design of future skimming tools with augmented intelligence.