Postdoc: Keystone Project (Machine-Verified LLM Inference) in Lausanne

EPFL, die Eidgenössische Technische Hochschule Lausanne, ist einer der dynamischsten Universitätsstandorte in Europa und gehört zu den 20 besten Universitäten weltweit. Die EPFL beschäftigt mehr als 6.500 Personen, die die drei Hauptmissionen der Institutionen unterstützen: Bildung, Forschung und Innovation. Der EPFL-Campus bietet ein außergewöhnliches Arbeitsumfeld im Herzen einer Gemeinschaft von mehr als 18.500 Menschen, darunter über 14.000 Studierende und 4.000 Forschende aus mehr als 120 verschiedenen Ländern.

Mission

Das Keystone-Projekt zielt darauf ab, Wissen in den folgenden Bereichen voranzubringen:

• Formale Verifikation und interaktive Theorembeweise (Rocq, Lean)
• Sichere und leistungsstarke Computersysteme, einschließlich ML-Infrastruktur

Wir suchen herausragende Kandidaten, die in formalen Methoden und/oder Computersystemen arbeiten und Interessen in einem oder mehreren der folgenden Bereiche haben: maschinengeprüfte Verifikation von Systemsoftware, GPU-Kernel-Semantik und -Verifikation sowie KI-unterstützte Beweisführung.

Die Position ist Teil einer ARIA-finanzierten Zusammenarbeit zwischen EPFL und Imperial College London, deren Ziel es ist, eine formal verifizierte ML-Inferenzmaschine zu entwickeln, die zeigt, dass KI helfen kann, verifizierte Systeme hinsichtlich Entwicklungsaufwand, Funktionen und Leistung wettbewerbsfähig zu machen.

Hauptaufgaben und Verantwortlichkeiten

• Durchführung von Forschungsarbeiten im Zusammenhang mit dem Keystone-Projekt, einschließlich der Mitgestaltung und Konstruktion einer maschinenverifizierten LLM-Inferenzmaschine. Der genaue Fokus wird mit dem erfolgreichen Kandidaten je nach Hintergrund, Fachwissen und Vorlieben besprochen.
• Mögliche Richtungen umfassen:
• Formalisation der GPU-Kernel-Semantik (z.B. PTX/Triton) in einem Beweisassistenten und Verifikation von hochleistungsfähigen Inferenzkernen (numerische Genauigkeit, Speichersicherheit, Datenrennenfreiheit, funktionale Korrektheit)
• Implementierung und Verifikation der Inferenzkoordinationsschicht (Batching, KV-Cache-Management, Scheduling) in Rocq/Lean mit Extraktion in ausführbaren Code
• Entwicklung agentischer KI-Workflows zur automatischen Formalisierung von Spezifikationen, Beweisgenerierung und Beweisreparatur
• Aufbau eines starken Netzwerks in den Bereichen formale Verifikation, Systeme und ML-Infrastruktur, einschließlich enger Zusammenarbeit mit dem Team des Imperial College London (regelmäßige Besuche in London werden erwartet)
• Beitrag zu Open-Source-Veröffentlichungen von Spezifikationen, Beweisen und verifizierten Artefakten
• Engagement im ARIA-Programm, einschließlich Red/Blue-Team-Übungen und Sprint-Reviews

Profil

• PhD (oder kurz vor Abschluss) in Informatik oder einem eng verwandten Bereich
• Hintergrund in formaler Verifikation, Programmiersprachen, Systemen oder ML
• Forschungserfahrung in einem oder mehreren der folgenden Bereiche: interaktive Theorembeweise (Rocq, Lean, HOL, Isabelle oder ähnlich), GPU-Programmierung oder Semantik, Compiler, Parallelität oder ML-Systeme (z.B. vLLM, SGLang oder ähnliche Inferenzmaschinen)
• Starke rechnerische und analytische Fähigkeiten, einschließlich solider Software-Engineering-Fähigkeiten in mehreren Sprachen (z.B. Python, C++, OCaml, funktionale Sprachen)
• Erfahrung mit oder Bewertung von LLM-basierten Werkzeugen zur Code- oder Beweisgenerierung ist von Vorteil
• Publikationsrekord (relativ zu Ihrem Karriereweg) in international führenden Zeitschriften und Konferenzen
• Unabhängig, kreativ und lösungsorientiert
• Exzellente schriftliche und mündliche Kommunikationsfähigkeiten in Englisch
• Starke Motivation, neue Forschungsbereiche an der Schnittstelle von KI und formalen Methoden zu erkunden
• Guter Teamgeist und Begeisterung für die Arbeit in einem verteilten, multi-institutionellen Team

Wir bieten

• Ein stimulierendes und internationales Arbeitsumfeld
• Exzellente Arbeitsbedingungen
• Die Möglichkeit, Spitzenforschung in einer der dynamischsten wissenschaftlichen Institutionen Europas innerhalb eines hochkarätigen ARIA-finanzierten Projekts durchzuführen
• Die Möglichkeit, mit international anerkannten Experten an der EPFL und dem Imperial College London sowie mit einem starken Team von Postdoktoranden und Doktoranden zu interagieren
• Großzügiger Zugang zu fortschrittlichen KI-Modellen und Hochleistungsrechnern für Beweisassistenten-Arbeiten
• Finanzierte Reisen für die Zusammenarbeit zwischen Lausanne und London sowie für Konferenzen

Informationen

Für weitere Informationen kontaktieren Sie bitte: Nate Foster.

Vertragsbeginn: , oder nach Vereinbarung

Aktivitätsrate: 100.00

Vertragsart: CDD

Dauer: 1 Jahr, verlängerbar (je nach Projektlaufzeit)