Postdoc: Keystone Project (Machine-Verified LLM Inference) — EPFL

Vollständige Beschreibung

Mission

Das Keystone-Projekt zielt darauf ab, das Wissen in folgenden Bereichen zu fördern: • Formale Verifikation und interaktives Theoremnachweisen (Rocq, Lean) • Sichere und leistungsstarke Computersysteme, einschließlich ML-Infrastruktur

Wir suchen herausragende Kandidaten, die in formalen Methoden und / oder Computersystemen mit Interessen in einem oder mehreren der folgenden Bereiche arbeiten: maschinengeprüfte Verifizierung von Systemsoftware, GPU-Kernel-Semantik und Verifizierung sowie KI-gestütztes Proof-Engineering.

Die Position ist Teil einer von ARIA finanzierten Zusammenarbeit zwischen EPFL und Imperial College London, deren Ziel es ist, eine formal verifizierte ML-Inferenz-Engine zu entwickeln, die zeigt, dass KI dazu beitragen kann, verifizierte Systeme in Bezug auf Entwicklungsaufwand, Funktionen und Leistung wettbewerbsfähig zu machen.

Hauptbestandteil • Durchführung von Forschungsarbeiten im Zusammenhang mit dem Keystone-Projekt, einschließlich eines Beitrags zum Entwurf und Bau eines maschinell verifizierten LLM-Inferenzmotors. Der genaue Fokus wird mit dem erfolgreichen Kandidaten je nach Hintergrund, Fachwissen und Affinitäten besprochen. Mögliche Richtungen sind: • Formalisierung der GPU-Kernel-Semantik (z. B. PTX / Triton) in einem Proof-Assistenten und Verifizierung von Hochleistungs-Inferenzkernel (numerische Genauigkeit, Speichersicherheit, Datumsrennenfreiheit, funktionale Korrektheit) • Implementierung und Verifizierung der Inferenz-Koordinationsschicht (Batching, KV-Cache-Management, Scheduling) in Rocq/Lean, mit Extraktion zu ausführbarem Code • Entwicklung von Agentsc AI-Workflows für Spezifikations-Autoformalisierung, Proof-Generierung und Proof-Reparatur • Aufbau eines starken Netzwerks in den Bereichen formale Verifikation, Systeme und ML-Infrastruktur, einschließlich der engen Zusammenarbeit mit dem Team des Imperial College London (regelmäßige Besuche in London werden erwartet) • Beitrag zu Open-Source-Veröffentlichungen von Spezifikationen, Nachweisen und verifizierten Artefakten • Engagieren Sie sich am ARIA-Programm, einschließlich rot/blauer Teamübungen und Sprint-Reviews

Profil

• PhD (oder kurz vor dem Abschluss) in der Informatik oder einem eng verwandten Bereich • Hintergrund in formaler Verifikation, Programmiersprachen, Systemen oder ML • Forschungserfahrung in einem oder mehreren von: interaktiver Theoremprüfung (Rocq, Lean, HOL, Isabelle oder ähnliche), GPU-Programmierung oder Semantik, Compilern, Parallelität oder ML-Systemen (z. B. vLLM, SGLang oder ähnliche Inferenz-Engines) • Starke Rechen- und Analysefä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 Tools für die Code- oder Beweisgenerierung ist ein Plus • Publikationsaufzeichnung (relativ zu Ihrem Berufspraktikum) in organisierten führenden Zeitschriften und Konferenzen • Unabhängig, kreativ und lösungsorientiert • Hervorragende schriftliche und mündliche Kommunikationsfähigkeiten in Englisch • Starke Motivation, neue Forschungsdomänen an der Schnittstelle von KI und formalen Methoden zu erkunden • Guter Teamgeist und Klärung für die Arbeit in einem verteilten, multi-institutionellen Team

Wir bieten

• Ein anregendes und internationales Arbeitsumfeld • Ausgezeichnete Arbeitsbedingungen • Möglichkeit zur Durchführung modernster Forschung in einer der dynamischsten wissenschaftlichen Einrichtungen in Europa im Rahmen eines hochkarätigen ARIA-finanzierten Projekts • Gelegenheit zur Interaktion mit renommierten Experten EPFL und Imperial College London und mit einem starken Team von Postdoktoranden und Doktoranden • Großzügiger Zugriff auf Frontier-Modelle und Hochleistungs-Compute für proof-assistant Workloads • Geförderte Reisen für die Zusammenarbeit zwischen Lausanne und London und für Konferenzen

Information

Nur über die Online-Plattform eingereichte Bewerbungen werden berücksichtigt. Sie werden gebeten, Folgendes zu liefern: • Ein kurzes Anschreiben (pdf, bis zu 2 Seiten).

Und in einem PDF

• Ein Lebenslauf mit einer Publikationsliste. • Eine Forschungserklärung (pdf, bis zu 3 Seiten). • Kontaktangaben für 3 Berichte.

Für weitere Informationen kontaktieren Sie bitte: Nate Foster (n)

Fragen zu dieser Stellenanzeige