4 papers
Automating Bitvector and Finite Field Equivalence Proofs in Lean
Elizaveta Pertseva, Valentin Robert, Clark Barrett +1
Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and…
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor +4
This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving…
Contrastive Attention Networks for Attribution of Early Modern Print
Nikolai Vogler, Kartik Goyal, Kishore PV Reddy +5
In this paper, we develop machine learning techniques to identify unknown printers in early modern (c.~1500--1800) English printed books. Specifically, we focus on matching uniquel…
Fine-tuned LLMs Know More, Hallucinate Less with Few-Shot Sequence-to-Sequence Semantic Parsing over Wikidata
Silei Xu, Shicheng Liu, Theo Culhane +4
While large language models (LLMs) can answer many questions correctly, they can also hallucinate and give wrong answers. Wikidata, with its over 12 billion facts, can be used to g…