tlringer

7 ms·

1.
by tlringer 3y ago
Every DeepMind press release is like this.
2.
by tlringer 3y ago
(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&
3.
by tlringer 3y ago
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 y
4.
by tlringer 4y ago
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 t
5.
by tlringer 4y ago
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 ethic
6.
by tlringer 4y ago
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.
7.
by tlringer 4y ago
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 o
8.
by tlringer 4y ago
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
9.
by tlringer 4y ago
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 o
10.
by tlringer 4y ago
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
11.
by tlringer 4y ago
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.
12.
by tlringer 4y ago
Incorrect. https://news.ycombinator.com/item?id=34382901#34385678
13.
by tlringer 4y ago
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 pa
14.
by tlringer 4y ago
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 tho
15.
by tlringer 4y ago
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/
16.
by tlringer 4y ago
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 verify
17.
by tlringer 5y ago
I didn't demand anything. I contributed my story to a decision that I along with the rest of the community will make democratically.
18.
by tlringer 5y ago
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.
19.
by tlringer 5y ago
If you can't see the many differences between those situations, I don't feel like we will have a productive conversation.
20.
by tlringer 5y ago
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
21.
by tlringer 5y ago
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 i
22.
by tlringer 5y ago
My understanding was that it was the icing on the cake to Huet. I'm still not sure that changes much.
23.
by tlringer 5y ago
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
24.
by tlringer 5y ago
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 w
25.
by tlringer 5y ago
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, su
26.
by tlringer 5y ago
> 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
27.
by tlringer 6y ago
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 addition
28.
by tlringer 6y ago
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 thi
29.
by tlringer 6y ago
Seems he indeed was an international student.
30.
by tlringer 6y ago
This student was an international student. If he quit, he would have lost his visa and had to leave the country.

More ›