LLM-verktyg gör matematiska bevis interaktiva och lättare att förstå

arXiv cs.AI

Forskare har byggt ett system som använder LLM:er för att översätta skrivna matematiska bevis till Lean (ett programspråk för maskinverifierade bevis), så att läsaren kan klicka sig igenom varje steg, testa egna exempel och se logiska beroenden. I en användarstudie med 16 deltagare gav de som hade tillgång till de interaktiva funktionerna märkbart bättre och mer detaljerade svar på förståelsefrågor. Det intressanta är poängen att LLM-output i sig är statisk text – det är kopplingen till körbar formell kod som faktiskt möjliggör äkta interaktivitet.