Discussion about this post

User's avatar
Mario Pasquato's avatar

More general comments to come, but for now this caught my attention: “Such a tool could help us preserve our field norms around accreditation and authorship by redirecting us to human-written papers rather than feeding the user a sea of assimilated language slop. Imagine if I could type in “What are the L^2-Betti numbers of H^3?” and be directed to a reference written by humans.” As it happens I worked closely with a company that built a RAG (retrieval augmented generation) system of this kind, though trained on the astronomy arxiv corpus. This was built for INAF (the Italian national institute of astrophysics) on a very limited budget. It seems that you would just want to keep the retrieval part and deemphasize or even remove the generation part. Better yet, instead of a RAG it would be interesting to consider some sort of reasoning engine as the backend. Perhaps if there is enough interest we could discuss this. At any rate the technology we need is precisely this kind of AI that yields a centaur/enhanced human rather than aiming at replacing us.

Torgeir Lysen's avatar

Regarding Internal #5:

It might be interesting to also develop tools that only prove theorems in formal languages and not natural language. Unless I’m mistaken this is how AxiomProver works.

I think this helps users mentally separate the work of the LLM from that of the human, which may ultimately mitigate skill atrophy and make intellectual ownership clearer. Translating from a formal language to a natural language would also require the author to understand the proof.

Focusing on developing these tools also gives researchers who want to work on automated theorem proving opportunities to remain in academia.

22 more comments...

No posts

Ready for more?