Hallo zusammen und herzlich willkommen zu einer neuen Folge von "Knowledge Science Pulse"! Wir beschäftigen uns heute mit zwei spannenden wissenschaftlichen Papers zum Thema Künstliche Intelligenz und Language Models. Mit dabei ist wie immer mein Kollege Carsten. Hi Carsten!
####
Moin Sigurd, freut mich auch! Ich bin schon ganz gespannt was wir heute lernen werden. Um welche Papers geht es denn genau?
####
Wir schauen uns zwei Papers an. Das erste mit dem Titel "Towards Large Language Models as Copilots for Theorem Proving in Lean" untersucht, wie große Sprachmodelle Menschen beim Beweisen mathematischer Theoreme unterstützen können.
####
Interessant! Also nicht komplett automatisch beweisen, sondern den Mathematikern assistieren sozusagen. Wie machen die Autoren das genau?
####
Sie haben ein Framework namens "Lean Copilot" entwickelt, mit dem Language Models Inferenzen direkt in Lean durchführen können. Damit lassen sich verschiedene Tools bauen, zum Beispiel welche die Beweisschritte vorschlagen, bei Teilzielen helfen oder relevante Prämissen auswählen. Die Modelle laufen dabei entweder lokal mit einer C++ Bibliothek oder auf einem Server.
####
Das klingt nach einem sehr praktischen Ansatz. Dann arbeiten Mensch und KI also nahtlos in der gewohnten Lean-Umgebung zusammen. Wie waren denn die Ergebnisse im Vergleich mit den bisherigen regelbasierten Ansätzen?
####
Die Autoren haben ihr System in Lean-Übungsaufgaben getestet. Im Vergleich zur rein manuellen Beweisführung und zu regelbasierten Methoden konnten sie mit dem Lean Copilot mehr Theoreme beweisen und den menschlichen Aufwand stärker reduzieren.
####
Ein vielversprechender neuer Ansatz, das Mensch-KI-Teamwork. Was steht denn in den anderen Paper?
####
Das zweite Paper mit dem schönen Titel "LONG EMBED: Extending Embedding Models for Long Context Retrieval" geht es um textuelle Embedding-Modelle. Die sind bisher meist auf eine Kontextlänge von maximal 512 Token beschränkt. Die Autoren erforschen nun, wie man diese Modelle auch für Dokumente mit tausenden Wörtern einsetzen kann.
####
Ach ja, Embeddings sind super wichtig fürs Information Retrieval und für Retrieval-augmentiertes Generieren. Wie haben die Autoren es geschafft die Kontextlänge so massiv zu erweitern?
####
Sie wenden verschiedene Methoden an, um die Kontextlänge bestehender Modelle ohne zusätzliches Training um ein Vielfaches zu verlängern. Dazu haben sie auch einen neuen Benchmark namens "LONGEMBED" entwickelt mit synthetischen und echten Retrieval-Tasks.
####
Und was waren die spannendsten Ergebnisse auf diesem LONGEMBED Benchmark?
####
Sie konnten Modelle mit 512 Kontext auf bis zu 4096 Token und Modelle mit 4096 auf bis zu 32.768 Token erweitern. RoPE-basierte Modelle ließen sich dabei besser skalieren als solche mit absoluter Positionskodierung. Die Genauigkeit wurde um bis zu 20% verbessert verglichen mit den Originalmodellen.
####
Wow, das ist ein massiver Fortschritt! Damit eröffnen sich ganz neue Anwendungsmöglichkeiten für textuelle Embeddings. Beim letzten Paper geht es dagegen um Multimodalität, oder?
####
Genau, im dritten Paper...Moment mal...Carsten, ich glaube das Paper haben wir gar nicht in dieser Runde dabei! Meines Wissens wollten wir uns heute nur die beiden Papers zu Theorem Proving und Long Embeddings ansehen.
####
Oh, sorry, da habe ich wohl was durcheinander gebracht! Aber die beiden Papers hatten es auch echt in sich. Für mich ist das Fazit: Große Sprachmodelle werden immer besser darin eng mit Menschen zusammenzuarbeiten, sei es beim Theoreme beweisen oder bei immer längeren Texten. Das wird noch viele spannende Anwendungen ermöglichen!
####
Da stimme ich dir voll zu! Es bleibt spannend die Entwicklungen zu verfolgen. Vielen Dank an unsere Hörer fürs Zuhören. Wir hören uns dann bei der nächsten Ausgabe des "Knowledge Science Pulse" wieder. Bis dahin, macht es gut!
####
Tschüss zusammen!