Toby Murray

Formal Verification in the Age of AI For decades, research in formal verification has been guided by a simple mental model that I recently coined the formal verification triangle. The triangle captures a trade-off between three desirable...

New blog post: Formal Verification in the Age of AI verse.systems/blog/post/20...

No sleep, no worries

Avigad had written an important note grappling with the rise of AI for mathematics. Almost all is equally applicable to much of computer science. Academics must face the challenge of re-prosecuting our mission as researchers and educators in the age of AI. www.andrew.cmu.edu/user/avigad/...

Home-brand Howard, perhaps?

AI and Humans Verify Fields Medal Proof for the First Time How did AI help solve a 24-dimensional puzzle in just two weeks? Dive into the world of sphere packing and find out.

Almost no matter what base of human effort this was situated on, 200K lines of proof in 2 weeks is remarkable. In Isabelle/HOL we used to reckon on about 10K lines of proof = 1 person-year. spectrum.ieee.org/ai-proof-ver... cc @lawrpaulson.bsky.social @microkerneldude.bsky.social

Family includes everyone! ❤️

Thoroughly enjoyed this

As I said a few months ago (bsky.app/profile/toby...), GenAI allows thought policing and surveillance of a kind Orwell couldn’t dream of. We should expect the familiar debates between safety-by-surveillance vs civil liberty to be rehashed on this arena, as this piece shows

Only more important. However of course that’s what I want the answer to be, because that’s what I find most interesting (rather than the algorithms themselves). OTOH maybe learning the algorithms is already sufficient to internalise the design principles and to recognise when each applies

See eg Levitin whose book is centred on this approach (and from where I inherited it). I’m not sure I’m disagreeing with you, Shriram, but I do wonder to what degree the arrival of GenAI has shifted what it important for students to learn. Intuition tells me that learning how to design has become

with canonical instances. Then give them problems to solve (“design an algorithm to …”) with breadcrumbs pointing to which paradigm ought to be applied, with the canonical instances serving as exemplars. This is very well trodden ground and I have to admit to not having innovated much here.

This is very thoughtful (I’d expect nothing less from Shriram). There is a massive gap I’m sure between what I wish students would focus on and what they actually take away. That’s entirely expected. The way I have tried to teach this stuff previously was to introduce algorithmic paradigms

Know someone doing outstanding research towards or resulting in practical improvements for Australia's national security or capability for defence?

Nominate them for the Eureka Prize for Outstanding Science in Safeguarding Australia by 16 April

https://bit.ly/40jSZi0

Would love to see this talk. But, dude, here is my "program incorrectness" checker:

function is_incorrect(prog) {
return true;
}

It is accurate for 99.9999999.....% of programs, requires no evidence, nor any oracles.

Right. This is something that I'd love your take on. I feel like these kinds of dynamics explain well why simply trying to improve education, critical thinking, etc. is no panacea against disinformation, because people believing bullshit has much more to do with e.g. group belonging than rationality

the rational part that knew that since HDMI transmits coded digital signals the result is all or nothing and “signal quality” is meaningless.

What a perfect example of social dynamics leading to irrational decision making. Mine: a salesman once talked me into paying for a much more expensive HDMI cable to ensure “superior sound and video signal”. In hindsight I’ve always been amazed that the social part of my brain totally overrode

Heaps good. Let's all learn something. Without trying to preempt you, would you have agreed with @ccanonne.github.io 5 years ago? Or does the disagreement stem from different ideas about what the point of teaching "algorithm design" was in the first place?

Peter Schachte and I had exactly this conversation last week and reached almost exactly the same conclusion. Giving students a framework (and familiarity having applied it) to think lucidly about how to solve computational problems. But that was the point all along.

🤯

bsky.app/profile/grog...

call me a thursday night pub special, cause I'm a well done angus

I’ve never been a Gates fanboy but I note that the passion project of the tech bloke who was the world’s richest man when I was a teen was about saving millions of lives, not ending them.

Cartoon showing a street in the rain. A man on a bike is delivering food, while another courier is delivering packages from Amazon. Two other workers are collecting garbage. Inside one of the houses on the street, we see robots labeled 'AI' sitting dry and warm, engaged in making a paining, playing the violin and writing.

The robot apocalypse hasn't happened yet, but still I can't escape the feeling that something has gone horribly wrong... Cartoon for Dutch newspaper @trouw.nl.

More of my work for Trouw: www.trouw.nl/cartoons/tje...

#ArtificialIntelligence #creativity #work #GenerativeAI

I cannot imagine a better term to devalue the intellectual activity of programming.

Hello first years! Welcome to Code Generation 101. It’s wonderful to lead you in your first steps as future computer scientists.

OTOH as a programmer whose primary job it is to implement feature X, not learn library Y, for whom learning happens *incidentally*, maybe the study correctly models that reality, and it’s fair to conclude that AI use hampers incidental learning.

I also wondered about this aspect. I think it’s possible that the instructions affect how people might choose to use AI. Were I told “get it done fast” vs “ learn as much as you can” I expect I’d use the AI very differently. However their results suggest there may be ways to be both quick and learn.

I agree and am glad you called this out. But I’m also a bit wary of trying to generalise too much from these results. The study participants were not (eg.) novice programmers.

Thanks for the thoughts! I read that study mostly through the angle of education, and to me the key takeaway (explicitly made by the authors) is that early AI use when coding prevents the acquisition of the very skills later needed for effective use of AI in coding. (Cf. Breakdown of participants...