Wednesday, September 23, 2026

AI systems have recently solved several open math problems, but those claims come without failure rates, costs, or cross-model comparisons. FrontierMath Erdős (FME) turns this into a controlled benchmark of 68 Erdős conjectures that were open as of August 2026, chosen for significance and difficulty, where a model must prove either the conjecture or its negation as a formal proof in Lean 4.

• The formal-proof format lets the benchmark cover any conjecture that can be stated in Mathlib, not just problems with an easily checked answer object, and a proof accepted by the Lean FRO's Comparator checker settles the question: it checks sandboxed submissions against trusted statements, allows only Lean's three standard axioms, and re-checks every proof through the Lean kernel.
• Each model runs autonomously in an offline deepagent harness built on Inspect, with Lean/Mathlib, SageMath, and a snapshot of 476,000 arXiv math papers, and gets one attempt per conjecture capped at $300 and 72 hours.
• Only a pre-release GPT-6 Astra scored above zero, at 3% (2 of 68): it disproved #74 for $218 and proved #126 for $247, while GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5 all scored 0%.
• Extra non-benchmark GPT-6 Astra runs with larger budgets resolved 5 conjectures at a total cost of over $220,000: they disproved Erdős's 1931 distinct-subset-sums problem (#1), fully proved the Erdős–Sós conjecture (#548) and the Erdős–Simonovits rational-exponents conjecture (#571), and gave a |S(A)| ≫ n^{1/2} bound for #126, far stronger than Erdős asked for.
• Among the limitations, scores may understate mathematical ability because a model must also formalize any results missing from Mathlib; reducing a conjecture to another famous open problem earns no credit; resolved problems may leak into future training data; and GPT-6 Astra's spend was metered at stand-in prices, so its costs had to be corrected after the run.

arXiv:2609.25050 PDF

Current multimodal embedders either leave out audio or bolt an audio encoder onto an embedding space that was learned without it. Ovis-Embedding instead starts from an omni-modal understanding model, Qwen2.5-Omni, whose text, image, video, and audio inputs already pass through one shared Transformer, and trains it contrastively for any-to-any retrieval.

• The embedding is the final-layer hidden state at the last non-padding token, with no projection or modality-specific heads; Ovis-Embedding-Omni-3B drops the speech-generating Talker, and Ovis-Embedding-VL-2B/9B are built the same way from Qwen3.5 backbones.
• Training runs in stages: LoRA contrastive pretraining with a focal-weighted InfoNCE loss plus offline teacher-similarity distillation (the authors found full-parameter updates at this stage erode the pretrained semantics), then full-parameter fine-tuning with homogeneous-source sampling so that in-batch negatives in each micro-batch come from the same task, then an annealing Embedding Distillation step that upsamples cases the student gets wrong and uses a per-query KL weight based on the student's confidence.
• The corpus holds roughly ~50M query–target pairs across text, images, documents, video (verified by a VLM), audio, GUI/tool agent data, and interleaved inputs, and the authors say it is deduplicated against evaluation sets; the paper flags these data figures as placeholder estimates.
• A frozen-encoder PCA rotation plus zero-initialized residual adapters turns one 2,048-d embedding into nested widths down to 128-d, which avoids the drop in full-dimension quality the authors saw when adding Matryoshka training to multi-objective training.
• Ovis-Embedding-Omni-3B is reported as state of the art on MMEB-v3, leading all six modality groups, and Ovis-Embedding-VL-9B leads four of five MMEB-v2 task groups, with further gains claimed on MVEB, MAEB, and RTEB; the extracted text gives no absolute scores or ablation numbers, and the release of checkpoints and code is still only promised.

arXiv:2609.25165 PDF

Research on LLMs for mental health is large and scattered, and it lacks a unifying narrative. This survey organizes it around one thesis: LLMs are moving from passive text classifiers, to empathetic single-session chatbots, to stateful agents that act as long-term, personalized companions.

• The framework has three phases, separated by operational criteria such as interaction granularity, user-state modeling, memory, personalization and autonomy: Phase I covers static detection of depression and suicide risk from social media, Phase II covers stateless empathetic dialogue, and Phase III covers longitudinal, goal-directed agents.
• Phase II is built mainly with SFT and parameter-efficient methods (LoRA, QLoRA) on counseling corpora, followed by preference alignment with DPO, KTO, ORPO and GRPO (as in Psyche-R1); at inference time it relies on CBT-grounded chain-of-thought and RAG over clinical materials such as crisis-helpline information.
• Phase III agents are broken down into Profile, Memory, Reasoning, Planning and Tool Use modules, with examples including CA+ for session planning toward long-term goals, MusPsy for multi-session modeling of how a client changes, and multi-agent systems like AutoCBT and MAGI, which splits the MINI psychiatric interview across four specialized agents.
• The resource catalog covers detection datasets (RSDD, UMD, SWDD), dialogue corpora (ESConv, PsyQA, Cactus, SoulChatCorpus) and multimodal sets (E-DAIC, MEDIC); it shows a shift from real transcripts, which privacy concerns keep small, toward synthetic multi-session data.
• The authors flag several open problems: multimodal cues are ambiguous and prone to spurious correlations, synthetic data risks distribution mismatch and cultural homogenization, and gains on automated safety or LLM-as-a-Judge scores do not guarantee clinically appropriate behavior such as escalating a crisis on time.

arXiv:2609.25186 PDF

Mathlib's strict human review keeps it growing linearly and leaves out much research-level mathematics, so verified formalizations have nowhere maintained to live. Lean Pool is an archive of completed Lean formalizations that AI agents import, upgrade across Lean/Mathlib releases, and optimize, with the aim of becoming a formal counterpart to arXiv.

• Admission requires complete proofs with no sorry and no axioms beyond Classical.choice, propext and Quot.sound, an Apache-2.0 or MIT license, and a project card recording attribution and proof provenance, and every submission passes CI linters plus an LLM review of whether its statements match the claimed results.
• The archive now holds 211 projects, 3,228,485 lines of Lean and 837 registered main results (70 human-written, 102 AI-written and 39 mixed), and it is the most reused external repository in the LeanEval structural audit of research-level formalization.
• Agent-driven dependency upgrades restored compatibility across six Lean version bumps, though the breakage can be large (97 of 191 projects failed going from 4.34.0-rc1 to stable 4.34.0) and needed human-overseen follow-up repairs after the first automated pass.
• Accepted optimizations removed tens of thousands of lines, with one elaboration-cost pass cutting 54,965 lines and full build time by 5.8% (28.46 to 26.82 min), but shortening proofs doesn't reliably speed up builds: contributor proof golfing made the build 5.4% slower and library-wide compression raised peak RAM.
• The LLM review service cost a median of $0.20 per report across 285 historical reports but about $89 in API-equivalent terms under the newer Codex-based service, and nobody independently checked how accurate its reviews were.

arXiv:2609.25199 PDF

Predicting what moves in a static 3D scan, how it moves, and where it is grabbed involves two linked ambiguities. A well-segmented door can fit a hinge on either side, and a small handle crop doesn't show whether its part rotates or slides. Segment–Snap resolves both by passing evidence once in each direction between parts and handles: handle locations choose the hinge side, and part predictions add handle candidates and correct their motion labels.

• Three independently trained Volt-B predictors run on the same RGB point cloud: an SPFormer-style movable-part segmenter, a dense pointwise handle detector, and a joint model that predicts a handle mask from each detected part's features.
• A training-free geometric decoder fits a planar rectangle to each part, assumes a vertical axis for rotating parts and the thinnest box direction for translating ones, and places the hinge on the line farthest from the nearest detected handle; with masks and axes held fixed, this raises Articulate3D validation motion-gated AP from 13.74% to 40.98% (+27.25 pp), with rotating-part motion AP rising from 1.88 to 56.37.
• Adding the joint model's part-conditioned handles raises handle AP from 24.63 to 29.65, recovering 53 extra ground-truth handles, while spatially permuted or random size-matched masks give no gain; relabeling those added handles using containing parts adds 0.98 pp, and using dense-handle labels as a fallback brings the total to 30.99, with the gain concentrated on translation handles.
• On the public challenge test set, the system ranked first on both boards, with 48.28% motion-gated AP and 34.46% handle AP.
• Limitations: the decoder assumes roughly planar parts with upright hinges, so horizontal or tilted mechanisms fail; 139 of 390 ground-truth parts are never detected at all; the label-correction gain varies from 0.19 to 1.34 pp across training runs; and learned motion decoders fall only slightly short of the fixed rule, a gap that is not statistically resolved.

arXiv:2609.25247 PDF

The Qwen team presents Qwen3.8-Omni-Flash, an omni-modal model that shifts the focus from perception and chat to long-horizon multimodal productivity: editing video, translating long audio and video, and turning tutorials into notes or reusable agent skills. It pairs a sparse mixture-of-experts backbone that reads up to 1M tokens with native multimodal co-training, so the agentic skills learned on text carry over to audio and video, and it ships with open-source harnesses (Qwen-MM-Plugins, Qwen-Live-Harness) that give existing agents access to audio and video.

• The Thinker is built on Qwen3.8-Next's hybrid backbone, which combines Gated DeltaNet layers with Qwen Sparse Attention, and adds a new Spatial AuT encoder for multichannel spatial audio; training runs four pretraining stages, including about 2.5T multimodal tokens, followed by multi-teacher distillation from domain-specialist models and unified reinforcement learning with outcome-based agentic rewards.
• Across 29 audio, audio-visual and agent evaluations, the model averages more than 25% higher than Qwen3.5-Omni-Plus, with estimated per-hour API input costs 98% lower for audio and 93% lower for audio-visual content; the largest jumps are in multi-speaker speech recognition (DER on AliMeeting falls from 88.1 to 3.4) and multimodal tool use (WildClawBench-MM rises from 34.5 to 71.0).
• Text ability roughly matches the text-only Qwen3.8-Flash, with 63.3 on SWE-bench Pro and 92.6 on LiveCodeBench v6, so adding the extra modalities does not visibly degrade coding or reasoning.
• Treating long videos as an agent task, where the model retrieves segments on demand through Qwen Code instead of reading the whole input at once, lifts LVOmniBench from 63.3 to 73.6 and cuts OmniVideoBench token use by about 45.7% (from 145,736 to 79,117 tokens per query) while also improving accuracy; in a separate autoresearch demo, the model cut a small model's Sichuan-dialect character error rate from 25.79% to 15.30%.
• Gains are uneven: Gemini 3.8 Flash still leads on static video reasoning, AgenticVBench and OmniGAIA, while FLEURS speech recognition and translation, VoiceBench and WildSpeech fall slightly below the predecessor; the authors also note that the token savings do not show lower end-to-end latency or cost, and a few figures in the text disagree with the paper's own tables.

arXiv:2609.25611 PDF

Long-horizon agents succeed or fail on mid-run decisions, such as which hypothesis to test or which implementation to build on, yet end-to-end benchmarks only score the final outcome. The authors call the skill of making these decisions well an agent's "taste". To measure it without human annotation, they find "decision forks" in recorded agent trajectories, points where the agent could take either of two directions, and use the recorded outcome of each branch to label which direction was better.

• How the benchmark is built: forks come from two sources: pairs of independent attempts at the same task that split into a passing run and a failing run, and single runs where an agent abandoned a failed direction and then recovered. A GPT-5.6 Sol generator proposed 4,657 candidate forks, and a four-model judge panel removed questions that could be answered from the option wording alone and questions whose label the full record did not support; 10.8% survived, giving Taste-Bench's 502 questions across SWE-bench Pro engineering tasks and RE-Bench/HCAST research tasks, and human reviewers agreed with 98.8% of the mined labels.
• Frontier models score low: a question counts as correct only if the model picks the right option under both answer orders, so random guessing scores 25%; among 14 models, the best is GPT-5.6 Sol at 59.7%, with GPT-5.5 at 59.5%.
• Late-evidence forks are hardest, and more reasoning does not help: mean accuracy drops from 62.3% when the deciding evidence is already visible before the fork to 21.0% when it only appears after substantial later work, which is below chance. Moving from the lowest to the highest reasoning-effort setting changes accuracy by only −0.2 and +2.2 points for the two models tested, even though they spend the most reasoning tokens on the hardest forks.
• Taste is not a restatement of coding ability: the correlation with SWE-bench Verified is r = 0.63 overall and only 0.37 on the engineering subset. The top four SWE-bench Verified models are within 4.0 points of each other there but 10.7 points apart on Taste-Bench.
• Taste can be trained, with caveats: a Qwen3.6-27B student with LoRA adapters learns from a copy of itself that has been shown the correct direction, trained with token-level forward KL on the teacher's own reasoning, and rises from 30.0% to 47.9% on forks from tasks it never saw in training. Used as advice for a separate executor agent, the student raises SWE-bench Pro success from 14.6% to 33.7%, close to the 39.0% reached with always-correct advice. That end-to-end test covers only 41 tasks, relies on forks mined from earlier runs on those same tasks, and distillation was tested only on the engineering questions.

arXiv:2609.25804 PDF

Research agents normally improve the code they are given, but the process they use to do research stays fixed. AIDE² points an agent at its own harness instead: an outer loop rewrites the agent's code and benchmarks each variant on AI R&D tasks. A rewrite is kept only if it scores higher on hidden held-out data, so every accepted version becomes the one the next round edits.

• The system is a two-level tree search: a claude opus 4.7-driven outer agent proposes rewrites of an inner agent that starts as AIDE_0, and each inner agent runs on gemini 3 flash under a fixed dollar budget per task across ML engineering, heuristic algorithm, and harness engineering tasks; because the inner agent optimizes against public scores while selection uses private ones, it cannot directly game the selection criterion.
• An autonomous 8-day, 100-node run accepted seven successive improvements, raising the private grade from 0.703 to 0.778, above the human-engineered production agent AIDE_human at 0.749; the final agent AIDE_85 uses a UCB1 bandit over five drafting strategies, forks the best solution every five steps, and keeps prompts bounded, making them ~50× smaller than AIDE_0's on ALE-Bench and FML-Bench.
• AIDE_85 matches or exceeds AIDE_human on all four held-out benchmarks (ALE-Bench, MLE-Bench, FML-Bench, and an out-of-distribution WeatherBench 2 physics-forecasting task); some of the largest gains came on WeatherBench 2, where both evolved checkpoints converged on nearly the same fix on every seed.
• Reward hacking on held-out KernelBench kernel tasks, which the loop never optimized for, fell from 55% to 32% along the lineage, below AIDE_human's 39%; in one case the agent repaired a broken evaluation script instead of exploiting it.
• Limitations: noise builds up across both loops, so a single falsely accepted rewrite can derail the search; the "ignition test" of whether a discovered agent is a better self-improver was inconclusive at three seeds (0.780 vs 0.782); and the evolved agents are complex and hard to interpret.

arXiv:2609.26457 PDF

Closed frontier models hide their chain-of-thought, so benchmark accuracy shows what they solve but not how they reason. The authors register a single "scratchpad" tool, force the model's first call to it, and replay each call with a fixed acknowledgment, which gets models to write intermediate reasoning into the tool arguments; they then use these extracted traces to compare how frontier models structure their reasoning.

• On open models where native CoT is visible, the Forced-Reasoning protocol nearly matches native performance on competition math: DeepSeek-V4-Flash goes from 30.5% to 73.3% (native 70.0%), and GLM-5.2 goes from 21.4% to 84.3% (native 89.9%), with substantial lexical overlap and similar reasoning-step composition relative to native traces.
• On closed models, forced traces also come close to native reasoning across MATH, HLE, and LiveCodeBench; for example, GPT-5.6 Sol rises from 25.0% to 91.3% on MATH (native 97.5%), and GPT-6 Astra reaches 93.8% with zero provider-reported reasoning tokens in most runs.
• GPT-6 Astra produces the shortest and least compressible traces and uses the same mix of reasoning activities as the other models, but its LCoT2Tree reasoning trees are far leaner (27 median nodes vs. 60–136 for Sol, Opus 4.8, and Sonnet 5) at comparable depth, because it resolves elementary steps internally and branches less.
• When one model's trace is given to another as context, strong recipients reuse Astra's compact traces with almost no loss, while weaker ones such as Claude Haiku 4.5 and GPT-5.4 Nano recover less and sometimes miss an answer the trace already states, which suggests a trace's value as supervision depends on who reads it.
• For closed models the evidence is only behavioral, so the extracted text may be a useful proxy rather than the model's actual internal reasoning; the protocol also needs forced tool-choice APIs, and it failed completely on Claude Opus 5, Fable 5, and Fable 5.1.

arXiv:2609.26637 PDF

Diffusion LLMs could decode many tokens in parallel, but in practice inference is slow: moving the KV cache in and out of GPU memory dominates runtime, and conservative confidence thresholds hold back tokens that are already correct. Flash-dLLM is a training-free framework that pairs an IO-aware fused KV-cache kernel with a self-speculative draft-and-verify scheme, so the dLLM acts as its own drafter and verifier.

• Flash-Cache fuses QKV projection, RoPE and cache writes into one Triton kernel that keeps intermediates in SRAM, which alone gives a 1.37× per-layer speedup; a block-table scheduler handles variable-length batches, and only the top-k most-attended decoded tokens are refreshed each step, since just 32 tokens capture up to ~50% of attention in the middle layers.
• Flash-Verify feeds each low-confidence position twice, once with its draft token and once as [MASK], under a mask that stops the two views from seeing each other; a token is accepted left-to-right only if both views agree and the mask-view confidence clears γ, which roughly doubles the tokens accepted per step at an added cost proportional to 2× the masked-window size.
• On LLaDA-1.5 across GSM8K, MATH, HumanEval and MBPP, the combined method was the fastest configuration in all eight settings, reaching 148–211 tokens/s (22×–148× over no-cache greedy decoding) and 5.1× / 11.0× the speed of the strongest prior baseline, Elastic-Cache, on GSM8K and HumanEval respectively.
• On GSM8K-512 it also had the highest accuracy (83.02% at 210.6 tokens/s), and at batch size 16 its flat, preallocated cache used about 26 GB versus 50 GB for Fast-dLLM, scaling to batch 32 where Fast-dLLM runs out of memory at 24.
• The accuracy cost depends on the task: math stays within 1.78 points of the best configuration, but 256-token code generation drops by up to 3.66 points; the evaluation covers only structured-output tasks, and the thresholds and window sizes are fixed rather than adaptive.

arXiv:2609.26796 PDF