tlringer

Every DeepMind press release is like this.

(Conflating a few things here, and only noticing now; there are also languages with undecidable type checking in which one cannot prove false, mostly because of fancy equality checking, though that's undesirable in some ways. But it's not accurate to think of typeclass resolution as part of the type checker IMO. It is in a layer similar to tactics.)

Typeclass resolution is implemented as a layer of automation that is above the type-checking kernel, so much like with nonterminating tactics, if it doesn't halt you mostly just end up with confusing automation that doesn't help you prove something, but you shouldn't be able to prove false. Mostly it's a usability nightmare for typeclasses, and in the case of this post also a way for hilarity to ensue.

It was fine, unless you reach far enough to take it literally, which is quite obviously not what Timnit intended.

Hopefully I'll see you there!

BTW what you say about the sadly common assumption Timnit and other AI ethics folks don't have "real contributions" is too real. It has impacted me even though my work isn't on AI ethics at all, just because I bother to talk about it online in public sometimes. Similarly for any social justice work or any work improving the work environment in research. It is like some people cannot comprehend that one can be technically proficient and still care about social justice and ethics and other "soft" issues. I love how confused those people are when they learn my expertise is in formal logic and proof haha

I went to AITP for the first time last September, and I found it an absolute pleasure. Everyone was kind and wonderful and open-minded. The venue was wonderful too. Highly recommended if you're interested at any point.

ML folks often call it "neural theorem proving." SOTA results are still from combinations of tactic prediction models with specialized tree search processes. They do OK on some interesting benchmarks, but still can handle mostly only fairly simple proofs. So far, they seem strictly complementary to symbolic methods. Interest is growing dramatically, though, and progress is accelerating, so I'm excited about the near future.

Language models are showing a lot of promise for autoformalization: automatically converting natural language mathematics to formal definitions, specifications, and proofs. This is a task where symbolic methods do not seem particularly promising in general, and one that meshes nicely with synthesis.

A good conference to look at is AI for Theorem Proving (AITP). It's small but has a lot of relevant work. All of the talks from this past year are recorded and on the website. MATH-AI at NeurIPS had some good work this year, too.

There is a bit of a culture and citation gap dividing the work in the AI community from the work in the PL/SE communities; in PL/SE I'd recommend work by Emily First and Alex Sanchez-Stern. They are undercited in AI work despite having SOTA results on meaningful Coq benchmarks. In AI, I'm particularly psyched about work by Tony Wu, Markus Rabe, Christian Szegedy, Sean Welleck, Albert Jiang, and many others. Tony's papers are a good gateway into other AI papers since the AI papers tend to cite each other.

OK, first clarification after further correspondence, the mistake on the environment numbers was small---accidentally misunderstanding the context in which Strubell mentioned particular numbers, I think? And Strubell's numbers were off because they used only public data they had access to, and I think misunderstood some things too. Some of the authors did not even know about it and it is news to them now. And it could have been addressed in a camera-ready, nonetheless. It was no reason to force the authors to retract a paper or remove their names, and that is part of the treatment of them that was extremely messed up.

Got it, thank you. On why Timnit is criticized so intensely everywhere anonymity is possible, I honestly think that is more an artifact of sexism and racism than an indictment of anything she has done. Also a matter of the target audience of a lot of the anonymous forums.

FWIW, at Google in Research, many people have mentioned her to me as the only person they trusted to talk to about the things they went through when they were not treated well. After she was fired, many of those same people felt no longer able to raise issues about internal treatment and culture.

Timnit was not carrying just her own burden, but the burden of many at Google in Research who were not treated well, especially women and people of color in Research. And so she spoke not just for herself. She had witnessed for years how demoralizing it is to try to really change things within Google. I think the only person who has done that and not burned out is Kat Heller. I did a lot of it over the summer, and it really took a toll on my wellbeing, and my desire to stay (part-time) at Google to finish my own work there. I'm excited for my affiliation to end so I can remove myself more thoroughly from Google's internal politics and culture, though I hope I've made enough of a dent that some things actually continue to change for the better.

Note that not everything was a misunderstanding on Jeff's end, just the early stuff before she was fired, which Timnit did not know. To be honest, I don't think Timnit would even believe that now. It's maybe one place where I diverge from her on this. She would find what I wrote about Jeff way too charitable. Her view is valid and is one of the reasons I rarely discuss this in public anymore, because it's hard for me to do so and not defend Jeff, and it's hard to defend Jeff and not gaslight Timnit. I probably messed up somehow above too.

It's hard to believe sometimes that someone so smart in some ways can miss such obvious signals. It took a long time for me to come to that conclusion and to understand, and I'm still very upset with how Jeff reacted. These are all people though, they make mistakes, Timnit included. The way she was treated is still not at all OK, and sometimes when we are in positions of power like Jeff we still hold responsibility for our mistakes.

I won't say anything else about Jeff in public. I did try to help minimize damage and pain in all directions. It was painful and exhausting and not very fruitful.

(Also who are you?)

Nah, this is the actual truth. You can feel free not to believe me, but I have more complete information about this situation than anyone else you'll ever talk to.

Incorrect. https://news.ycombinator.com/item?id=34382901#34385678

It was Megan Kacholia, who had put Timnit Gebru and others close to her down for a long time constantly within Google, always talking down and being condescending and rude, failing to respect Timnit in how she confronted Timnit about the paper (which she was ordered to retract by way of not Google's normal paper review process, but by a then-newly-implemented and since retracted secondary "sensitive topics review" process, due to a combination of actual mistakes like the environment numbers, and also Google being too afraid of reputational damage for her discussion of the very real and tangible harms of LLMs).

Timnit tried to raise this to Jeff Dean to get help (Jeff was Megan's manager at the time). Jeff completely misunderstood what she was asking for, and instead sent some response about the environment numbers being incorrect (and they are, but that doesn't at all justify the way Timnit was treated). Not beginning to imagine that Jeff could have missed this signal, Timnit responded sarcastically. Jeff didn't pick up on the sarcasm and thought all was good.

Timnit then reacted by describing her frustrations with how she was treated in an internal diversity mailing list. She also emailed Megan Kacholia with a number of demands, mostly to be treated reasonably. Appalled at how she and her coauthors were treated, she refused to retract the paper. Megan reacted by taking her note that she would work on a resignation date if demands were not met in combination with Timnit's email completely pedantically and out of context, using them as an excuse to fire her by rushing her out, without allowing her to follow the actual resignation process. She also acted over Timnit's manager's head (Samy Bengio), who was so annoyed he later quit. (Megan cc'd Jeff, but hadn't spoken to Jeff about any of this, and was acting on her own.)

Google reacted by gaslighting Timnit to protect its ass. After Timnit Tweeted that Jeff had fired her (Timnit probably really thought that Jeff and Megan had spoken to each other before Megan had sent that email), Jeff participated in this part in public, on Twitter, with a lot of serious consequences for Timnit and others, without considering power dynamics. (Jeff suffered a lot on Twitter, too, but that doesn't excuse not considering power dynamics in such a consequential way on such a consequential medium.) Timnit and others, including me, were harassed and threatened because of this, by way of third-party harassers. I was not even involved on the paper, just proximal damage. I was afraid for my life honestly.

Meg Mitchell, feeling lost, having seen the truth of how Timnit was treated internally, and trusting Jeff to protect her, tried to put together some things for Jeff to get him to see how Timnit was mistreated. She panicked and backed them up on her personal email because she was afraid of retaliation from Google (a reasonable fear---doing any diversity or community work at Google that at all challenges the status quo IME gets you retaliatorily reported to PeopleOps, who then try to get you in trouble and read your private communications and so on). She was transparent about doing this and gave instructions for Google to remove her personal copy if needed. Sundar Pichai fired her and then comms smeared her publicly with outright lies. She was harassed and threatened for this, too, and a number of places refused to hire her because of Google's treatment of her. Really tangible damage emotionally, financially, and reputationally.

Out of fear of being sued, Google's comms and legal departments reacted by continuing to censor and gaslight. Sundar was extremely complicit in this, too. Megan was moved out of Research, but not much else happened; she continues to send monthly emails about diversity, as if her continued contact with Research is not actively harmful to diversity.

So sick of internet people speculating about this without knowing anything about the situation. Sorry if I broke anyone's trust here. Just can't deal with this incorrect speculation anymore.

It's a really absurd opinion that AI will destroy the world, and one that does not deserve serious consideration in any research community. It's only in strange Rationalist corners and the companies in Silicon Valley that echo those corners that this is considered at all "hotly debated."

If you're interested in verification you should probably talk to people who actually work on verification, for example, literally anyone from our research community: https://www.floc2022.org/

I'm not sure how Scott ended up buying the party line of the weird AGI Doomsday Cult but so be it. In any case, none of the things he says about verifying AI in this post make any sense at all, and if OpenAI actually cares about verifying AI and not just about hiring people who believe in the AGI Doomsday party line, probably they should hire verification people. Alas, that is not the point.

I didn't demand anything. I contributed my story to a decision that I along with the rest of the community will make democratically.

I do not believe you are engaging in good faith, given that I just explained to you very clearly and concisely that this is not just about me.

If you can't see the many differences between those situations, I don't feel like we will have a productive conversation.

If I were the only one complaining, I'd agree (with this being unnecessary---I don't quite see how the cost here is very large). But many women in the community both in the US and in France echo my experiences and concerns, as do many men. I also view it as part of my job as incoming faculty to discuss things that students may feel too vulnerable to discuss themselves.

Also, many on the core Coq development teams at Inria just feel this is bad branding for them at this point, as it inhibits adoption of the tool internationally.

Yeah, but sexual words in particular lead to harassment of women by strangers. I'd love to fix society so that this becomes false, but it's not how society currently works.

I'll keep that in mind though if I work with folks in the UK at some point.

My understanding was that it was the icing on the cake to Huet. I'm still not sure that changes much.

Can you explain the Git thing? It keeps coming up but I've never heard of an English word "git." I looked it up and it seems it exists, but is it common? I've lived in this country for 30 years and have never heard it in a nib-technical context.

We are mostly researchers, so this is not so much a language we use as our life's work. This means we talk about it a _lot_, including in public. It's not just about people at work making jokes; it's also about what happens when you leave work and mention what you do in public as a force of habit. It's pretty awful to expect all of us, especially the women in the community, to have to police the behavior of every stranger we encounter who hears us say that we are Coq experts or something similar, and uses that to make jokes at our expense or harass us.

The core team of Coq developers in France has mulled over this for years, but hasn't had enough momentum or interest to push for it. Right now the broader community of contributors and users, myself included, are arguing our points, suggesting name ideas, and attempting to drive some kind of consensus. My understanding is that the final decision will be democratic among users and contributors. Some are projecting weird politics onto this, but the conversation is otherwise proceeding quite civilly and constructively.

Almost all dissenters in the thread (possibly all of them, I don't remember) do not work for Inria, the research institute at which Coq is professionally developed. Though they are community members like me (I am lightly in favor of the change, and I am both a contributor and a user).

> These re-namings always follow the same pattern. Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

Hello, I'm the woman who chimed in with the story of the Uber driver harassing me. I'm not just a Coq expert (check my publications), but also a contributor to the proof assistant (check my Github). Every year during non-pandemic times I go to France for a week for the Coq Users & Developers Workshop, and I am quite close with the team.

I also hear "Coq" before "cock" when people say either of those words, naturally, since I spend so much time working on Coq. Unfortunately, this means that in public I frequently forget that almost everyone who has never heard of it before hears "cock," and this is what most often gets me into bad situations like in the Uber.

The problem isn't that we are community outsiders; it's that you can't imagine us being community insiders.

These problems are more closely related than you imagine. In particular, when you change a program, there is often necessarily more information you must give the computer in order to make the corresponding change in the proof. That additional burden is creativity, and is in many cases unavoidable.

With good proof repair techniques you can fix the proof almost fully automatically in a way that mimics the change in the program, but then just ask the programmer a few questions to give the needed creativity to fix the proofs. As far as easy to understand goes, then, that "just" comes down to good UX for asking those questions. (Still not solved!)

Here is the state of the art right now (my most recent paper): https://arxiv.org/abs/2010.00774

Lots left to do but the dream is quite realistic.

This is my thesis area! If you're interested in proof repair, check out my latest work: https://arxiv.org/abs/2010.00774

More on my website: https://dependenttyp.es/

I hope more people work on this problem. It is a big and promising space. And I'll need students soon :)

Seems he indeed was an international student.

This student was an international student. If he quit, he would have lost his visa and had to leave the country.