36 citations · 37 across the 8 of their papers we have counts for
9 papers
Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs
Lazar Milikic, Etienne Bamas, Emmanuel Abbe +1
Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts often leave GPUs waiting and withhold rewards from potentiall…
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Lazar Milikic, Simon Guilloud, Khanh Nguyen +1
We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects. Recent verifier-in-the-loop systems show that la…
Orthologic for SAT Solving
Vladislas de Haldat, Simon Guilloud, Viktor Kunčak
We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementati…
Are Dependent Types in Set Theory Feasible?
Yunsong Yang, Simon Guilloud, Viktor Kunčak
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, wi…
RLMEval: Evaluating Research-Level Neural Theorem Proving
Auguste Poiroux, Antoine Bosselut, Viktor Kunčak
Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still…
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…
Orthologic Type Systems
Simon Guilloud, Viktor Kunčak
We propose to use orthologic as the basis for designing type systems supporting intersection, union, and negation types in the presence of subtyping assumptions. We show how to ext…
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…
Mechanized HOL Reasoning in Set Theory
Simon Guilloud, Sankalp Gambhir, Andrea Gilot +1
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant f…