[freyr]

I suspect it was Timnit’s behavior after the paper didn’t pass internal review that actually got her fired (issuing an ultimatum and threatening to resign unless the company met her demands; telling her coworkers to stop writing documents because their work didn’t matter; insinuations of racist/misogynistic treatment from leadership when she didn’t get her way).

[visarga]

I think it was a well calculated career move, she wanted fame, she got what she wanted. Now she's leading a new research institute

> We are an interdisciplinary and globally distributed AI research institute rooted in the belief that AI is not inevitable, its harms are preventable, and when its production and deployment include diverse perspectives and deliberate processes it can be beneficial. Our research reflects our lived experiences and centers our communities.

https://www.dair-institute.org/about

[tlringer]

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.)

Interestingly, Timnit's email to the diversity list was so resonant that several of the changes it asked for in how Google approaches diversity were enacted after her firing. But Megan and Google's official line on all of this chose to obsess over Timnit's rhetorical devices and take them literally instead, using an email to a diversity list about diversity against her. People are still too afraid to talk about diversity on diversity lists, now, because of Google using that email against her.

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. (I have extremely thorough information about this, but to those directly involved, please feel free to correct me about any details I got wrong, or about important details I omitted.)

[YeGoblynQueenne]

Cheers. That's way much more information than I ever wanted to know about that sorry affair. If it can quell the torrent of ad-hominems, it's worth it, but I doubt it. All those hardcore soft. engineers here on HN who spend 99.99999% of uptime close to the bare metal think that people like Gebru who work on ethics are useless hangers-on without any "real contributions" (probably because none of them has bothered to check her background on wikipedia).

Nevertheless, hoping to check your sources I clicked through your profile and I have a question, totally unrelated to all this. Can you say something about the state of the art in "neural proof synthesis"? To clarify, I'm scare-quoting because I didn't even know that's a thing. For context, my background is in the European tradition of Resolution-based automated theorem proving (Prolog and all that) but also statistical machine learning, so don't worry about simplifying terminology too much.

Btw, the "proof engineering" link in your profile gives me a security alert on firefox.

[tlringer]

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 Yuhuai (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.

[YeGoblynQueenne]

Thanks. I'm a bit more familiar with neural theorem proving. It's an interesting area. For example, if I could train me a model to speed up (NP-complete) θ-subsumption for very long terms that would be a worthy addition to the purely symbolic toolbox I'm more at home with.

Autoformalization also sounds interesting. I've had some conversations about automatically turning big corpora of natural language text into Prolog with language models, for example. I don't reckon anyone is even researching how to do this with symbolic methods at the moment.

I'll check out AITP. Thanks for the pointers. I'm used to small conferences [and to underciting between disciplines] :)

[tlringer]

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.

[YeGoblynQueenne]

And the next one is easy to get to by train from my current location. That's great (I don't fly). Nice.

[tlringer]

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.

[rajup]

I’m sorry but this is a bunch of crock and honestly sounds like just a lot more speculation adding nothing to the conversation.

[tlringer]

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.

[freyr]

None of that disputes what I said or excuses her behavior. The “resonant” email is public, we can’t pretend it was in any way professional or appropriate.

Vanishingly few people can get away with acting like that at work without getting fired. She thought she was an exception and she wasn’t.

[tlringer]

It was fine, unless you reach far enough to take it literally, which is quite obviously not what Timnit intended. The call to stop DEI work was a rhetorical device to highlight to an audience that presumably cares strongly about diversity that the current work is not meaningful without broader systemic change within Google. Plus an emotional plea to what should have been a sympathetic audience to understand how exhausting doing any real diversity work within Google is. This is true and resonant and so triggered a lot of said change after she was fired. The change is still ongoing.

Everyone who tries to actually enact real systemic change within Google Research to improve how women and people of color are treated, or the work environment in general, burns out or gets fired. It is only toeing the company line when it's officially your role to do so, taking extremely conservative actions while ignoring real issues like abuse, harassment, and discrimination, that lets you survive while doing DEI work at Google in Research without burning out or getting fired. The sole exception I know of right now is Kat Heller, god bless her.

The feeling of "none of this is worthwhile, what's the point of any of it" is something everyone who tries to do real diversity and culture work within Google Research or even within the computer science research community more broadly has felt, and a diversity mailing list ought to have been a safe place to share that feeling.

Instead it was used against her. Now nobody feels safe sharing these feelings anywhere within Google Research.

Jeff to his credit is now working on many of these things. As is the DEI committee. I hope they all succeed. But I don't think any of that would have happened without Timnit highlighting these very real issues. It's depressing that she was fired for it. She wanted to change things and keep her job and her team, not to be a martyr.

[freyr]

Timnit’s backpedaling regarding her email and her ultimatum was absurd. You seem completely unwilling to factor Timnit’s own behavior into the chain of events, so it doesn’t make sense to continue this. This elimination of personal responsibility when it’s inconvenient to the narrative has become endemic among the activist employees. To your credit, it seems like your heart is in the right place with wanting to help her and others.