EPFL sucht Postdoc für Algorithmen und formale Verifikation

Die Lehrstuhlgruppe Numerische Modellierung und Simulation der Eidgenössischen Technischen Hochschule Lausanne in der Schweiz hat eine Postdoc-Stelle mit Fokus auf formale Verifikation und KI-gestützte Algorithmenentdeckung für die numerische Analyse ausgeschrieben. Die Position zielt darauf ab, die Integration fortschrittlicher formaler Methoden und künstlicher Intelligenz in die numerische Behandlung partieller Differentialgleichungen systematisch zu erforschen und in den akademischen Alltag zu überführen. Der Aufgabenschwerpunkt besteht im Aufbau und in der strategischen Ausrichtung einer neuen Forschungslinie. Im Zentrum steht die empirische Untersuchung, wo Werkzeuge wie das mathematische Proof-Assistant-System Lean sowie moderne KI-Modelle das Design und die Analyse numerischer Schemata konkret voranbringen und wo aktuelle methodische Grenzen liegen. Vorgesehene Arbeitspfade umfassen die formale Formalisierung und Verifikation von Stabilitäts- und Fehlerabschätzungen für Finite-Elemente-Methoden sowie die KI-unterstützte Generierung neuer Diskretisierungsparadigmen für PDE-Fragestellungen, in denen Standardverfahren ineffizient versagen. Die entdeckten Algorithmen werden im Anschluss durch maschinenprüfbare formale Beweise abgesichert. Die EPFL betont dabei die enge Verzahnung von numerischer Simulation und geometrischer Modellverarbeitung. Die besetzende Person trägt die Verantwortung für die eigenständige Experimentplanung, die internationale Publikation der Ergebnisse sowie deren Präsentation auf Fachkonferenzen. Das Projekt ist bewusst offen konzipiert und erfordert keine starre Vorgabe zu Beginn. Die konkrete Forschungsrichtung soll sich dynamisch durch Pilotexperimente und iteratives Feedback innerhalb der Gruppe entwickeln. Die Bewerbung ist mit flexibel handhabbarem Starttermin und bis zur tatsächlichen Stellenbesetzung laufend offen. Anforderung sind ein Lebenslauf, ein Motivationsschreiben zur Skizzierung einer konkreten Forschungsfrage an der Schnittstelle numerischer Analyse, formaler Verifikation und Algorithmenentdeckung sowie die Kontaktdaten zweier Referenzpersonen. Die Ausschreibung verfolgt das strategische Ziel, den Wandel in der angewandten Mathematik und wissenschaftlichen Informatik durch den verstärkten Einsatz verifizierbarer Formalismen und intelligenter Suchverfahren zu beschleunigen und damit robuste Simulationswerkzeuge für komplexe ingenieurwissenschaftliche und naturwissenschaftliche Problemstellungen zu etablieren.