It's L3 Lab CUA Week!
Over the next week, we'll have several research releases about realtime agents that interact with the digital and physical worlds.
Stay tuned if you're interested in realtime agents, multi-agent communication, RL envs, computer-use, robotics, or new models score below 10%!
Over the next week, we'll have several research releases about realtime agents that interact with the digital and physical worlds.
Stay tuned if you're interested in realtime agents, multi-agent communication, RL envs, computer-use, robotics, or new models score below 10%!
5
13
47
4,778
Led by Pranjal Aggarwal (@PranjalAggarw16)!
Follow along here and at our CUA Week page:
- cmu-l3.github.io/cua-week/
We'll update the page as each project is released.
Follow along here and at our CUA Week page:
- cmu-l3.github.io/cua-week/
We'll update the page as each project is released.
1
0
9
600
Day 1 of CUA Week:
Gym-Anything-RT: Scaling Real-Time Environments for Vision-Language Agents by @PranjalAggarw16
arxiv.org/abs/2610.37567
We know how to build agents for situations where they can pause and think, but what about agents that need to act quickly in real-time?
Gym-Anything-RT synthesizes clever minigames that change as the model is thinking. The environments end up being pretty difficult even for frontier models:
- GPT Astra: 9%
- Opus 5.5: 5%
0
0
0
136
Sean Welleck retweeted
We collaborated with @browser_use to create Odysseys2, a set of 100 web navigation tasks that are much harder and longer horizon than the original Odysseys.
Most importantly, all of these tasks are based on real user requests made to Browser Use, and represent a true al users want CUAs and web navigation agents to do. We also produced a much stronger automatic judge for evaluations, which was sorely needed for these very long horizon evals. GPT-6 Astra is the best performing model on Odysseys2. It gets 47% of tasks perfect, so there's plenty of headroom for improvement!
Great work led by @JangLawrenceK and @Alezander9!
Most importantly, all of these tasks are based on real user requests made to Browser Use, and represent a true al users want CUAs and web navigation agents to do. We also produced a much stronger automatic judge for evaluations, which was sorely needed for these very long horizon evals. GPT-6 Astra is the best performing model on Odysseys2. It gets 47% of tasks perfect, so there's plenty of headroom for improvement!
Great work led by @JangLawrenceK and @Alezander9!
Introducing: Odysseys2 - hardest long horizon benchmark for web agents based on real user tasks 🏗️
We collaborated with @JangLawrenceK @rsalakhu from Carnegie Mellon University
> SOTA agent fully completes only 47/100
> 5 agents complete none
> 8-12 real rubrics per task, 60 min on thare becoming better than humans at knowledge work.
odysseysbench.com/v2
3
8
33
1,996
Day 1 of CUA Week:
Gym-Anything-RT: Scaling Real-Time Environments for Vision-Language Agents by @PranjalAggarw16
arxiv.org/abs/2610.37567
We know how to build agents for situations where they can pause and think, but what about agents that need to act quickly in real-time?
Gym-Anything-RT synthesizes clever minigames that change as the model is thinking. The environments end up being pretty difficult even for frontier models:
- GPT Astra: 9%
- Opus 5.5: 5%
Gym-Anything-RT: Scaling Real-Time Environments for Vision-Language Agents by @PranjalAggarw16
arxiv.org/abs/2610.37567
We know how to build agents for situations where they can pause and think, but what about agents that need to act quickly in real-time?
Gym-Anything-RT synthesizes clever minigames that change as the model is thinking. The environments end up being pretty difficult even for frontier models:
- GPT Astra: 9%
- Opus 5.5: 5%
LLMs might be superhuman at math, but can they act in real time?
Not even close!
Presenting Gym-Anything-RT, a framework for generating real-time minigames in which the game keeps moving while the model thinks.
Even the best frontier model, GPT-6 Astra, scores just 9%!
🌐: gym-anything.github.io/gym-anything-rt
🧵
4
5
31
1,363
Website: gym-anything.github.io/gym-anything-rt
Paper: arxiv.org/abs/2610.37567
CUA Week: x.com/wellecks/statu…
- cmu-l3.github.io/cua-week/
Paper: arxiv.org/abs/2610.37567
CUA Week: x.com/wellecks/statu…
- cmu-l3.github.io/cua-week/
It's L3 Lab CUA Week!
Over the next week, we'll have several research releases about realtime agents that interact with the digital and physical worlds.
Stay tuned if you're interested in realtime agents, multi-agent communication, RL envs, computer-use, robotics, or new models score below 10%!
0
0
3
226
- Code: github.com/gym-anything/g…
- Website: gym-anything.github.io/gym-anything-rt
- Paper: arxiv.org/abs/2610.37567
- Website: gym-anything.github.io/gym-anything-rt
- Paper: arxiv.org/abs/2610.37567
1
0
1
52
CUA Week: x.com/wellecks/statu…
It's L3 Lab CUA Week!
Over the next week, we'll have several research releases about realtime agents that interact with the digital and physical worlds.
Stay tuned if you're interested in realtime agents, multi-agent communication, RL envs, computer-use, robotics, or new models score below 10%!
0
0
0
50
Sean Welleck retweeted
LLMs might be superhuman at math, but can they act in real time?
Not even close!
Presenting Gym-Anything-RT, a framework for generating real-time minigames in which the game keeps moving while the model thinks.
Even the best frontier model, GPT-6 Astra, scores just 9%!
🌐: gym-anything.github.io/gym-anything-rt
🧵
Not even close!
Presenting Gym-Anything-RT, a framework for generating real-time minigames in which the game keeps moving while the model thinks.
Even the best frontier model, GPT-6 Astra, scores just 9%!
🌐: gym-anything.github.io/gym-anything-rt
🧵
7
19
88
6,437
Sean Welleck retweeted
The next few days are going to be exciting!
It's L3 Lab CUA Week!
Over the next week, we'll have several research releases about realtime agents that interact with the digital and physical worlds.
Stay tuned if you're interested in realtime agents, multi-agent communication, RL envs, computer-use, robotics, or new models score below 10%!
5
5
45
4,168
Sean Welleck retweeted
Today we’re bringing Aristotle to software and hardware!
Describe the properties your code must satisfy and Aristotle formally verifies that it meets them.
I’ve spent the past few months helping Aristotle expand from proving math to verifying code. I’m excited to see it available to everyone today.
Try it: aristotle.harmonic.fun
Describe the properties your code must satisfy and Aristotle formally verifies that it meets them.
I’ve spent the past few months helping Aristotle expand from proving math to verifying code. I’m excited to see it available to everyone today.
Try it: aristotle.harmonic.fun
We’re bringing Aristotle to code.
AI is writing more code than anyone can review. We're building the AI that verifies it.
Starting today with C and Verilog.
3
4
51
2,145
Sean Welleck retweeted
Lean Verified Tokenizers (srush.github.io/verified-token…)
Training-inference mismatch kills RL runs, but yet we build messages in Jinja? Prototypes a Lean-verified Rust agent pipeline.
Training-inference mismatch kills RL runs, but yet we build messages in Jinja? Prototypes a Lean-verified Rust agent pipeline.
21
35
388
21,715
Sean Welleck retweeted
Amazing progress!
The largest math proof in human history is now computer-verified.
Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry."
About 15,000 pages, built by over 100 mathematicians across generations.
10
7
97
6,052
Sean Welleck retweeted
Software Verification in Lean (SVIL) comes to Stanford University on Saturday, November 7.
Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end y-critical systems.
Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels.
Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds.
In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward.
Program and registration: beneficial-ai-foundation.github.io/SVIL2026_Fall/
Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end y-critical systems.
Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels.
Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds.
In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward.
Program and registration: beneficial-ai-foundation.github.io/SVIL2026_Fall/
4
57
348
21,390
Sean Welleck retweeted
🚀 Introducing LLM2Cert: the first end-to-end framework bringing Lean into agentic synthesis + verification of Lyapunov/barrier certificates, co-led by @Zhipeng0727 and me.
🏆 Automatically synthesized & formally verified safety/stability certificates for 81 of 105 benchmark dynamical systems (77%). On a common subset, 2.1× the successes of 5 prior pipelines combined.
More details in the thread below 🧵👇
🏆 Automatically synthesized & formally verified safety/stability certificates for 81 of 105 benchmark dynamical systems (77%). On a common subset, 2.1× the successes of 5 prior pipelines combined.
More details in the thread below 🧵👇
2
9
24
1,531
Sean Welleck retweeted
That’s a great benchmark to look at
1/5
Verification has become the bottleneck as LLMs start proving conjectures at scale! No worries, Lean can help. But how well can AI agents solve open problems formalized in Lean, end to end?
Introducing reuF2F: 244 open math problems from Research Experiences for ograms, spanning a broad range of math areas, formalized by experts in Lean.
We also build Leanimum-agent, a minimal coding agent for Lean, so every model is compared under the same harness.
Even the best-performing model resolves only 109 out of 244 problems. More below 🧵
0
1
3
4,481
Sean Welleck retweeted
If you've noticed a distinct dialect emerging in frontier AI models and struggled to understand what they're talking about, you're not crazy!
We turned to psycholinguistics to investigate what makes the writing style so weird, and why this might be happening
🚨New preprint! 🧵
We turned to psycholinguistics to investigate what makes the writing style so weird, and why this might be happening
🚨New preprint! 🧵
28
136
897
91,136
Sean Welleck retweeted
AI agents can't yet carry out open scientific research
Into the Unknown benchmarks 9 frontier agents on 15 unsolved research directions curated by DOE scientists. None of the 135 submissions meets the scientist's bar, and 114 fail an integrity check for fabricated or inconsistent results.
Into the Unknown benchmarks 9 frontier agents on 15 unsolved research directions curated by DOE scientists. None of the 135 submissions meets the scientist's bar, and 114 fail an integrity check for fabricated or inconsistent results.
5
7
41
2,694
Sean Welleck retweeted
REUF2F: Benchmarking coding agents on formalized undergraduate research problems. ~ Zeyu Zheng et al. zeyu-zheng.github.io/reuF2F.pdf
#AI4Math
#AI4Math
0
1
2
378