ENProof Engineer, Autoformalisation Engineer
IliadRemote
Mondiale catastrofale risico’sAI-veiligheidSoftware engineeringOnderzoek
Waarom staat dit op het bord
Wiskundig onderzoek naar de veiligheid van AI-systemen hangt af van bewijzen die echt kloppen, en die met de hand nakijken kan onderzoekers maanden kosten. Als jij een systeem bouwt dat hun voorstellen omzet in bewijzen die een computer kan controleren (in de bewijstaal Lean), werkt elke onderzoeker die het gebruikt sneller en met minder kans op een verborgen fout.
Dit bord is in bèta en dit is ons oordeel. Denk je dat we het mis hebben, laat het weten. Geef feedback · Zo redeneren we
Over de functie
Build and operate an autoformalisation engine using LLM agents to turn mathematical research proposals into formal Lean programmes. - Work with researchers to understand proposals and identify mathematics requiring formalisation into formal programme specifications. - Own engine operation, debugging, and optimisation to ensure definitions and theorems faithfully represent research objectives. - Help researchers use formal programmes for calculations, equation solving, and technique applicatio…
Wil je eerst meer weten?
Begin met onze gratis cursus van zo’n 100 minuten: zes korte delen, in je eigen tempo en zonder aanmelding (Engelstalig). Wil je daarna verder, meld je dan aan voor de EA Fellowship: vijf weken lezen en praten in een kleine groep. Ook gratis, maar selectief.