Software Engineer: Keystone Project (Machine-Verified LLM Inference)

EPFL, das Schweizerische Bundesinstitut für Technologie in 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 Forscher aus mehr als 120 verschiedenen Ländern.

Mission

Das Keystone-Projekt, eine von ARIA finanzierte Zusammenarbeit zwischen der EPFL und dem Imperial College London, zielt darauf ab, eine formal verifizierte ML-Inferenz-Engine zu entwickeln, die zeigt, dass KI helfen kann, verifizierte Systeme in Bezug auf Entwicklungsaufwand, Funktionen und Leistung wettbewerbsfähig mit unverifizierten Systemen zu machen. Zu den Aufgaben gehören das Design und die Implementierung von verifizierten Inferenzkomponenten, die Formalisierung der GPU-Kernel-Semantik, die Entwicklung von KI-unterstützten Proof-Engineering-Workflows und die Open-Source-Veröffentlichung von Spezifikationen, Beweisen und verifizierten Artefakten.

Wir suchen einen hervorragenden Software-Ingenieur, der eine zentrale Rolle dabei spielt, verifizierte Forschungsprototypen in eine produktionsreife, leistungsstarke Inferenz-Engine umzuwandeln. Vorherige Erfahrungen mit formaler Verifikation sind willkommen, aber nicht erforderlich: Ein starker Systemingenieur mit der Motivation, die Technologie von Beweisassistenten zu erlernen, wird in dieser Rolle gedeihen.

Hauptaufgaben und Verantwortlichkeiten

• Technische Expertise in Systems Programming und Performance Engineering zur Unterstützung der Forschungsprojekte einbringen; Zusammenarbeit mit den Forschungsteams an der EPFL und dem Imperial College London.
• Kernkomponenten der verifizierten LLM-Inferenz-Engine entwerfen, implementieren und warten, einschließlich der Laufzeit und des Verbindungs-Codes, der extrahierten verifizierten Codes, GPU-Kernels und Treibern.
• Die Ingenieurinfrastruktur des Projekts organisieren und verwalten: differenzielle Tests gegen Referenz-Engines (vLLM, SGLang), kontinuierliche Integration für Code und Beweise sowie Leistungsbenchmarking.
• Agentische KI-Pipelines für die automatisierte Formalisierung von Spezifikationen, die Generierung von Beweisen und die Reparatur von Beweisen entwickeln und pflegen.
• Dokumentation, Verfahren und Empfehlungen schreiben, um die Reproduzierbarkeit der Artefakte des Projekts sicherzustellen.
• Fehler und Regressionen im gesamten Software-Stack diagnostizieren, verhindern und beheben.
• Das Sicherheitsniveau und die vertrauenswürdige Computing-Basis der entwickelten Komponenten analysieren und zu Red/Blue-Team-Übungen im Rahmen des ARIA-Programms beitragen.
• Zu Open-Source-Veröffentlichungen beitragen und sich mit deren Benutzer-Communities engagieren.

Profil

• Höherer Abschluss in Informatik oder gleichwertiger Ausbildung; Erfahrung im Bereich.
• Ausgezeichnete technische Kenntnisse in Systems Programming und starke Programmierfähigkeiten in mehreren der folgenden Sprachen: Python, C/C++, Rust, OCaml oder anderen funktionalen Sprachen.
• Kenntnisse in einem oder mehreren der folgenden Bereiche mit starker Motivation, in den anderen zu wachsen: GPU-Programmierung (CUDA, Triton, PTX) oder Hochleistungsrechnen; ML-Inferenz- oder Serviersysteme (vLLM, SGLang, PyTorch-Interna oder ähnliches); Interaktive Theorembeweise (Rocq, Lean, HOL, Isabelle oder ähnliches) oder andere formale Methoden.
• Erfahrung in der Wartung von Entwicklungstools: Build-Systeme, kontinuierliche Integration und Testinfrastruktur.
• Erfahrung mit LLM-basierten Entwicklungstools oder dem Aufbau agentischer Workflows ist von Vorteil.
• Beherrschung der englischen Sprache unerlässlich (mündlich und schriftlich); Französisch ist von Vorteil, aber nicht erforderlich.
• Prioritäten setzen, Integrität und Autonomie in der Arbeit.
• Teamgeist und Eignung für technische Untersuchungen und Implementierungen; ausgezeichnete Kommunikationsfähigkeit mit unterschiedlichen Zielgruppen, von Beweisingenieuren bis hin zu Systemforschern.
• Starkes Servicebewusstsein und Initiative.

Wir bieten

• Die Möglichkeit, einem dynamischen und stimulierenden Team in einem hochkarätigen, von ARIA finanzierten Projekt beizutreten.
• Ein multikulturelles und akademisches Arbeitsumfeld von hoher Qualität.
• Chancen zur Weiterbildung und beruflichen Entwicklung.
• Exzellente Arbeitsbedingungen.
• Großzügiger Zugang zu modernen KI-Modellen und Hochleistungsrechnern.
• Finanzierte Reisen zur Zusammenarbeit zwischen Lausanne und London sowie zu Konferenzen.

Informationen

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

Vertragsbeginn: nach Vereinbarung.

Aktivitätsrate: 100,00%

Vertragsart: CDD

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