Знайомтеся, @duveZK, інженер zkVM у Nexus. Він вивчав логіку та CS, а зараз працює над формальною верифікацією, доведенням з нульовим розголошенням та інфраструктурою, що забезпечує роботу перевіреного штучного інтелекту.

У центрі уваги Таннера – формальна верифікація для штучного інтелекту. «У міру того, як штучний інтелект розгортається в критично важливих системах, ненадійний вихід може бути катастрофічним. Доведена правильність означає формальні та криптографічні гарантії безпеки, конфіденційності та справедливості».

Особливо його захоплює перетин PL, AI та ZK. «Існує реальний імпульс у використанні штучного інтелекту для допомоги в офіційній верифікації — навчанні LLM на даних Lean для створення перевіреної математики та програмного забезпечення».

Повний текст інтерв'ю читайте тут: