iiinova — where your digital self keeps evolving

I do think a lot of people are in denial though!

020

I don’t think literally everyone should drop what they’re doing. But my sense is PL research as a whole is significantly under-reacting to AI. So I suppose I think *some more* PL people should bet on AI (but maybe not you!)

Happy to mail you a couple. Email me, my address is on my website

200

I think you’ve put your finger on the exact worldview mismatch because 5-10 years seems like an insanely long time horizon to me

Why constrain the grammar - just pull more samples and keep the ones that pass :p

Mike Dodds @m-dodds.bsky.social · 20/01/2025

Hot take for POPL: the PL community is still mostly in denial about AI. This is bad because PL+AI go great together - PL can solve the hardest problem with AI - trusting the output it produces - AI can solve the hardest problem with PL - finding enough engineers who can even use the tools

2141

Mike Dodds @m-dodds.bsky.social · 20/01/2025

I’m bringing these cute Galois stickers to POPL so if you want one, come find me

1110

Mike Dodds @m-dodds.bsky.social · 27/12/2024

8 years on, the future is here! xkcd.com/1813/

xkcd.com

Vomiting Emoji

040

If I understand right, the private test set is only used during evaluation of the model - not available to the team doing the training

OpenAI o3 Breakthrough High Score on ARC-AGI-Pub

Seems almost certain it’s deliberately trained on math reasoning. The way the o-series models seem to work is by long CoT, with reinforcement learning to impose correct reasoning. Not much public about how o3 works internally, but Chollet has some speculation: arcprize.org/blog/oai-o3-...

arcprize.org

OpenAI o3 scores 75.7% on ARC-AGI public leaderboard.

A big jump on coding skill as well:

010

Re o3 - this is the big one for me. The Frontier Math benchmark is designed to be extremely difficult, and it has a private test set (no data contamination). Today, o3 is v expensive. But seems inevitable it’ll soon be cheap. If these results hold up, that means MUCH more powerful automated math

332

I think specification will be a much harder problem. Nearly all successful proof deployments have been in “easy to specify” domains - OSs, hardware, crypto, etc. these are unusual, & most systems are very difficult to specify formally

020

Optimistically this could haul a lot of tools across the break-even line into viability. There are many formal methods ideas that simply haven’t been tried because the cost/benefit never worked out. Exciting times for proof tech / FM

100

I think there’s good reason to be optimistic that proofs themselves will get much cheaper. Most proof tools are structured as untrusted search and trusted checking. Gen AI is a just new untrusted search process which should slot right in alongside SMT solving etc

100

I gave a talk recently about proof technologies - what people deploy today, what might be available soon, and what seems far off even with fancy AI. Slides here: mikedodds.github.io/files/talks/...

1175

(& yes, I’d be excited to hear more about what you’re working on!)

000

Completely agree. Today’s LLMs are nowhere near the hardest verification tasks, and getting there will take more leaps. I’m not sure what’s needed - more special purpose tooling, or just more generic intelligence from the LLM+RL combo. To be determined I think

100

I think LLMs + reinforcement learning + trad synthesis seems quite promising for inductive invariants. There’s some hope that AI can knock out the 80% of “easy” cases, even if a hard core remains

Yes, totally agree the specific claim matters. I sometimes mean “this is astonishing and seems like it can automate many tasks we care about” and maybe people are hearing “AGI is here, this can code better than a human”. I do aim for a little more nuance in person than on social media though :)

Well, it’s hard to say because in the skeptics typically don’t want to make clear bets :) But my sense in such conversations is they are denying capabilities that are already here. An SMT solver (or a printf statement) can generate a FramaC spec, that’s not what we’re talking about

I think progress is astoundingly rapid and it seems plausible (not certain!) that AIs will routinely beat human experts on many of these tasks soon

100

Obviously, even the most capable current LLM can’t do these kinds of tasks perfectly, every time, for big programs etc. But surprisingly often people will fully deny they can do them *at all*

A few off the top of my head: writing function specifications in eg FramaC, generating correct programs based on free-text problem descriptions, solving logic puzzles that require structured reasoning, finding bugs in code

I have had conversations with professor types who say “oh I don’t think an LLM will be able solve <whatever> for a long time” and I show them the base ChatGPT model doing <whatever> first time with simple prompting. Many people’s intuitions are stuck (especially LLM critics)

181