[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]

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

[YeGoblynQueenne]

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.