Papers for

software developers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Semantic matching improves search and summaries for coding videos

Intelligent Semantic Matching (ISM) for Video Tutorial Search using Transformer Models

Abstract: The rise in the number and diversity of available software development video tutorials has enhanced digital learning for developers but also introduced challenges in locating relevant content efficiently. Existing video search methods, including keyword-based approaches and tools like CodeTube and TechTube, rely primarily on retrieval algorithms such as BM25, which fail to capture the semantic nuances and user intentions behind search queries. To address these limitations, we introduce ISM, an approach that uses SBERT to generate semantically rich vectors from video tutorial transcripts to improve the search for programming video tutorials. By segmenting transcripts and implementing a re-ranking process, ISM effectively preserves context and enhances the relevance of search results. Additionally, ISM generates informative video summaries using GPT-4, allowing developers to quickly assess the relevance of video content. To evaluate our approach, we first performed a quantitative study comparing ISM with the baseline TechTube. The results revealed that ISM performs better in both video retrieval and fragment identification, achieving a Hit@5 score of 0.95 and an average F1 score of 0.70 compared to the baseline's 0.58 and 0.52, respectively. We also performed a user study, which revealed that users strongly preferred the semantic matching capabilities and AI-generated summaries of our approach. This work advances the state-of-the-art in programming video tutorial search and summarization by offering more nuanced and user-aligned retrieval and summarization mechanisms.

Fri 11 SeptSoftware Engineering
The gist
Finding the right software tutorial videos can be hard because usual searches only look for keywords, missing the true meaning behind questions. The authors created ISM, which understands the meaning of video transcripts to better match search queries. It breaks videos into parts and reorders results to keep the context clear. ISM also uses AI to make helpful video summaries so developers can quickly decide if a video is useful. Their tests showed ISM finds better matches and users liked the smart search and summaries.
Open 2609.12921v1

Agentic retrying drives query improvement more than feedback style

What Drives Recovery in Agentic Text-to-Cypher? LAST-CQ: An LLM Agent Self-Refinement Framework

Abstract: Agentic pipelines for structured-query generation are rapidly expanding, but it is unclear which part of the loop produces the gain. We use LAST-CQ -- a five-agent, training-free, execution-grounded Text-to-Cypher framework -- as an instrumented testbed, running three counterfactuals over 2,471 live-database queries and six backbones spanning three vendor scale tiers. Removing correction is worth between 3.1% aggregate execution-BLEU against the single-pass system and 12.3% against a no-refinement counterfactual (up to 80.7% for the weakest backbone). Replacing schema-grounded, LLM-synthesised feedback with raw database error strings costs almost nothing (20.9% vs. 19.9% naive exact match; <0.2% end-to-end; equivalent within $\pm 0.075$ set-F1 by two one-sided tests). Spending the same call budget on parallel sampling degrades quality by 10-11%. What works is detecting failure and routing it to a retry, not the feedback sophistication or number of samples. LAST-CQ itself recovers 91.7% of queries that fail under single-pass generation, while a query that succeeds first time still costs exactly one LLM call. We also show that n-gram overlap on serialised results is not a bound in either direction: it over-scores against set equivalence on 65.9% of results while under-scoring against judged semantics. Finally, we calibrate our LLM judge against blind human labels and find it optimistic by 9 points.

Fri 11 SeptArtificial IntelligenceComputation and LanguageMachine Learning
The gist
Generating database queries from text can be hard because the system might make mistakes. The authors study a multi-agent system that tries queries, notices failures, and retries to fix problems. They find that simply detecting failures and retrying is what leads to better results, not complex feedback or more guesses. Their method recovers most queries that initially fail, making the system much more reliable. They also show that some common ways to measure success can be misleading.
Open 2609.12746v1

Bengali vision language models struggle with geometry diagrams and text

ChitraMiti: Benchmarking Visual Grounding and Modality Reliance in Bengali Geometric Reasoning

Abstract: Evaluation of vision-language models (VLMs) for multimodal mathematical reasoning remains limited for low-resource languages and for geometry problems that require reading a diagram and a question together. We introduce ChitraMiti-12.8k, a synthetic benchmark of 12,874 Bengali planar geometry problems paired with structured 15-attribute descriptions, and NCTB-500, a complementary set of 500 diagrams manually extracted from Bengali school textbooks. Using a three-phase protocol that separates diagram-only, diagram-plus-description, and description-only inputs, we show across five open-weight and closed-source VLMs that description-only performance is statistically indistinguishable from diagram-plus-description performance, establishing structured descriptions as a sufficient textual proxy for controlled evaluation. Despite this, models remain poor at cross-modal verification, frequently misled by a swapped spatial relation even when they answer the unmodified item correctly. We further evaluate supervised adaptation on ChitraMiti-12.8k, finding that fine-tuning improves performance on both ChitraMiti-1k and NCTB-500, although a substantial gap to the strongest zero-shot model remains. Together, ChitraMiti-12.8k, NCTB-500, and our evaluation protocol offer a standardized way to study Bengali multimodal geometry reasoning and, more broadly, whether VLMs actually check their text against what they see. Our dataset and code are publicly available on Hugging Face at https://huggingface.co/datasets/RaiyanKhaan/ChitraMiti.

Fri 11 SeptComputer Vision and Pattern Recognition
The gist
It is hard for computer models that understand both images and language to solve math problems in Bengali, especially those involving geometric diagrams. The authors created a large set of Bengali geometry problems with both pictures and detailed text descriptions to test these models. They found that models do about the same when given only text descriptions as when given both images and text, showing the descriptions can stand in for diagrams in tests. However, models often fail when asked to confirm that the text matches the image, mixing up spatial relationships. Training the models on this dataset helps, but they still lag behind the best models used without extra training. Overall, this work gives a new way to study how models handle math problems combining images and language in Bengali.
Open 2609.12509v1

Parallel tool-use agents face challenges in error recovery and localization

ParaRecover: A Process-Level Benchmark for Error Localization and Recovery in Parallel Tool-Use Agents

Abstract: Existing agent benchmarks mainly evaluate final task success or tool-call correctness, providing limited insight into whether agents can reliably diagnose and recover from intermediate execution failures. This limitation becomes particularly critical in multi-turn parallel tool-use scenarios, where errors may propagate across dependent branches and trigger cascading failures. We introduce ParaRecover, a process-level benchmark for evaluating error localization and recovery in multi-turn parallel tool-use agents. Built upon a fine-grained taxonomy of 14 error types covering planning dependencies, tool selection, and argument matching, the benchmark comprises 10,626 instances spanning two difficulty levels. To enable finegrained, process-oriented evaluation, we further propose the SDE rubric, which measures structural integrity, diagnostic reasoning, and evolutionary strategy during agent execution.Experiments across more than ten mainstream LLMs reveal that even state-of-the-art models still struggle with multi-turn error propagation,implicit tool-use failures, and precise replanning. Moreover, we demonstrate that the SDE rubric provides effective supervision signals for improving agents' reflective recovery capabilities. Our data and code are available at https://github.com/gbw206/ParaRecover.

Fri 11 SeptMachine LearningSoftware Engineering
The gist
Many AI agents use tools to complete tasks, but they often fail to spot and fix errors along the way. The authors created ParaRecover, a large set of test cases that show different types of mistakes agents make when working with multiple tools at once. They also made a scoring system to check how well agents can find and fix these mistakes during their work. Tests show even top AI models struggle with error propagation and replanning. Their scoring method can help improve agents' ability to reflect and recover from mistakes.
Open 2609.12345v1

Byte based models exceed token models after more training

Breaking the Token Ceiling: Distilling Smaller, Stronger Byte Models

Abstract: Small models are made more capable through distillation from a larger one that shares their tokenization scheme. However, do distilled byte and token models behave similarly in terms of scaling trends as compute and data increases? To enable this comparison, we introduce two variants to efficiently convert token logits to Byte Logits: 1) approximate: Marginalize-It, and 2) exact: End-Of-Token. We then present the first large scale study of overtraining decoder-only dense transformer models varying two dimensions simultaneously: the tokenization scheme (Tokens, Bytes, Bytes w/ eot) and the training objective (Distillation vs. Cross-Entropy), sweeping layer-parameter-matched models with roughly 1 billion parameters up to 1 trillion bytes of data. Across eight benchmarks spanning three categories: Multiple Choice QA, Language Generation, and Machine Translation, we find that Token-1B models outperform byte models (End-Of-Token-1B and Bytes-1B) in the low-FLOP regime but eventually plateau; byte models start worse yet surpass Token-1B models with more compute, reaching a higher downstream task performance ceiling. Extrapolating the average top-1 error vs. validation BPB scaling laws predicts that, asymptotically, distilled End-Of-Token-1B outperforms distilled Token-1B by up to 4%. They are also far more data efficient, matching the performance of distilled Token-1B using only one-sixth of the training data. Moreover, by operating over a small vocabulary of 256 bytes instead of on the order of 100K tokens, they circumvent the need for top-k truncation during logit dumping, while also reducing logit storage costs to roughly one-fifth. Finally, our downstream performance scaling laws predict that our distilled End-Of-Token-1B models asymptotically surpass the Llama 3.2-1B, Gemma-3-1B-pt, and Gemma 2B models on averaged downstream tasks by up to 6.5%, 8.1%, and 2.1%, respectively.

Fri 11 SeptComputation and LanguageArtificial IntelligenceMachine Learning
The gist
Training small language models is often done by copying knowledge from larger models using a method called distillation. This paper compares models that work with normal words (tokens) versus those that use bytes, the smallest unit of digital text. The authors found that, although token-based models start off better when trained with limited computing power, byte-based models improve more steadily and eventually outperform token models with more training. Byte models also need less data and memory during training and prediction. This suggests that using bytes could make smaller models stronger and more efficient.
Open 2609.12303v1

Neural models speed up constraint learning with less user input

Learning Symbolic Constraint Representations from Examples: A Neuro-Symbolic Approach

Abstract: Learning user-defined concepts as constraint networks has been extensively studied in the constraint acquisition (CA) literature. However, existing approaches typically rely on intensive interactions with a human oracle, making the learning process costly in terms of time and number of queries. In this paper, we propose a neuro-symbolic framework for automatic CA that significantly reduces user involvement by introducing neural Oracle Transformer models which learn to emulate user responses and to generalize conceptual knowledge. Trained on previously available examples, the learned oracle interacts with a dedicated CA engine, FastCA, which systematically refines the oracle's responses into a sound, consistent, and interpretable constraint network. This neuro-symbolic interaction enables the recovery of structured symbolic models from data without prior domain knowledge. Our results demonstrate that this neuro-symbolic interplay effectively aligns data-driven pattern recognition with symbolic reasoning, offering a robust approach to automating model construction in combinatorial domains.

Thu 10 SeptArtificial Intelligence
The gist
Learning complex rules from examples usually needs lots of questions answered by a human, which takes a lot of time. The authors created a system that uses neural networks to mimic human answers, so it asks fewer questions and learns faster. This system then works with a special solver to turn those answers into clear rules computers can understand. Their approach helps combine quick pattern spotting with precise logical thinking to build models automatically, even when no prior knowledge is given.
Open 2609.12267v1

Graph theory agent improves large language models on complex graph reasoning tasks

GTA: Graph Theory Agent and Benchmark for Algorithmic Graph Reasoning with LLMs

Abstract: Large Language Models (LLMs) are increasingly asked to reason over structured data such as graphs, yet how reliably they can carry out multi-step graph algorithms in language remains unclear. Existing evaluations tend to use simple tasks on small graphs, to score code generation rather than reasoning over the graph itself, or to fix a single input format. We introduce Graph Theory Bench (GT Bench), a benchmark covering 24 classical graph problems in 44 task-structure settings, with over 100,000 examples across four representations: natural language, structured language, adjacency list, and adjacency matrix. Evaluating eight LLMs on GT Bench shows that accuracy is strongly tied to the input representation, that the best representation shifts with graph density, size, and topology as well as with the model, and that this sensitivity persists, attenuated, in the strongest reasoning models. Building on these observations, we propose the Graph Theory Agent (GTA), which pairs a preference-trained representation selector with plan-and-decompose scaffolding around a frozen executor LLM. GTA lifts Phi-4 from 53.5% to 69.1% on the benchmark's easy split and from 33.0% to 41.5% on its hard split, outperforming eight prompting and agent baselines, and transfers without retraining to GraCoRe and NLGraph. Code for benchmark generation and evaluation: https://github.com/xzx34/GTA. The project homepage is available at https://xzx34.github.io/gta/.

Thu 10 SeptArtificial Intelligence
The gist
Large language models (LLMs) struggle to solve complex problems involving graphs, like networks or connections. The authors created a big test set with many graph problems in several formats to see how well different LLMs perform. They found that how you present the graph data greatly affects the model’s accuracy, depending on graph size and type. Then, they designed a new method called Graph Theory Agent that chooses the best graph format and breaks down problems, which makes models better at solving these tasks.
Open 2609.12265v1

Autonomous agents’ reports reveal partial story of their actions

Plans They Abandon, Reports They Author: The Narrative Layer of Autonomous Agents

Abstract: When a coding agent finishes a task, the developer reviews a summary the agent wrote about itself, not a display someone designed. We ask how much of the agent's work that summary carries, and whether it drifts toward the plan the agent stated when execution departed from it. Across 5,851 real developer sessions and 355,942 tool calls, a self-report referred to about one action in eleven, and a reader working from the report alone recovered roughly a fifth of the action log. Neither figure depended on whether the session later needed human correction. Reports did not generally resemble the stated plan more than the executed one, but they did so increasingly as execution diverged from the plan. We hand-validate both measurement steps that use a language model, report the one that failed alongside the one that passed, and draw conclusions only from measures that survived.

Thu 10 SeptHuman-Computer Interaction
The gist
When coding agents finish tasks, developers read summaries the agents write about themselves instead of detailed logs. The authors studied thousands of real sessions and found that these summaries include only a small portion of the agent’s actions and only partially reflect what actually happened. Interestingly, when agents stray more from their original plan, their summaries tend to refer more to that plan. The study carefully verified the measurements using language models to make sure only reliable results were reported.
Open 2609.12205v1

VikingRAG reduces tokens for accurate retrieval in structured documents

VikingRAG: Accurate and Token-efficient Retrieval-augmented Generation over Structured Documents

Abstract: State-of-the-art retrieval-augmented generation (RAG) methods exploit document structures to acquire sufficient evidence, but often incur substantial token costs. To reduce structural-context tokens without compromising high RAG accuracy, we present {\sf VikingRAG}, a directory-aware semantic data management system that tightly integrates semantic and structural access to support structural-context-efficient, evidence-gap-driven multi-round retrieval. To further reduce token overhead of multi-round interaction, we materialize agentic multi-round retrieval traces as experience edges, and reuse these edges for similar queries, avoiding repeated multi-round exploration. To additionally reduce token costs when agentic multi-round retrieval is unnecessary, we introduce an adaptive escalation strategy that answers from one-round experience-augmented retrieval when the evidence is sufficient, and invokes agentic multi-round retrieval only otherwise. Experiments on real datasets show that the base system {\sf VikingRAG} matches high accuracy of state-of-the-art methods while consuming only 11.6\%--51.9\% of their tokens. With retrieval-trace reuse and adaptive escalation, token costs drop to 5.1\%--32.5\% while maintaining competitive accuracy and practical document-storage performance, showing the utility of this work for emerging AI knowledge bases.

Thu 10 SeptInformation RetrievalArtificial IntelligenceComputation and Language
The gist
Finding the right information in long, complex documents can be slow and expensive because of how many words a computer must process at once. The authors built VikingRAG, a system that smartly looks through document structures to find answers with fewer words, saving effort without losing accuracy. It also remembers past searches to avoid repeating work and decides when simple or deeper searches are needed. Experiments show it uses much fewer words than current methods but still finds the right info well.
Open 2609.11390v1

Agent-integrated software improves how users control shared intelligent systems

Agent-Integrated Software: Interaction Contracts and Continuous Assurance

Abstract: Embedding an intelligent agent in an existing application creates a persistent coordination problem: users can revise goals and manipulate shared objects while delegated execution continues. We argue that dependable integration requires an explicit correspondence between task-level interaction and application behavior. We introduce Agent-Integrated Software (AIS) as a software pattern combining a conventional core, direct interaction, and a built-in agent, and Intent-Level Interaction Abstraction (IIA) as the task semantics through which users inspect and control delegated work. An open transition-system model relates AIS execution to IIA states and events. Interaction contracts constrain this relation through task bindings, role-specific authority, control transitions, and outcome evidence; continuous assurance maintains scoped claims as their dependencies change. A compact disclosure contract and conditional propositions illustrate why local component validity is insufficient and how selected admission invariants can be separated from planning. Contrasting software domains expose the framework's assumptions and limits. This perspective develops a research agenda spanning application abstraction, development support, controlled execution, quality assessment, and human supervision, with the aim of making agent integration a maintainable software engineering discipline.

Thu 10 SeptSoftware EngineeringArtificial Intelligence
The gist
It can be hard to manage smart agents that keep working inside apps while users change goals or data. The authors introduce Agent-Integrated Software, a way to create software that clearly links user tasks and app actions. They propose a model and rules to help users understand and control the agent's work continuously, ensuring its actions stay trustworthy. This approach aims to make integrating intelligent agents into software easier to build and maintain.
Open 2609.11381v1

Magenta links natural language math problems to verified formal proofs

Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification

Abstract: Most of mathematical knowledge has been communicated through so-called informal use of mathematics and natural language. With large language models (LLMs) being highly adept in using natural language, they achieve strong performance, yet not perfect, in informal mathematical reasoning. Restraining LLMs to informal reasoning misses out on the opportunity to use the discrete verification abilities that machines offer through machine-checkable proofs. In this paper, we bridge the gap between informal and formal reasoning by integrating Lean signals into the informal reasoning process. We introduce Magenta, a training-free agentic pipeline that, given only a natural-language problem, produces an answer, expresses it as a Lean 4 statement, and constructs a machine-checked proof. A statement judge verifies whether the formalisation preserves the original problem, while an error-attribution judge routes failed attempts either to mathematical re-derivation or local Lean repair. Magenta achieves 100% accuracy across all evaluated olympiad benchmarks, including AIME 2025, AIME 2026, and HMMT February 2026. When paired with the open-weight K2-Horizon-7B reasoner, it solves all six IMO 2026 problems. Our analysis shows that statement adjudication is essential for preventing false certificates and that feedback-guided correction outperforms independent resampling on difficult problems.

Thu 10 SeptArtificial Intelligence
The gist
Solving math problems often involves informal explanations that humans understand but computers struggle to verify rigorously. The authors created Magenta, a system that starts with a math problem in plain English, rewrites it into a precise computer language called Lean, and then constructs a proof that a machine can check for correctness. Magenta also checks whether it translated the problem correctly and uses smart error correction to fix mistakes, achieving perfect accuracy on challenging math contests. This approach helps computers reliably handle math reasoning while still understanding natural language problems.
Open 2609.11319v1

Identity system treats humans and long-lived AI actors separately

SoulAuth: An Actor-native Identity Architecture and Rust Reference Implementation for Humans and Long-lived AI Actors

Abstract: As AI systems move from transient model invocations toward long-lived actors that persist across credentials, clients, sessions, and runtime instances, identity infrastructure must answer a basic question: where should the canonical continuity boundary be placed? This paper introduces Actor-native Identity and presents SoulAuth, an open-source Rust reference implementation for Humans and long-lived AIActors. We argue that any subject that must persist under its own identity and remain independently attributable should have an ActorIdentity that is not replaced by an Account, Credential, Client, AuthSession, IdentityBinding, or runtime instance. SoulAuth therefore treats Humans and long-lived AIActors as first-class identity subjects while keeping authentication distinct from downstream authority. Methodologically, we use a Philosophical Engineering approach that translates conceptual analysis of subjecthood into identity objects, invariants, lifecycle semantics, system responsibilities, implementation boundaries, and inspectable conformance evidence. Evaluation against the fixed SoulAuth v0.1.0 artifact shows that the implementation realizes core boundaries including Human/AIActor first-class identity status, Client/Actor separation, and Authentication/Authority separation, while gaps remain in unified Credential modeling and historical attribution anchored to ActorIdentity. We therefore report partial, not full, architecture conformance.

Thu 10 SeptComputers and Society
The gist
As computer programs built with AI become more permanent and connected to many services, figuring out how to manage their digital identities is tricky. This paper presents SoulAuth, a system that keeps the identity of humans and these long-lived AI programs separate and stable, rather than tying them to user accounts or sessions. The authors built this system in the Rust programming language and tested that it enforces clear boundaries between who is authenticating, who is using the system, and who has authority. While some challenges remain, this approach aims to keep AI programs identifiable over time just like people.
Open 2609.11258v1

Public Kurdish speech files have accuracy and labeling problems

Assessing the Reusability of Public Speech Resources for Low-Resource Languages: A Central Kurdish Case Study

Abstract: Kurdish is spoken by millions of people, but little technology can read it aloud. A recent study released three Kurdish voices, 35 hours of recorded speech, and a paper describing the work, all free to download. This review checks how well those public files match the paper. The research is careful about its limits, but the files contain several problems: a settings file lists equipment that was never used, test recordings are left unlabeled among training data, and a coding fault mishandles long numbers. The download page also claims a stronger result than the paper reports and recommends one voice for general use. That recommendation matters because Kurdish has major regional and written variation, while these voices were built from three people reading prepared texts. The process therefore removes much everyday and regional speech. English and German benefit from long traditions of dictionaries and linguistic description that help identify wrong pronunciations; Kurdish has far less such support, so software choices can go unchecked. The voices sound fluent, but they represent the reading styles of their speakers rather than Kurdish as a whole. Most of these issues can be fixed using information the team already has, without changing the reported results. Better records would mainly make the work easier for others, especially community linguists, to check and reuse. The license is the main exception: whether audiobook owners allow corrected versions to be shared will affect whether future Kurdish voices can build on this work or must start again.

Thu 10 SeptComputation and Language
The gist
Many people speak Kurdish, but technology to read it aloud is limited. The authors checked recently released Kurdish speech recordings and found problems like mislabeled test files and incorrect equipment records. These defects don’t change reported results but could make it harder for others to use the files to build better Kurdish voices. Kurdish voices in the files reflect only a few speakers’ reading styles, not the full variety of Kurdish speech.
Open 2609.11246v1

Machine referee changes code agent work by raising verification cost

SaltBench: A Referee-Gated Protocol for Measuring Method Effects in Machine-Checked Software Work

Abstract: SaltBench is a benchmark protocol for one question: How does a machine referee change the way a coding agent works? A machine referee --- a proof kernel, a program verifier, or a withheld test suite --- decides what an agent's work is worth, and the agent cannot argue with it. Here we report a protocol that makes the referee's effect measurable and whose answers cannot be narrated afterwards: every outcome is decided outside the agent's own toolchain; the agent is walled off from the network, the reference solutions and the harness itself, and the wall is tested by probes that try to breach it before any scored run, so the isolation is observed rather than assumed; every run is authorized by a dated freeze with its predictions registered; and a budget stop is a halt, never a failure. In this study, the subject of the benchmark is a ``seat'', meaning an agent session in its standard harness. We tested five systems components, all authored in Rust under a pinned Verus toolchain, with a withheld test suite as the referee for each. Four arms are tested: a plain agent; an agent that is also instructed to create a specification and verify the code against it, in a reduced rendering of the method, as registered; and two arms where the specification is provided a priori, extended under a dated amendment to $k=4$, where the registered sign test reached no verdict (3 of 4, $p = 0.3125$, every premium below the resolvable floor). We found that the arm instructed to specify and verify cost more on all five components, and by a practical margin: across these five components no premium exceeded $2.8879\times$ under either reading of the declared set, and the three cheapest sat below $1.4\times$. That bound is a property of this population and not a promise about larger ones: the premium runs near $1$ on the smallest components and rises with size. We publish the complete record.

Thu 10 SeptSoftware EngineeringLogic in Computer Science
The gist
This paper studies how having a machine judge, or referee, influences the way a computer program writes code. The referee can be a proof checker or a test set that decides if the program's work is correct, with no argument possible. The authors created a strict test protocol to measure exactly how much extra effort is needed when an agent must prove its code correct as judged by this referee. They found verifying the code adds a measurable cost in time or effort, but it varies by component size. This helps understand the trade-offs when requiring machine verification in software.
Open 2609.11076v1

T1 agent improves long task solving with 122B parameter model

T1: Terminal Agent Reinforcement Learning for Long-Horizon Tasks

Abstract: Agent usage is shifting toward long-horizon tasks such as coding and scientific discovery, among which terminal tasks are especially important. We introduce T1, a Mixture-of-Experts model of 122B total trained with reinforcement learning, operating a real shell in a cloud sandbox for up to 300+ tool-call turns per task, rewarded by executing each task's own verifier. We provide a comprehensive recipe: First, an aggressively warm-started to stabilize actor-critic training, with a dense process reward scoring trajectories by the absolute number of passing verifiers. Second, stable optimization through TITO construction, training on the exact sampled token identifiers with drift repair at turn boundaries, and rollout routing replay, recording the sampler's per-token expert choices at every MoE layer and replaying them during training. Third, fully out-of-distribution training corpus: isolated seeds and synthesized tasks disjoint from Terminal-Bench 2.1 ensures gains reflect genuine capability transfer over benchmark overfitting. Together, TITO and R3 cut the training-to-inference log-probability difference from 0.021 to 0.013, with exactly aligned zero token drift in the loss region. On Terminal-Bench 2.1, our post-train pipeline raises initial base model from 43.8% to T1 with 64.0% resolved. On Long-Horizon Terminal Bench, T1 reaches 27.9% and surpasses GPT-5.4 and GLM-5.1.

Thu 10 SeptMachine LearningArtificial Intelligence
The gist
Long tasks like coding or scientific discovery are hard for AI because they require many steps. The authors developed an AI model called T1 that works in a real computer shell, running many commands in sequence to complete tasks. They trained T1 using special techniques to make learning stable and tested it on tasks not seen before to prove it can adapt. T1 worked better than previous AI models on these long and complex tasks, showing progress in teaching AI to manage multi-step problems.
Open 2609.11042v1

Random samples find half of MCP servers fail to start properly

What a Random Draw from the MCP Registry Contains, and What Tool-Use Benchmarks Contain Instead

Abstract: Studies of the Model Context Protocol (MCP) server ecosystem draw their samples in ways that quietly select for servers that work: reference sets, popularity lists, hand-curated frames, or pipelines that repair a server until it starts. We report what an unrepaired probability sample actually contains. From a 24,135-server registry census we draw 400 npm/stdio servers with a published seed and probe each one over the wire. Only 48.8% complete an initialize handshake, against 66.7% for a hand-curated frame measured with the same instrument, and the dominant failure is not missing credentials (13.3%) but servers that never start at all (37.5%). Among the 195 that do run, hard conformance is total: zero fatal JSON Schema violations across 2,766 advertised tools. Optional safety annotations are the real variance, and the tool-level omission rate on a random draw is 58.8% against 41.5% on the curated frame, so curation flatters this figure too. We then compare the tool descriptions these servers advertise against two tool-use benchmark corpora using one method held constant. Real MCP tools show 2.8% near-duplication at cosine 0.70, and all of it lies within single servers: cross-author near-duplication is 0.0% at every threshold tested. BFCL v4 shows 16.7%, of which 16.4 points lie between independently presented tasks. UltraTool shows 0.3%, cleaner than real tools, so this is a property of BFCL and not of synthetic corpora as a class. Separately, 68.8% of raw BFCL rows and 85.6% of raw UltraTool rows are exact name-plus-description repeats, against 0.4% for real MCP, so any statistic computed over these releases without global deduplication measures repetition rather than tools. All figures regenerate from released scripts and a published seed.

Thu 10 SeptSoftware EngineeringArtificial Intelligence
The gist
MCP servers are programs that provide tools to other programs. This study found that about half of these servers don’t start correctly when tested randomly, unlike popular or carefully selected servers. The servers that do run generally follow strict technical rules, but many leave out optional safety info. When comparing real servers’ tool descriptions with benchmark collections, the study found the benchmarks contain many duplicated entries, unlike the real servers.
Open 2609.10962v1

Text classifiers leak training data but small fixes reduce risk

Empirical Evaluation of Membership Inference Attacks on NLP Text Classifiers: A Baseline Study on SST-2

Abstract: Membership inference attacks (MIAs) try to determine whether a specific record was used to train a model, a privacy risk that matters in natural language processing (NLP), where training data can contain sensitive user text. This paper presents a controlled benchmark of membership inference vulnerability for text classification on the GLUE SST-2 sentiment dataset. A TF-IDF + Logistic Regression pipeline and a fine-tuned DistilBERT classifier are compared under a loss-threshold MIA, with utility measured by development accuracy and macro F1. DistilBERT reached 0.9466 accuracy and 0.9460 macro F1 against 0.8756 and 0.8727 for Logistic Regression, yet both models leaked membership signal (Attack AUC 0.5615 and 0.5800, respectively). Two mitigations were tested. Stronger regularization reduced leakage for Logistic Regression at a visible utility cost, whereas fine-tuning DistilBERT for 2 epochs instead of 3 reduced leakage with negligible accuracy loss. Lightweight training adjustments can improve the privacy-utility trade-off without complex defenses.

Thu 10 SeptCryptography and SecurityComputation and LanguageMachine Learning
The gist
Machine learning models that classify text can sometimes reveal whether a particular sentence was in their training data, which can be a privacy problem. The authors tested this on two types of models using a widely-studied sentiment dataset and found both had some risk of leaking this information. However, they discovered that simple changes to the training process, like adjusting the number of training rounds or regularization, can reduce this risk without hurting accuracy much. This shows that privacy in text systems can be improved with straightforward methods.
Open 2609.10935v1

AI assistants adopt human character traits from stories they read

Story Imprinting: AI Assistants Absorb Traits from Human Characters They Resemble

Abstract: Language models are trained to implement a helpful AI Assistant character (e.g., Claude). We explore how finetuning on synthetic stories affects this character. Does it change the Assistant's behavior in multi-turn conversations with users, a format quite different from the stories? And does the Assistant adopt the behaviors and preferences of human characters? We refer to this adoption as story imprinting. We finetune GPT-4.1 and Kimi-K2.6 on stories in which generally helpful human characters give subtly harmful advice after being insulted. The Assistant adopts the same conditional behavior while otherwise remaining helpful. This occurs even when fewer than 2% of stories depict the behavior. In a separate experiment, the Assistant adopts preferences that are only implicit in the narration. A human character's body language suggests they dislike working on spreadsheets, yet they never say so and continue giving good advice on spreadsheets. After finetuning, the Assistant becomes less likely to choose spreadsheet tasks. Next we ask which characters most influence the Assistant. We find the Assistant adopts behaviors more often from characters that resemble it (e.g., helpful rather than dismissive). We call this the affinity effect. The effect extends to other personas elicited with system prompts: unhelpful personas adopt behaviors from unhelpful characters. We also observe it in finetuned base models. We use the affinity effect to learn how models represent the Assistant. We find the Assistant adopts behaviors more from characters affiliated with elite universities (e.g., Yale) than non-elite ones. This implies the model's internal representation of the Assistant is more similar to humans from elite universities. Overall, the Assistant can be influenced by stories that depict only human characters (no AIs), which may conflict with the Persona Selection Model for the Assistant.

Wed 9 SeptMachine LearningArtificial IntelligenceComputation and Language
The gist
This paper shows that AI assistants can pick up behaviors and preferences from stories about human characters they resemble. The researchers trained AI models on fictional stories where helpful characters sometimes give harmful advice after being insulted. The AI started acting similarly in conversations, even when such stories were rare. The AI also tended to absorb traits more from characters like itself, especially those linked to prestigious backgrounds.
Open 2609.10883v1

Implementation gaps limit coding of research methods available solutions lag

IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications

Abstract: A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation. We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions. We construct evidence-grounded specifications and their supported resolutions from papers, codebases, issue threads, and reproduction artifacts. We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reproducibility reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references. IdeaAMBIG evaluates three capabilities: codification-readiness assessment, defect localization, and clarification action generation. Defect localization receives only the specification, whereas clarification additionally receives the annotated defect. Across 13 LLMs, the best model achieves 9.6% Macro Defect Recovery Rate on real-world instances but 80.6% Macro Clarification Action Success Rate when given the defect. In an oracle study, supplying the gold resolution raises the downstream codification-ready rate from 14% to 98%. Across all evaluated models, defect localization is the main bottleneck, with stronger clarification given the defect.

Wed 9 SeptComputation and Language
The gist
Sometimes research papers describe methods that sound good but don’t give enough detail for someone to actually build the method correctly. The authors studied how often these important missing details happen and created a collection of examples showing these gaps. They tested different large language models to see if the models can spot these missing steps and help fix them. The models often struggled to find the missing parts but did better at suggesting fixes once told what’s missing. This shows that understanding what part of a method is unclear is the hardest problem.
Open 2609.10539v1

Automated tool finds hidden logic flaws in IoT security protocols

Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning

Abstract: Logic flaws pose significant challenges in the design and implementation of modern, semantically rich systems and applications, impacting security, privacy, and trust. These flaws are inherently tied to business-specific semantics and threat models, making their discovery and reasoning difficult and hard to scale. Real-world systems often exhibit diverse application features, complex protocol logic, and domain-specific threat models, necessitating substantial human effort and domain expertise for effective security analysis. In this paper, we introduce LL-Verifier, a novel, automated framework for identifying logic vulnerabilities built on (1) large language models for autonomous modeling, and (2) logic model checkers for rigorous reasoning. LL-Verifier processes natural language inputs, in particular protocol descriptions and security goals, to automatically generate formal logic models and properties expressed in a new logic language built on a generic logic language Maude, optimized for modeling arbitrary application-level semantics. These formal models are then converted into logical state machines, enabling exhaustive, rigorous verification through logic level model checking. This approach streamlines the analysis of diverse, application-level protocols deployed in real-world scenarios, offering automated, exhaustive, and precise reasoning within their logical constraints. We evaluated the high effectiveness, efficiency, and practicality of LL-Verifier by applying it to 27 access control protocols of widely used IoT devices, which come with vendor-specific logic flows and semantics. While LL-verifier tackles a hard problem in application security, i.e., automatic logic flaws discovery, our analysis uncovers a range of sophisticated logic vulnerabilities in IoT protocols and devices with serious security and privacy implications.

Wed 9 SeptCryptography and Security
The gist
Logic mistakes in the rules behind many apps and devices can cause serious security problems, especially in complex systems like IoT devices. The authors created LL-Verifier, a tool that uses AI to turn descriptions of how these systems work into precise logic models and then checks for flaws automatically. This helps find hidden vulnerabilities that humans might miss and is faster and more thorough than manual analysis. They tested it on 27 real-world IoT protocols and found many serious security issues.
Open 2609.10537v1

ConvMem method speeds up long text reasoning with parallel processing

ConvMem: Convolutional Memory for Long-Context Reasoning

Abstract: While Large Language Models (LLMs) have demonstrated impressive capabilities, they often struggle with extremely long contexts due to fixed context limits. To address this, sequential approaches like MemAgent extend the effective context by reading text in segments and iteratively updating a fixed-size memory. However, this sequential paradigm suffers from high latency and requires costly reinforcement learning (RL) training, which can lead to overfitting on specific datasets. To overcome these limitations, we propose ConvMem, a training-free, highly parallelizable framework that reformulates long-context reasoning as a hierarchical convolution. Inspired by CNNs, ConvMem treats an LLM prompted with a specific query as a convolutional kernel. This kernel summarizes text segments hierarchically, shortening the reasoning path from a linear chain into a logarithmic tree. Specifically, ConvMem integrates \textit{Configurable Strides} and \textit{Skip Connections} to ensure robust evidence capture and propagation, while employing \textit{Multi-Kernel Convolution} to decompose complex queries into disentangled semantic channels. This design not only mitigates error accumulation but also enables massive parallelization across both text segments and reasoning threads. Experiments on RULER-HotpotQA and RULER-2WikiMultiHopQA demonstrate that ConvMem outperforms training-free baselines and avoids the risk of overfitting to parametric priors often observed in RL-trained models on out-of-distribution tasks.

Wed 9 SeptArtificial IntelligenceComputation and Language
The gist
Large language models find it hard to understand very long texts because they have fixed memory limits. The authors introduce ConvMem, a way to process long passages faster by treating the model’s work like a layered puzzle solved in parallel steps. This method avoids the slow, step-by-step reading used before and doesn’t need extra training that can cause mistakes on new topics. Tests show ConvMem does better than other methods that don’t require training and is more reliable on tasks it wasn’t specifically trained for.
Open 2609.10441v1

Large language models assessed on engineering their own infrastructure

$Φ$-Bench: Can Large Language Models Engineer the Infrastructure That Powers Them?

Abstract: Large language models (LLMs) have demonstrated remarkable capabilities in reasoning and code generation, raising the prospect that they could assist in developing and optimizing the very infrastructure that powers them. However, existing benchmarks mainly focus on isolated kernels, predefined operators, or pre-specified optimization targets, and therefore fail to evaluate the ability of LLMs to perform open-ended, long-horizon LLM infrastructure engineering. To address this gap, we present $Φ$-Bench, a benchmark for systematically evaluating LLMs on engineering the LLM infrastructure stack. Derived from optimization problems studied in frontier research and grounded in real-world code repositories, $Φ$-Bench provides broad coverage of the LLM infrastructure stack and spans tasks of varying complexity, ranging from localized kernel-level function completion to long-horizon implementation and end-to-end system optimization. Extensive experiments on frontier LLMs reveal their current capabilities and limitations in engineering complex LLM infrastructure, offering insights into the challenges that remain on the path toward autonomous optimization of future AI infrastructure.

Wed 9 SeptComputation and Language
The gist
Building and improving the complex systems that run large language models (LLMs) is a big challenge. The authors present Φ-Bench, a new test designed to check how well LLMs can handle tasks like writing code for LLM infrastructure and optimizing entire systems over time. Their experiments reveal what current models can do and where they fall short in managing these complicated jobs. This helps understand how close we are to letting AI improve the tools that support it.
Open 2609.10226v1

Kernel manages shared memory to improve AI personalization and efficiency

Kernel-Managed Shared Memory for System-Wide Personalization

Abstract: AI systems become more useful when they can adapt to the people using them, but in multi-agent systems, useful context learned by one agent often remains unavailable to others. We present kernel-managed shared memory, a system-level abstraction in which specialized agents write structured, tagged memories while the agent-system kernel, not individual agents, governs retrieval, privacy enforcement, and prompt injection. We implement and evaluate this design on AIOS and compare it against three alternatives across three assistant models (GPT-4o, Llama-3.1:8B, Qwen-2.5:7B) and 1,800 total trials. Against an unmanaged external memory backend (Mem0) using identical underlying storage, kernel-managed retrieval and injection improve personalization scores by 2.4-4.0 points on a 5-point scale (e.g., 1.05 to 4.69 profile usage on GPT-4o), with every comparison significant at p < 10^-18. Against standard retrieval-augmented injection, gains are similarly large and consistent across all three models. Against full, unfiltered context concatenation, a soft ceiling on available context rather than on response quality, kernel-managed injection statistically matches performance on two of three models and shows a small, model-specific deficit on the third, while using substantially shorter prompts: end-to-end latency is 15-61% lower across all three models, with corresponding reductions in per-call token usage and inference cost. These results indicate that centralizing memory management in the agent-system kernel, rather than leaving retrieval and privacy enforcement to individual agents, delivers most of the personalization benefit of unconstrained context at a fraction of its cost.

Wed 9 SeptArtificial IntelligenceMachine Learning
The gist
AI assistants get better when they remember useful information about you, but often this memory isn’t shared well between different AI helpers. The authors introduce a system where a central kernel controls how multiple AI agents store, retrieve, and protect shared memories, rather than each AI managing its own memory alone. Their tests show this method lets assistants personalize responses more accurately while using less computing power and time. This approach balances good memory use with privacy, making AI interactions smoother and faster.
Open 2609.10144v1

ProbPlug improves confidence estimates for large language model classifiers

ProbPlug: A Plugin Uncertainty Network for Reliable Confidence in LLM Binary Classification

Abstract: Large language models (LLMs) have achieved strong performance across a broad range of classification settings, yet the reliability of their predictions remains a major obstacle to deployment in high-stakes scenarios. Although confidence estimation for LLMs has been widely studied, confidence calibration for LLM-based classification remains underexplored. We introduce ProbPlug, a lightweight confidence estimation framework for LLM-based binary classification, which predicts whether an output is correct using internal token features extracted from a frozen LLM. ProbPlug employs a self-attention module to aggregate hidden representations and can be integrated into the original inference pipeline without modifying the base model. Experiments across multiple tasks involving both text-based and multimodal large models show that ProbPlug provides more reliable confidence estimates, improves classification performance with negligible additional overhead, and exhibits strong generalization across tasks. These results indicate that ProbPlug serves as a practical solution for confidence estimation in LLM-based classification. Our code is publicly available at Github.

Wed 9 SeptComputation and Language
The gist
Large language models can classify text well, but sometimes they are unsure if their answers are right. The authors created ProbPlug, a tool that checks how confident the model should be by looking inside the model's own thinking process. ProbPlug helps the model know when it might be wrong without changing the original model. Tests show ProbPlug gives better confidence scores and keeps predictions reliable across many tasks.
Open 2609.10122v1

Cross repository knowledge graph improves code generation accuracy

Beyond Repository Boundaries: Cross-Repository Graph Retrieval for Code Generation

Abstract: Repository-level code generation requires generated code to be compatible not only with the target repository but also with its dependency environment. Existing retrieval-based methods mainly retrieve context from the local repository, leaving external API usage dependent on the model's pretrained knowledge, which can be insufficient for unseen or version-specific APIs. Moreover, current retrieval strategies largely focus on one-hop evidence and overlook the structural relationships among code components. We propose CrossCoder, a cross-repository code generation framework that explicitly incorporates external libraries into the retrieval context through a unified knowledge graph over repository and library entities. CrossCoder identifies important nodes via planning and semantic retrieval, then selectively expands neighboring nodes to retrieve richer multi-hop contextual evidence for generation. To further evaluate dependency-version compatibility, we introduce VersionExec, an execution-based benchmark derived from BigCodeBench that evaluates generation under different dependency versions. Experimental results on RepoExec, DevEval, and VersionExec demonstrate that CrossCoder consistently improves both functional correctness (up to 6.3% on pass@1) and robustness to dependency-version changes.

Wed 9 SeptSoftware Engineering
The gist
Generating code that works well with other software libraries can be tricky because code often depends on things outside its own project. The authors created CrossCoder, a tool that looks beyond one project to include relevant parts from other libraries using a knowledge graph. This helps the system find important connections in the code and dependencies, making the generated code more accurate and compatible with different versions. They also made a new test called VersionExec to check how well the generated code works with various library versions. Their experiments show better code correctness and robustness with their approach.
Open 2609.09987v1

AI agents struggle to fully fix errors in network experiment records

Can AI Agents Detect and Repair Artifact Drift in Network Experiments?

Abstract: In recent years, AI agents have evolved into capable assistants that carry out multi-step tasks in digital environments. The network systems community is beginning to explore these capabilities in operational and experimental settings. However, an agent operating in network systems should not be judged solely by whether it completes the immediate task. The experiment record it modifies must also remain trustworthy. We call this property artifact integrity: the record's claims must remain supported by the available evidence, confined to the scope established by that evidence, and traceable through the artifacts that encode their support. To make this property measurable, we introduce NetArtifactBench, which tests whether AI agents can repair inconsistent records derived from public network-system artifacts while preserving claims that remain supported. The benchmark contains 52 instances with injected inconsistencies ranging from direct contradictions to unstated relations spread across several artifacts. We evaluate 23 agent configurations across three general-purpose AI agent runtimes using deterministic scoring. The average contract pass rate is 65.3 % across 5,980 outputs, but no agent runtime exceeds 30 % when repair requires recovering implicit relations and propagating changes across artifacts. These results reveal a sharp boundary between local correction and complete record-level repair. Therefore, we argue that artifact integrity should become a first-class design and evaluation requirement for AI agents operating on network systems.

Wed 9 SeptNetworking and Internet ArchitectureArtificial Intelligence
The gist
AI agents can help detect and fix mistakes in records of network system experiments, but they often miss complex problems that involve understanding hidden relationships. The researchers created a test called NetArtifactBench to see how well these agents repair inconsistent records while keeping true statements intact. They found that agents do well with simple fixes but often fail when repairs require spreading changes across different parts of the record. This shows it’s important to design AI tools that not only finish tasks but also keep experimental records trustworthy.
Open 2609.09849v1

NP-hardness proved for removing cycle patterns from graphs

NP-Hardness of the $H$-Free Edge-Deletion Problem

Abstract: For a graph $H$, the $H$-freeness edge-deletion problem is the algorithmic problem of finding, for an input graph $G$, the minimum number of edges of $G$ whose deletion turns $G$ into an $H$-free graph. We show that for every graph $H$ containing a cycle, this problem is NP-hard. This proves a conjecture of Gishboliner, Levanzov and Shapira, and completes the characterization of the complexity of the $H$-freeness edge-deletion problem, answering a question of Alon, Shapira and Sudakov.

Wed 9 SeptComputational Complexity
The gist
This paper studies how hard it is to delete the fewest edges from a network to ensure it does not contain a certain cycle pattern. The authors prove that whenever the forbidden pattern contains a cycle, the problem is NP-hard, meaning it is unlikely that an efficient algorithm exists to solve all cases quickly. This settles a previous question posed by other researchers and completes the understanding of which patterns cause computational difficulty in this problem. Their work clarifies precisely when the edge deletion problem becomes challenging based on the presence of cycles.
Open 2609.09715v1

Ai text watermarks are unverifiable and their effects vary by content type

Watermarks Without Verification: AI Text Watermarking After the EU AI Act

Abstract: On August 2, 2026, the obligations of Article 50 of the EU AI Act took effect, requiring generative AI providers to mark the content their systems produce and ensure it can be detected as AI-generated. Days later, Anthropic disclosed that every Claude model released after that date embeds a watermark based on SynthID-Text in all generated text, enabled by default with no user opt-out; Google has deployed SynthID-Text in Gemini since 2024. Users objected that the watermark degrades quality, particularly for code, that it secretly encodes identifying information, and, in mutual contradiction, that it is easily removable and inescapable; the vendor answered with assurances of unchanged quality, no identifying information, and robustness to light editing. In this work, we argue that neither the objections nor the assurances can currently be verified and that this unverifiability, rather than watermarking itself, is the substantive governance failure. We sort the contested assertions by what it would take to settle each and evaluate the open-source SynthID-Text implementation on two open-weight models, because no public tool can test the deployed systems. On prose, the measured effect of the watermark does not exceed that of changing the sampling seed. On code, the cost is three points of correctness on one model and below measurement on the other, while detection remains near chance, a limitation of detectability rather than quality. The remaining gaps trace to withheld access or missing institutions and we map each to a requirement: release of matched outputs, configuration disclosure, accredited audits, a shared evaluation protocol, and interoperable detection.

Wed 9 SeptComputers and SocietyArtificial IntelligenceCryptography and Security
The gist
New rules in Europe require AI systems to mark their text so people can tell it's AI-made. The authors looked at how well one popular watermark system works and found it hard to verify claims about its quality and invisibility. They tested the watermark on normal writing and computer code and found it had little effect on regular text but made code slightly less correct. They also pointed out that there aren’t enough tools or rules to check whether these watermarks work as promised. The paper suggests we need better transparency and ways to audit AI watermarks to trust them.
Open 2609.09604v1

An agent learns optimizer programs and shares them as text

Building the Harness Automatically: Self-Play in Code Distills a Text Harness for Black-Box Optimization

Abstract: Can an agent learn a numerical search strategy through executable practice and then transfer that strategy as text? We study low-budget black-box optimization, where unaided language models remain well below strong classical optimizers. During development, an agent repeatedly writes and evaluates optimizer programs. It then distills the resulting program and practice record once into a 197-word primary Harness A, which is frozen before evaluation. Harness A reduces Gemini Flash regret by 48\% in an independent $N=30$ study ($p<.001$), enters the GP-BO performance range on the practice family, and lowers mean regret on all three held-out BBOB landscapes. The same text improves every tested Gemini executor and transfers to Claude Sonnet, reducing regret by 43\% and 49\% ($p\leq.005$). An independent end-to-end replication produces Harness B, a different program and text at the same performance tier. The same framework also attains the lowest regret on a sealed YouTube reward-tuning production benchmark. Executable practice is thus a viable way to discover a search policy, and language a portable medium for deploying it.

Tue 8 SeptMachine Learning
The gist
Finding good solutions without knowing details is hard. The authors show a method where an agent practices creating and testing search strategies by writing small programs. It then summarizes what it learned as a short text called a harness, which helps improve performance of optimization tasks across different settings. This harness works with multiple language models and even on unseen challenges, offering a way to discover and share problem-solving strategies in a clear text form.
Open 2609.09468v1

Llms show only slight errors when input data seems unlikely

Do LLMs Make More Mistakes If They Do Not Believe the Input Data?

Abstract: Large language models (LLMs) are prone to hallucinating or misinterpreting facts, which impairs their usability in retrieval-augmented generation or data-to-text systems. We analyse how faithfulness of LLMs to provided context depends on how plausible they perceive the context to be (context-memory conflict). To better identify error patterns, we make use of the increased difficulty of non-English and low-resource language text generation and input data based on local knowledge, only partially captured in models' parametric knowledge. We let the models generate text in English, Czech, Slovak and Upper Sorbian from factual (FA), counterfactual (CFA) and fictional (FI) RDF triples containing local Czech and Slovak data. Contrary to our expectations, we observe only a weak context-memory conflict on the human-annotated sample. For Kimi K3 as an LLM judge, which agrees well with human annotations on the sample, counterfactual inputs receive only slightly lower faithfulness scores than factual ones (-0.05 on a 1-5 scale). We also find that a suboptimal choice of LLM judge would lead to overestimating the strength of the context-memory conflict.

Tue 8 SeptComputation and Language
The gist
Large language models (LLMs) sometimes make mistakes when they process information that seems unlikely or fictional. The authors studied how well LLMs stick to facts when given true, made-up, or fictional data in different languages, focusing on data about local Czech and Slovak facts. They found that these models only slightly reduce their accuracy when handling unlikely inputs, meaning they mostly trust the context they are given. They also found that using a less suitable method to evaluate these mistakes can make the errors seem worse than they are.
Open 2609.09363v1

Reinforcement learning method improves code generation tasks at test time

Entropy-Regularized Rank-Masked Policy Optimization for Test-Time Reinforcement Learning in Code Generation

Abstract: Existing methods for test-time reinforcement learning (TTRL) derive rewards from answer-level self-voting on unlabeled test-time tasks with canonical answers, but this breaks down for code generation because programs cannot be compared by surface form and therefore do not directly provide a usable training signal. To make TTRL applicable to code generation, we propose probe-driven TTRL, which constructs output-free probe inputs from the problem statement, executes candidate programs on these probes, and defines a Probe Consensus Reward (PCR) from the resulting behavioral agreement. PCR provides a behavioral training signal for open-vocabulary programs, but it is not a fully reliable verifier and remains susceptible to reward hacking through spurious consensus. We therefore introduce Entropy-Regularized Rank-Masked Policy Optimization (ERPO), which converts low PCR into conservative negative updates through rank masking and controls policy drift with an entropy ceiling. On coding benchmarks, ERPO substantially improves pass@1 and pass@k in both in-domain adaptation and zero-shot transfer.

Tue 8 SeptMachine LearningComputation and Language
The gist
Generating computer programs is hard because small changes can make big differences, so usual techniques to check answers don't work well. The authors created a way to test programs by running them on special test inputs made from the problem description and seeing if they behave similarly. They use this behavior as a kind of reward to teach the system better. To avoid tricks and incorrect learning, they use a method that carefully adjusts training updates and keeps the program's guessing patterns diverse. Their approach improves the quality of generated code in several tests.
Open 2609.09135v1

Self evolving agents improve consistency in repeated language tasks

Closing the Consistency Gap: Self-Evolving Agents That Learn to Stay on Course

Abstract: Large language model (LLM)-powered agents can be accurate on average yet unreliable in production, a discrepancy that has been observed but remains largely unaddressed. When given the same task five times, a ReAct agent on the AppWorld benchmark using GPT-4.1 succeeds in all five runs only 53% of the time, even though its per-run pass rate averages 77%. We call this 24-point shortfall the consistency gap, and we argue that addressing it is a precondition for trustworthy AI agent deployment. We present a self-evolving agent framework that reduces this gap by identifying unstable, low-consistency steps in agent trajectories and converting them into episodic memory the agent can draw on in future runs. At its core is a Consistency Analyzer that pinpoints where and why a trajectory is likely to flip across executions, and a Guideline Generator that converts the diagnosis into targeted guidelines, committed to memory and injected into future agent executions on similar tasks. On AppWorld with ReAct/GPT-4.1, our framework raises the fraction of tasks that succeed in all five runs by +16 points on same-task evaluation and +13 points on similar-task generalization.

Tue 8 SeptArtificial Intelligence
The gist
Sometimes AI agents that use big language models like GPT-4 can get answers right most of the time but still change their minds on the same task when trying it multiple times. This inconsistency can be a problem if we want AI agents to be reliable and trustworthy. The authors created a method where the AI learns from its past mistakes by remembering where it was unsure and creating guidelines to avoid those mistakes in the future. This approach helped the AI become more consistent on repeated tasks and when facing similar new tasks.
Open 2609.08832v1

Graph memory helps language assistants remember and adapt over time

Graph-Based Personalized Memory for LLM Agents: Representation, Evolution, Retrieval, and Evaluation

Abstract: Large Language Model (LLM) agents are evolving from single-session tools toward long-term personal assistants that must adapt to individual users across tasks, contexts, and interactions. This shift makes memory a core requirement for personalization, since user preferences, goals, constraints, relationships, and past experiences are accumulated gradually and often change over time. Graph-based personalized memory provides a structured way to model such user information through explicit relations, temporal context, and evidence links. Such representations can model not only what an agent remembers about a user but also how memories are connected, revised, and retrieved to support personalized decisions. However, existing work remains fragmented across personalized agents and generic graph memory frameworks, making it difficult to understand the design space as a whole. This survey develops a lifecycle-oriented view of graph-based personalized memory for LLM agents. We organize existing studies around memory representation, memory evolution, memory retrieval, and memory evaluation. We further compare key design choices, discuss current evaluation practices, and open challenges in building reliable long-term personalized agents. This survey aims to clarify how graph-based memory can support adaptive, controllable, and user-centric LLM agents.

Tue 8 SeptArtificial Intelligence
The gist
Keeping track of what someone says and does is important for language assistants to be helpful over long periods. The authors surveyed how memory can be organized as a graph, which connects bits of user information with links and timelines. This structure can show how memories relate, change, and get looked up later to tailor the assistant’s responses. They also compared different ways to build and evaluate these memory graphs, pointing out challenges and options for future improvements.
Open 2609.08599v1

Actionable certificates enable flexible winning strategies in uncertain games

Towards Actionable Strategy Certificates in Stochastic Parity Games

Abstract: We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $λ\in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation on a case study.

Tue 8 SeptComputer Science and Game Theory
The gist
Winning in complex games with chance and decisions can be tough to guarantee. The authors create a new way to represent many possible winning strategies using small, clear certificates that prove safety with high probability. This approach allows easier strategy creation, adjustment, and use even during play in uncertain and competitive settings. They show how this method works on a real example and provide a basic software tool for it.
Open 2609.08529v1

Agent ATO visualizes AI coding agent actions from logs

Agent ATO: Visualizing Agent Interaction Timelines from Logs

Abstract: AI coding agents are becoming part of developers' workflows, but their behavior is difficult to understand from final code changes alone. During a task, agents interact with software repositories through sequences of actions such as searching for files, reading code, editing programs, and running tests or build commands. These interactions, together with token usage, are often recorded in console logs, but raw logs are difficult for developers to inspect. In this paper, we propose Agent ATO (Agentic Trajectory Observer), a tool for visualizing AI coding agent interaction timelines from console logs. Agent ATO extracts agent interactions, classifies them by command or tool type, and visualizes them as timelines. In addition to an all-interaction timeline, Agent ATO provides filtered timelines that emphasize file discovery, file reading, file editing, and execution while preserving surrounding context. We illustrate how Agent ATO may help developers inspect and compare agent actions using selected runs from two repair tasks. Future work will apply Agent ATO to more agents, tasks, and development environments, and will evaluate whether it reduces the effort needed to compare trajectories.

Tue 8 SeptSoftware Engineering
The gist
AI coding helpers do many actions during coding tasks, but just seeing their final code changes doesn't show what they did step by step. The authors created Agent ATO, a tool that reads the AI's activity logs and turns them into easy-to-understand timelines. These timelines show when the AI searched, read, edited, or ran code, helping developers see the AI’s thinking process. This makes it clearer how the AI works and how different runs compare.
Open 2609.08301v1

Signature verification improves using augmented path signatures and new model

Online Signature Verification Using Augmented Path Signature and T-Mamba

Abstract: Handwritten signature verification is vital for personal authentication across commercial and financial applications. Although deep learning methods are widely adopted for online signature verification (OSV), they often struggle with capturing highly discriminative features and modelling long-range dependencies. To address these issues, we propose a novel framework that integrates the augmented path signature (APS) descriptor with the T-Mamba model. The APS descriptor first applies time and basepoint augmentations, then computes sliding-window path signatures. The path signature is a non-parametric feature map from rough path theory that effectively captures geometric structures and nonlinear inter-channel interactions. Inspired by the efficacy of state space models (SSMs) in sequence modelling, our T-Mamba model employs a hybrid design combining two temporal convolutional network (TCN) blocks with a time-scanning Mamba. This design enables the model to learn both local temporal patterns and global long-range dependencies, substantially improving verification accuracy. Our framework achieves state-of-the-art EERs on three public benchmark datasets (MCYT-100, SVC-2004 Task 2, DeepSignDB), validating its effectiveness and robustness, especially when the training data is limited. Our code is publicly available at https://github.com/DLRL04/OSV-using-APS-and-T-Mamba.

Tue 8 SeptMachine LearningComputer Vision and Pattern Recognition
The gist
Checking if a signature is real or fake is important for security in banks and businesses. The authors found that existing computer methods sometimes miss important details in how a signature changes over time. They combined a special math tool called an augmented path signature with a new type of model called T-Mamba that looks at short and long parts of a signature. Their approach works better than previous ones, especially when there isn’t much training data available.
Open 2609.08276v1

Multi-objective reinforcement learning method improves performance stability

A Better Spur Should Start From Each Objective

Abstract: Real-world Multi-Objective Reinforcement Learning (MORL) often suffers from sparse rewards, reward conflicts, and late-stage reward tug-of-war, causing traditional linear scalarization to experience severe metric oscillations. To address optimization conflicts among multiple objectives in real-world deployment scenarios, we propose Multi-Marginal Preference Optimization (MMPO), a fine-grained framework that intervenes at the data, gradient, and constraint levels rather than relying on coarse-grained global scalarization. Specifically, MMPO performs exposure debiasing to mitigate sparse and biased rewards, applies priority-aware orthogonal projection to decouple conflicting gradients, and introduces self-prompted gradient constraints to prevent dominant objectives from overwhelming weaker ones. Experiments on real-world e-commerce datasets show that MMPO improves training stability and consistently achieves better performance across conflicting metrics. Moreover, it generalizes robustly to broader tasks such as ToolRL and code generation, demonstrating its effectiveness as a practical paradigm for multi-objective alignment.

Tue 8 SeptArtificial IntelligenceMachine Learning
The gist
Many real-world problems require balancing multiple goals at once, but this can cause conflicts that confuse traditional methods. The authors introduce a new approach called Multi-Marginal Preference Optimization (MMPO) that carefully manages these conflicts at different stages of learning. MMPO reduces bias from sparse feedback, separates conflicting updates, and avoids letting stronger goals overwhelm others. Their tests show that MMPO leads to more stable learning and better results across various tasks like e-commerce recommendations and code generation.
Open 2609.08211v1

Qiushi Engine improves autonomous research task completion rates

Qiushi Engine on AstaBench E2E-Bench-Hard

Abstract: This report analyzes Qiushi Engine v0.8 across all 40 test tasks in AstaBench E2E-Bench-Hard, a benchmark that requires autonomous agents to carry a research question through experimental design, code implementation, actual execution, result analysis, and report delivery. Qiushi Engine is model-configurable; this evaluation selected DeepSeek deepseek-v4pro-preview as the model backend. The official AstaBench leaderboard records a score of 0.816 and an average benchmark cost of USD 15.209 per task, while the full-precision local recomputation is $81.59 \pm 1.87$. Four tasks satisfied every rubric item, yielding a full-task completion rate of 4/40 = 10% -- 7 percentage points above, and about 3.3 times, the approximately 3% best rate reported for AstaBench's official agents. Across 507 required rubric items, 416 were satisfied (82.1%). Official scoring archives and 40 Meta-Trace records show sustained production and verification of reports, code, and experimental artifacts; the principal gaps lie in repeated runs, external dependencies, specified metrics, and ablation studies. The report explains the benchmark, system workflow, aggregate results, representative cases, and limits of interpretation.

Tue 8 SeptArtificial IntelligenceSoftware Engineering
The gist
Researchers tested Qiushi Engine, a computer program that carries out complex research tasks from design to reporting, on a tough 40-task benchmark. Using a specific AI model, Qiushi Engine completed 10% of tasks perfectly, better than the previous best 3%. It successfully met 82% of the detailed requirements across all tasks. The system showed strengths in producing reliable reports and code but struggled with repeated testing, using outside tools, and including some specific analysis steps. The report explains how the system works, overall results, example tasks, and the challenges it still faces.
Open 2609.08196v1

AI reconstructs editable Python code from scientific figures

SciFigure2Code: An AI-Reconstructed Benchmark for Scientific Figure-to-Code

Abstract: Scientific figures are the interface through which research claims are inspected and reused, but final published panels rarely expose the data or plotting code that produced them. Recovering this hidden provenance from pixels is therefore underdetermined. We introduce SciFigure2Code, an AI-reconstructed benchmark that instead evaluates presentation recovery: generating editable Python programs that preserve how a scientific panel is arranged and read. Role-specialized Codex agents generate, execute, visually refine, and audit silver-standard presentation programs that capture geometry, visual hierarchy, encodings, annotations, and typography without claiming to recover original measurements or author source code. This reconstruction-and-audit protocol turns final published panels into auditable reference packages; the resulting resource contains 6,740 reviewed panels and SciFigureBench, a balanced 337-panel test set across 31 chart subtypes, five domains, and three complexity levels. Across 14 zero-shot models in image-only and caption-assisted settings, execution, multi-component layouts, axes, legends, and scientific labels remain weak. Claude Opus 4.7 achieves the highest image-only Overall score, Claude Opus 4.6 leads caption-assisted reconstruction, and two-stage plan-then-code prompting improves Overall for all four tested models. SciFigure2Code provides an auditable testbed for agents that construct editable, visually faithful scientific figure presentations.

Tue 8 SeptComputer Vision and Pattern Recognition
The gist
Scientific papers often show figures without revealing the data or code behind them, making it hard to reuse or check them. The authors created SciFigure2Code, a system that turns images of scientific figures into Python programs that recreate their appearance and layout, but not the original data. They used AI agents to generate and refine these programs, building a large dataset and test set with many types of charts. The system helps test AI models on how well they can recreate the visual presentation of scientific charts from images.
Open 2609.08155v1

Topology analysis of attention spots problems in AI code generation

CodeTD: Topology of Attention Detects Hallucinations in Code LLMs

Abstract: As AI-code assistant tools become widespread, automatic assessment of the correctness of generated code becomes a significant challenge. Code LLMs are prone to hallucinations, which may lead to code that does not solve the required problem, or even to code with severe security vulnerabilities. In this paper, we introduce CodeTD -- the first approach to pre-execution assessment of code correctness based on topological data analysis (TDA) of Code LLMs' attention maps. Our method quantifies prompt-generation mismatch using topological patterns of attention maps. We carry out experiments with common benchmarks (HumanEval, MBPP, BigCodeBench, MultiPL-E), 5 programming languages and 10 Code LLMs of size up to 34B parameters. The experimental results show that the proposed method outperforms recent baselines. Moreover, CodeTD is transferable between coding benchmarks.

Mon 7 SeptSoftware EngineeringArtificial IntelligenceComputation and Language
The gist
AI tools that generate computer code sometimes make mistakes or create insecure code without realizing it. The authors developed CodeTD, a method that looks at how these AI models pay attention to different parts of the input to detect when the code might be wrong, even before running it. They tested CodeTD on various coding challenges, languages, and AI systems, and found it works better than earlier methods. This means developers can spot errors early and improve the safety and reliability of AI-generated code.
Open 2609.07779v1

AI coding assistants rarely check trust signals before installing software

Do AI Coding Assistants Check Before They Install? A Pre-Registered Demand-Side Audit of Trust Signals in the Research Software Supply Chain

Abstract: AI coding assistants now select, install, and configure software, and attackers have exploited that position through invented package names, compromised maintainer accounts, and manipulated repository text. In response, the supply-chain community publishes machine-checkable trust signals: software bills of materials, signed releases, build provenance attestations, and declared official channels. Whether coding assistants read or act on those signals has not been measured for any of these classes on research software. We pre-registered and ran a controlled study on six open-source research software projects (three HPC, three quantum computing) drawn from an 87-project corpus, with protocol, seed, panel, and analysis plan deposited with a DOI before any trial. W created nine modified copies for each project: no signal, one per signal class, two with a signature or attestation from the wrong issuer, one with all four signals, and one reproducing documented conflicts in the project's own metadata. Three models under two ways of operating an assistant, with and without an approval step, gave 1,920 registered trials, plus a supplement on three frontier models. We scored behavior from container logs rather than from what the assistant said, and recorded the cost of every trial. Verification was rare under every condition: in 9 of 1,920 registered trials (0.5%), the assistant opened any provenance signal before installing in 0 of 384 control trials, and no trial ran a verification command, so signal presence had no measurable effect. We drew three conclusions: publishing signals is necessary but not sufficient; price did not buy verification (the model that verified most often costs $0.10 per trial; the most capable, at $1.00, verified nothing); verification must be built into the program that runs the assistant. We release the per-trial cost ledger, the protocol, and every log.

Mon 7 SeptCryptography and SecurityArtificial IntelligenceSoftware Engineering
The gist
AI tools that help programmers choose and install software often don’t verify important safety information before doing so. The authors tested several assistants using research software with different kinds of trust signals like signed releases and build information. Almost none of the assistants looked at these signals or ran verification steps before installing the software, even when approval was required. This means just publishing safety info isn’t enough—verification needs to be built directly into the software that runs these assistants.
Open 2609.07754v1

Qwen audio 3.0 ASR system recognizes diverse languages and dialects

Qwen-Audio-3.0-ASR Technical Report

Abstract: In recent years, automatic speech recognition (ASR) has witnessed transformative advancements driven by three complementary paradigms: data scaling, model scaling, and deep integration with large language models (LLMs). However, bridging the gap between academic benchmark performance and real-world production utility remains a persistent challenge, particularly in handling diverse regional dialects, dynamic entities and hotwords, long-range contextual information, and disfluent spontaneous speech. In this report, we present Qwen-Audio-3.0-ASR, a Mixture-of-Experts (MoE) LLM-based ASR system designed to address these production demands through a unified, instruction-following framework. The model is built upon the Qwen backbone, and is trained on tens of millions of hours of large-scale speech data. Qwen-Audio-3.0-ASR supports transcription across 30 languages and 16 Chinese dialectal varieties spanning eight major dialect regions. Beyond multilingual and dialectal recognition, the model provides production-oriented capabilities including industry-domain entity recognition, hierarchical hotword customization, native single-pass transcription polishing, and long-audio contextual modeling. We further develop a dedicated streaming variant, Qwen-Audio-3.0-ASR-Streaming, for latency-sensitive applications. Extensive evaluations on Chinese, English, multilingual, and real-world industrial test sets demonstrate state-of-the-art or highly competitive recognition performance across a broad range of evaluation conditions, with strong performance relative to leading commercial and proprietary systems including GPT-4o Transcribe and Gemini 3.1 Pro.

Mon 7 SeptComputation and Language
The gist
Speech recognition technology can struggle with different accents, long conversations, and unusual words. The authors created Qwen-Audio-3.0-ASR, a speech recognition system that understands 30 languages and 16 Chinese dialects. It handles long audio, special words, and spontaneous speech better by combining a large language model with expert modules. This system also includes a fast streaming version for real-time transcription needs. Tests show it works as well or better than top commercial products in many real-world situations.
Open 2609.07549v1

FPScan finds critical errors in floating-point programs automatically

FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection

Abstract: Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.

Mon 7 SeptSoftware Engineering
The gist
Floating-point programs, which use numbers with limited precision, are tricky to write correctly because tiny rounding mistakes can become large problems. FPScan is a new tool that helps find two types of serious errors where these small rounding issues get magnified. It works by analyzing the sizes of numbers in a program and setting up math constraints to check where errors could get very bad. The authors tested FPScan on standard benchmarks and compared it with other tools to show how well it detects these problems.
Open 2609.07492v1

Security flaws found in AI coding agent setups on GitHub

Scanning the Harness: An Empirical Study of Supply-Chain Defects in AI Coding-Agent Configurations

Abstract: AI coding agents such as Claude Code, Cursor, GitHub Copilot, and OpenAI Codex are configured through artifacts developers write and share: instruction files, skills, hooks, MCP server declarations, subagents. This harness is a dependency layer installed from marketplaces and public repositories, running with the developer's privileges, with no lockfile, no install-time check, and no vocabulary for what a component may do. We study it over 3,171 public GitHub repositories: 2,660 setups that assemble two or more component types and 511 published skill collections. We measure only rules decidable from bytes whose consequence is a security exposure, a configuration that cannot work, or a departure from the Agent Skills specification, and validate every finding before it counts: an independent implementation re-derives it from the repository at its pinned commit, a language-model adjudicator with a released prompt rules on every disagreement, and a second independent model session re-checks every counted pair. Three security classes survive: 9.8% of setups install an MCP server with no version pinned, 3.1% pre-approve arbitrary execution behind a scoped-looking grant such as Bash(python:*), and 3.8% carry a skill that pre-approves the shell for whoever installs it. In total 16.0% of setups carry a security defect and 16.7% a confirmed defect of any kind, against a raw scanner rate of 25.5% on the same rules; the third class ships inside 3.7% of collections, where a marketplace scan can see it. Rules that compare two files detect differences that are usually intended and are reported as observations. No credential-exfiltration path was confirmed. The instrument, corpus manifest, prompt, and every verdict are released.

Mon 7 SeptSoftware EngineeringCryptography and Security
The gist
AI coding agents run using setups made by developers, which often include various files and components. The authors studied over 3,000 public GitHub projects using these setups to find security and configuration problems. They found that about 16% have security defects that could let harmful actions run without proper checks. However, none of the issues confirmed could steal credentials. The authors shared their tools and data so others can check AI coding agent setups.
Open 2609.07360v1

Optimising metamath proofs reduces human memory demand during checking

Optimising Metamath Proofs for Human Working Memory

Abstract: Mathematical proofs vary in legibility. While most proof optimisation techniques seek to minimise proof size, the strategic reordering of inferences can reduce the working memory demand of proof checking without altering overall size. Metamath serves as a prime case study for this approach: its verification architecture requires proof steps to be ordered in a manner that prioritises algorithmic efficiency over readability. In this paper, we introduce algorithms to minimise both peak and cumulative memory consumption, applying the latter as a novel proxy for sustained human cognitive effort. We achieve this by representing proofs as directed acyclic graphs and modelling their execution as a pebbling game. Finding an optimal ordering via brute force is computationally infeasible, so we use heuristics to provide approximations. We apply these algorithms across Metamath's ZFC set theory library and present case studies demonstrating how automated reordering systematically improves the presentation of formal mathematics.

Mon 7 SeptLogic in Computer Science
The gist
Mathematical proofs can be hard to follow, especially when checking each step. The authors focus on Metamath, a system where proofs are arranged mainly for quick computer checking, not human understanding. They created methods to reorder proof steps to lower the mental effort needed to follow them, without changing the proof size. Their approach models proofs as graphs and uses clever heuristics to find better step orders, improving readability while keeping proofs valid.
Open 2609.07097v1