5 papers
Reformalization of the Jordan Curve Theorem
Simon Guilloud, Sankalp Gambhir, Samuel Chassot
We present a case study in reformalization, a variant of autoformalization in which the input proof is not natural language but a formal development in a different proof assistant.…
LISA -- A Modern Proof System
Simon Guilloud, Sankalp Gambhir, Viktor KunÄak
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof che…
Interpolation and Quantifiers in Ortholattices
Simon Guilloud, Sankalp Gambhir, Viktor KunÄak
We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical…
Byte BPE Tokenization as an Inverse string Homomorphism
Saibo Geng, Sankalp Gambhir, Chris Wendler +1
Tokenization is an important preprocessing step in the training and inference of large language models (LLMs). While there has been extensive research on the expressive power of th…
Could ChatGPT get an Engineering Degree? Evaluating Higher Education Vulnerability to AI Assistants
Beatriz Borges, Negar Foroutan, Deniz Bayazit +87
AI assistants are being increasingly used by students enrolled in higher education institutions. While these tools provide opportunities for improved teaching and education, they a…