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.
(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.)
Talia, if this was all a misunderstanding from Jeff, then why was Timnit accusing Jeff for the longest possible time. I can understand Megan Kacholia was the main person in all this drama according to you, but the trolling/accusing that we saw in the aftermath was vicious and in poor taste. Honest bystanders who were giving neutral opinions were gaslighted to choose what side they morally belonged.
Why didn't any of you try to stop this verbal carnage? Also if Timnit was largely not at fault, why is that on every social media where any modicum of anonymity is possible, Timnit had been harshly criticized for her conduct.
We respect her contributions to advancement of ML, but that conduct was inexorable & in very poor taste.
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 emotionally want to defend Jeff, and it's hard to defend Jeff on just the things I believe he ought to be defended for and still hold him accountable, and not gaslight Timnit or minimize what she went through. 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. Even if Jeff genuinely misunderstood, he should have apologized for his role and moved to repair harm, rather than reinforcing and exacerbating harm in his public response.
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 sorry but who are you? Just because you addressed me by name and it feels weird when that happens unless I know who is talking to me.)
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.
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.)
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.
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.
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] :)
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.
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
It's lack of training I think. A good engineer should think about the consequences of her actions. People in the industry, it seems, just don't. Very disappointing.
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.
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.
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.
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.
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.
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."
Why do you think it's absurd? If we do eventually create an AGI that is significantly smarter than us in most domains, why is it that we should expect to be able to keep it under control and doing what we want it to?
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/
This kind of verification is what the other commenter was referring to, but it is very foundational and disconnected from current day-to-day ML aspects. If you're interested in practical, empirical AI safety research, see here for example: http://aisafety.stanford.edu/
They also explain the area of overlap with formal verification in their white paper.
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.
In terms of multiplicity of meanings, certainly. Anyway, if you're interested in my personal opinion on Huet's "humour" and how this degenerated, we can talk privately.
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.
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.
You realise men get harassed by strangers too? All the time, about stupid shit, and rare is the day that anything is done about it.
It's really quite self centred to create new problems for the entire world because of a taxi driver. Think about how many people will now have to double search for things, or change scripts, or waste time because they didn't realise new tool=old tool. It's a huge new technical debt being created here. Coq is software, it's been around for many years, so the old name will never die. People will be dealing with half baked renames and duplications forever.
Immature people will find ways to be immature and annoying no matter what - the difference between adults and children is we're supposed to be able to deal with it and keep things in proportion. That doesn't seem to be happening here and it's a pity.
And yet your demands have contributed to that decision.
Please don't accuse others of "not engaging in good faith" when they just outlined to you the rational basis for their viewpoints. It's just an ad-hominem insult. My engagement is in entirely good faith: I think you (and others making these demands) are refusing to consider the impact of your demands on other people, externalizing costs unnecessarily and generally acting in anti-social ways, whilst claiming the exact opposite.
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.
A guy I work with has 'balls' in his name. Yes, he and management expect people to keep their mouths shut.
Anyways, yes we could require him to change his name because it's distracting. That would be one thing to do. It's the solution suggested by people in this thread...
