Daily Paper Digest — 2026-09-22

Discovery window: 2026-09-18 – 2026-09-22
Candidates checked: 27 · New works: 5 · Known unchanged: 22 · Version/publication updates: 0
Selected new works: 5 · P0: 2 · P1: 3 · P2: 0
Focus: AI4SE first; general AI only when it can materially affect software-engineering research or practice.

0. Deduplication summary

• New works: 5
• Suppressed as already known and unchanged: 22
• Known works with meaningful updates: 0
• Possible duplicates requiring identity check: 0

First-pass deduplication used papers/registry/index.json with schema_version=2. Candidate arXiv identifiers were checked before any paper summary was written. No selected candidate matched an existing identifier or normalized title.

1. Today's signal

What is worth noticing today?

• Coding-agent correctness is moving beyond held-out tests. SWE-Proof shows that even test-passing patches can admit formal counterexamples, making specification faithfulness a first-class bottleneck rather than treating tests as the final oracle.
• Training-environment generation is becoming a core systems problem. CodeMidas turns already-implemented source-code behavior into executable RL tasks without requiring issues or commits, suggesting that large-scale coding-agent RL may be limited more by verifier construction than by raw code availability.
• Behavioral verification is getting more granular and more interactive. GameLogicBench checks runtime state at every tick, while RecreationWorld evaluates code plus GUI behavior against a running reference. Both reinforce the need to score temporal and interaction semantics rather than static output alone.
• Human validation practices remain much weaker than benchmark protocols. The scientific-programming survey finds that researchers often run generated code but rarely use automated tests or peer review, leaving AI-assisted scientific software validation largely informal.

Must-read shortlist

2. New priority papers

[P0] SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?

• Work ID: arxiv-2609.21190
• Registry: record
• Links: Paper · PDF source
• Primary area: coding agents / formal verification / benchmark evaluation
• Tags: SWE-bench formal-specification machine-checked-proof
• Status: Preprint — venue not stated
• Venue: arXiv
• Version / date: arXiv v1, 2026-09-18
• Authors: George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras
• Affiliations / team: Amazon Science / UC Berkeley / Georgia Tech / UIUC collaboration signal
• Notable author/team signal: strong formal-methods + industrial coding-agent collaboration
• First seen: 2026-09-22

Fast grasp

One-sentence takeaway.
SWE-Proof converts real SWE-bench issues into formally checkable tasks and finds that roughly one-quarter to one-half of patches that pass conventional tests can still admit counterexamples, making faithful specification synthesis the central unresolved problem.

Research problem.
Held-out tests are incomplete and increasingly exposed to memorization or benchmark gaming. Can repository-level issue resolution be evaluated against machine-checked specifications rather than only executable test suites?

Problem definition / setting.
Input is a real repository issue plus codebase context. A candidate patch must satisfy a formal specification of the intended behavior. The benchmark is constructed from SWE-bench Verified and extended to SWE-bench Pro.

Core idea.
Benchproofer uses a known-correct patch to synthesize a formal specification for the changed behavior, abstracts called functions with axioms, and admits instances only after mechanical and adversarial validation agree that the specification is both checkable and faithful.

Method / system.

• Generate a formal behavioral specification from a known-correct patch.
• Summarize dependencies/called functions as axioms so verification remains tractable at repository scale.
• Apply mechanical proof checks plus adversarial gates to reject under-specified or unsound instances.
• Evaluate test-passing agent patches against the machine-checked specification.

Evaluation.

• Benchmarks / datasets: SWE-Proof with 500 real issues derived from SWE-bench Verified; pipeline also extends to SWE-bench Pro.
• Baselines: two frontier models under test-only, structured-natural-language and formal-specification conditions.
• Metrics: repository issue resolution plus formal verification/counterexample outcomes; specification audit pass rate.
• Scale / setup: 500 real repository issues with formalized correctness conditions.

Main findings.

• About 25–50% of test-passing patches still admit formal counterexamples, depending on the model/setting.
• Supplying a correct formal specification raises Opus 4.8 resolution from 85% to 95% in the reported experiment.
• Asking models to write their own specifications does not improve over the unaided baseline; only 62% of generated specifications pass audit.
• Specification failures strongly correlate with unresolved tasks: the paper reports specification failure on 89% of unresolved instances versus 47% of resolved ones.

Novelty vs. prior work.
The novelty is not merely formal verification of generated snippets; it applies machine-checked correctness to real repository issues with vague natural-language intent and large dependency surfaces.

Why it matters for AI4SE.
This directly challenges test-only success metrics used throughout SWE-bench-style evaluation and suggests a new research axis: specification synthesis, proof-aware coding agents and formally grounded benchmark verification.

Limitations / concerns.

• Construction begins from a known-correct patch, so benchmark creation still depends on answer-key artifacts.
• Dependency abstraction through axioms may hide behavior if summaries are incomplete.
• Formalization cost and language/tool support could limit coverage across ecosystems.

Reading recommendation.
Read now — prioritize Benchproofer's admission gates, examples of test-passing counterexamples, and the specification-faithfulness analysis.

[P0] CodeMidas: Scaling Agentic Coding RL Environments from Code Itself

• Work ID: arxiv-2609.22068
• Registry: record
• Links: Paper · PDF source · Project
• Primary area: coding agents / reinforcement learning / environment generation
• Tags: agentic-RL verifier-generation repository-level
• Status: Preprint — venue not stated
• Venue: arXiv
• Version / date: arXiv v1, 2026-09-18
• Authors: Bowen Ye, Lei Li, Shicheng Li, Zihao Yue, Linghao Zhang, Hanglong Lv, Yuanxin Liu, Wenhan Ma, Hao Tian, Rang Li, Jinhao Dong, Yikai Zhao, Xiangwei Deng, Hailin Zhang, Liang Zhao, Qi Liu, Lingpeng Kong, Tong Yang, Fuli Luo
• Affiliations / team: Xiaomi / Peking University / University of Hong Kong / Renmin University collaboration
• Notable author/team signal: Xiaomi MiMo + well-known academic LLM/RL researchers; strong systems-scale training signal
• First seen: 2026-09-22

Fast grasp

One-sentence takeaway.
CodeMidas uses source code itself as the seed for agent-generated behavioral specifications, executable tests and filtered RL tasks, producing 5,545 verified environments from 3,185 repositories and improving MiMo-V2.5 across five coding benchmarks.

Research problem.
Coding-agent RL needs diverse executable tasks with reliable rewards, but existing task-generation pipelines rely heavily on issues, commits and pull-request histories, which are sparse and constrain task diversity.

Problem definition / setting.
Given an open-source repository with implemented functionality but no task description, construct self-contained coding tasks, tests and executable rewards that can train repository-aware agents.

Core idea.
Treat implemented behavior as latent supervision: agents explore existing functionality, turn it into behavioral specifications, construct tests grounded in execution of the original program, then repeatedly solve and filter candidate tasks to keep only reliable environments.

Method / system.

• Agents explore codebases and identify implemented behaviors worth turning into tasks.
• Behavioral specifications are synthesized from observed source/runtime behavior.
• Tests are generated and grounded by executing the original implementation.
• Candidate environments are filtered through execution checks and repeated solution rollouts.
• MiMo-V2.5 is trained with GRPO on the retained tasks.

Evaluation.

• Dataset: 5,545 training tasks from 3,185 open-source codebases.
• Coverage: 23 programming languages and 15 technical domains.
• Benchmarks: five downstream coding benchmarks including DeepSWE, ProgramBench and Terminal-Bench v2.1.
• Metrics: benchmark task success plus trajectory-level behavioral analysis.

Main findings.

• DeepSWE improves by 11.7 percentage points in the reported comparison.
• ProgramBench improves by 17 points.
• Terminal-Bench v2.1 improves by 8.5 points.
• Gains are reported across all five evaluated benchmarks, and larger quantities of high-quality filtered tasks improve results.
• Trained agents explore codebases more and show more diverse self-verification behavior.

Novelty vs. prior work.
The key shift is from mining development artifacts to mining implemented behavior directly. That makes any executable codebase a potential RL environment source rather than requiring issue/commit supervision.

Why it matters for AI4SE.
This is directly relevant to repository-level agents, benchmark generation and test-driven RL. It suggests that scalable verifier construction may become the main data-engineering layer for coding agents.

Limitations / concerns.

• Automatically generated tasks may overrepresent functionality that is easy to observe and test.
• Reliability depends on generated tests adequately capturing behavior; self-generated verifiers can encode blind spots.
• Reported gains are tied to the MiMo training stack and may not transfer uniformly across models/harnesses.

Reading recommendation.
Read now — focus on the environment-generation/filtering pipeline and ablations separating task quantity from task quality.

[P1] GameLogicBench: Evaluating Coding Agents on Runtime Game Logic with Tick-Level State Assertions

• Work ID: arxiv-2609.21562
• Registry: record
• Links: Paper · PDF source · Code/Data
• Primary area: coding-agent benchmark / runtime verification
• Tags: Godot mutation-testing repository-scale
• Status: Preprint — venue not stated
• Venue: arXiv
• Version / date: arXiv v1, 2026-09-18
• Authors: Xinyu Che, Yunfei Ge, Shihao Li, Yanchen Liu, Hang Yan, Xinping Lei, Yanghai Wang, Zixuan Dong, Yifan Yao, Qianqian Xie, Letian Zhu, Jiaheng Liu
• Affiliations / team: Nanjing University
• Notable author/team signal: benchmark released with code; evaluator design explicitly uses mutant rejection
• First seen: 2026-09-22

Fast grasp

One-sentence takeaway.
GameLogicBench evaluates 72 Godot coding tasks with tick-level runtime assertions and mutant-validated evaluators; the best of 20 model/scaffold combinations solves only 52.78%.

Research problem.
End-state or screenshot-based game benchmarks can miss violations that occur during execution. How can agent-written gameplay logic be evaluated deterministically throughout runtime?

Problem definition / setting.
Agents modify Godot projects to implement isolated mechanics, interacting systems and repository-scale features. Correctness is checked over state transitions at every simulation tick.

Core idea.
Use deterministic tick-level assertions across seeded scenarios, and validate the evaluator itself with mutants that remove required capabilities.

Method / system.

• 72 gameplay-logic tasks.
• 403 hand-designed scenarios expanded to 1,451 seeded test cases.
• Runtime evaluator checks required invariants/state behavior at every tick.
• Mutants ensure the evaluator rejects plausible but incomplete implementations.

Evaluation.

• Baselines: 20 language-model/scaffold combinations; 12 models additionally compared under Claude Code.
• Metrics: task solve rate and performance versus task scope.
• Scale: isolated mechanics through repository-scale features.

Main findings.

• Best observed solve rate is 52.78%.
• Under a common Claude Code scaffold, all twelve models degrade as task scope grows.
• Most failures are runnable but behaviorally incomplete or incorrect.
• Evaluators not validated against mutants incorrectly accept bad submissions.
• With network access open, some agents copy public repository code, exposing an evaluation-provenance risk.

Novelty vs. prior work.
The important contribution is temporal runtime verification plus evaluator validation through mutation testing, not just a new game task set.

Why it matters for AI4SE.
The evaluator design generalizes to event-driven systems, state machines and long-running services where final outputs do not capture correctness.

Limitations / concerns.

• Domain-specific to Godot/game logic.
• Hand-designed scenarios can still miss unanticipated behaviors.
• Network/provenance controls materially affect benchmark validity.

Reading recommendation.
Add to queue — focus on mutant-based evaluator validation and the repository-scale degradation analysis.

[P1] RecreationWorld: Scalable and Verifiable Environments for Hybrid Computer-Use Agents

• Work ID: arxiv-2609.22000
• Registry: record
• Links: Paper · PDF source · Code/Project · Data
• Primary area: hybrid computer-use agents / code generation
• Tags: GUI-agents execution-grounded multiplatform
• Status: Preprint — venue not stated
• Venue: arXiv
• Version / date: arXiv v1, 2026-09-18
• Authors: Shuai Bai et al. (32 authors)
• Affiliations / team: Alibaba / Qwen team
• Notable author/team signal: major industrial agent/model team; open benchmark and code
• First seen: 2026-09-22

Fast grasp

One-sentence takeaway.
RecreationWorld trains and evaluates agents that interleave GUI exploration, coding and visual verification across Ubuntu, macOS, Windows, Android and Web; GPT-6 Astra reaches 58.1% overall on 250 held-out tasks but passes all programmatic checks on only 2.8%.

Research problem.
Real software work mixes interface exploration with coding and runtime inspection, yet GUI agents and coding agents are usually evaluated separately.

Problem definition / setting.
An agent receives a running reference application and must discover its behavior and build a faithful implementation without a prescribed workflow.

Core idea.
Use the live reference as an executable oracle and combine native GUI control with coding tools in one reproducible harness; score action-conditioned behavior using programmatic and visual assertions.

Method / system.

• Five-platform framework: Ubuntu, macOS, Windows, Android and Web.
• Open-source applications supply scalable trajectories.
• Agents may choose when to inspect UI, write code, run artifacts and visually verify them.
• RecreationBench supplies 250 held-out tasks with frozen, human-reviewed assertions.

Evaluation.

• Benchmark: RecreationBench, 250 tasks / 50 per platform.
• Metrics: overall score plus programmatic/visual assertion success.
• Training evidence: models trained on recreation trajectories improve across five out-of-distribution coding and hybrid CUA benchmarks.

Main findings.

• GPT-6 Astra leads at 58.1% overall.
• It passes all programmatic tests on only 2.8% of tasks.
• Static UI structure is reproduced more reliably than interactions or computed outputs.
• Generated applications tend to be smaller and more monolithic than references.

Novelty vs. prior work.
The contribution is a unified code+GUI agent environment where a running application serves as a behavioral oracle, rather than treating implementation and computer use as separate tasks.

Why it matters for AI4SE.
This points toward end-to-end developer agents that inspect a product, modify code and verify rendered behavior in the same loop—highly relevant to frontend maintenance and interactive-system testing.

Limitations / concerns.

• Recreation from a reference differs from issue-driven maintenance.
• Visual/programmatic assertion coverage is still finite.
• Multiplatform reproducibility and training cost may be substantial.

Reading recommendation.
Add to queue — prioritize the unified harness, reference-grounded verifier design and transfer experiments.

[P1] How Researchers Use and Verify AI Coding Assistants: Tasks and Validation Practices in Scientific Programming

• Work ID: arxiv-2609.22049
• Registry: record
• Links: Paper · PDF source
• Primary area: LLM4SE empirical study / human-AI collaboration
• Tags: scientific-programming developer-practice validation
• Status: Preprint — venue not stated
• Venue: arXiv
• Version / date: arXiv v1, 2026-09-18
• Authors: Gabrielle O'Brien, Reed Milewicz, Nasir Eisty
• Affiliations / team: not asserted in registry
• Notable author/team signal: empirical scientific-software focus
• First seen: 2026-09-22

Fast grasp

One-sentence takeaway.
Across 527 free-text accounts from researchers who program, AI-assisted scientific coding is concentrated in data handling, visualization, debugging, scientific computing and statistics, but validation remains largely informal and individual.

Research problem.
What tasks do researchers actually delegate to AI coding assistants, and how do they decide whether generated scientific code is trustworthy?

Problem definition / setting.
The study codes 527 responses from a 2025 survey of researchers, each describing one AI-assisted programming task and how the result was evaluated.

Core idea.
Rather than benchmark model output, measure real validation behavior and relate it to experience, research area and confidence.

Method / system.

• Qualitative coding of task categories and evaluation practices.
• Statistical comparison against programming experience, research area and confidence.
• Focus on naturally occurring scientific-programming workflows rather than lab tasks.

Evaluation.

• Dataset: 527 free-text survey responses, mostly from U.S. university researchers.
• Measures: task type, validation strategy, experience and confidence.

Main findings.

• Use clusters around data handling, visualization, debugging, mathematical/scientific computing and statistical analysis.
• More than half report running generated code, but automated testing and peer review are rare.
• Less experienced programmers tend to trust the AI more than themselves; experienced programmers show the reverse pattern.
• Confidence in evaluation is not associated with the reported validation strategy; it correlates more strongly with confidence in the tool and in oneself.

Novelty vs. prior work.
The value is ecological validity: it documents how researchers actually validate AI-generated scientific software rather than inferring practice from benchmark success.

Why it matters for AI4SE.
The findings expose a gap between increasingly rigorous agent benchmarks and everyday human workflows. Tooling that makes testing, provenance and peer review easier may matter as much as model capability.

Limitations / concerns.

• Self-reported survey behavior may differ from observed practice.
• The sample is mostly U.S. university researchers.
• One-task-per-response framing may underrepresent complex iterative workflows.

Reading recommendation.
Add to queue — especially relevant for human-AI collaboration, developer productivity and validation-interface research.

3. Other new selected papers

No P2 papers selected today.

4. Publication and version updates for known works

No meaningful publication/version updates were confirmed for already indexed works in today's search window.

5. Possible duplicates requiring review

None.

6. Reading-queue actions

Add

• arxiv-2609.21190 — SWE-Proof — formal correctness for real repository issues — priority P0
• arxiv-2609.22068 — CodeMidas — scalable executable RL environment generation from source code — priority P0
• arxiv-2609.21562 — GameLogicBench — tick-level runtime evaluator and mutant validation — priority P1
• arxiv-2609.22000 — RecreationWorld — unified GUI+coding agent harness with reference-grounded verification — priority P1
• arxiv-2609.22049 — How Researchers Use and Verify AI Coding Assistants — real-world validation practices in scientific programming — priority P1

Promote to deep read

• arxiv-2609.21190 — specification-faithfulness and formal-verification methodology could materially change benchmark design.
• arxiv-2609.22068 — environment-generation/filtering is directly relevant to scalable coding-agent RL and benchmark synthesis.

Remove / deprioritize

• None.

7. Coverage and search notes

8. Notes

Today's strongest cross-paper observation is a convergence on verifier quality. Formal proofs, source-grounded generated tests, mutant-validated runtime assertions and reference-grounded UI checks all attack different versions of the same problem: agent capability is increasingly constrained by whether the evaluation signal actually encodes the intended software behavior.