Lean und LLMs: Automatisierte Beweise machen dependent types praktisch
We have proof automation now
Adam Langley zeigt anhand eines Zstandard-Dekompilierers in Lean, wie LLMs die Beweislast dependent typisierter Sprachen drastisch reduzieren können. Er erklärt die Grundlagen der Entropiekodierung in Zstandard und argumentiert, dass die Kombination aus LLMs und Beweisirrelevanz die praktische Nutzung solcher Sprachen ermöglicht.
Potentiell machen LLMs dependent-type-Systeme plötzlich dramatisch praktischer.