EUROPROOFNET-WG5: THEOREM PROVING AND MACHINE LEARNING IN THE AGE OF LLMS

A
Alekseev, Stanislav	Are LLMs Ready for Software Verification?
Alhessi, Yousef	Neuro-Symbolic Lemma Conjecturing
Axelrod, Guy	Intrinsic Motivation To Construct Terms In A Dependent Type Theory
B
Barket, Rashid	Transformers to Predict the Applicability of Symbolic Integration Routines
Baudart, Guillaume	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Beckert, Bernhard	Towards LLM-support for Deductive Verification of Java Programs
Benzmüller, Christoph	The Fatio Protocol for Formal Dialogue in Isabelle/HOL
Berezun, Daniil	Are LLMs Ready for Software Verification?
Bernardy, Jean-Philippe	Structure-Aware Neural Representations of Agda Programs
E
Einarsdóttir, Sólrún Halla	Neuro-Symbolic Lemma Conjecturing
Engel, Igor	Are LLMs Ready for Software Verification?
England, Matthew	Transformers to Predict the Applicability of Symbolic Integration Routines
F
Fernando, Tim	Between min cost search and least action
Fikiori, Alexandra	On Abstract Logics for Interacting Provers
First, Emily	Neuro-Symbolic Lemma Conjecturing
Freer, Cameron	Autoformalization and autoinformalization via probabilistic reasoning
G
Gallego Arias, Emilio Jesús	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Gandolfi, Alberto	How LLMs could Fool a Proof Checker: The Risks of Inconsistent Assumptions in Automated Proof Systems
Gerhard, Jürgen	Transformers to Predict the Applicability of Symbolic Integration Routines
Gkantzounis, Asterios	On Abstract Logics for Interacting Provers
Goc, Daniel Sebastian	Proof By Abduction in Isabelle/HOL
Granberry, George	Neuro-Symbolic Lemma Conjecturing
H
Huerta Y Munive, Jonathan Julian	DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant
J
Johansson, Moa	Intrinsic Motivation To Construct Terms In A Dependent Type Theory Neuro-Symbolic Lemma Conjecturing
K
Khramov, Nikita	CoqPilot benchmarking framework
Kogkalidis, Konstantinos	Structure-Aware Neural Representations of Agda Programs
Kozyrev, Andrei	CoqPilot benchmarking framework
L
Lelarge, Marc	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Lew, Alexander	Autoformalization and autoinformalization via probabilistic reasoning
Lisitsa, Alexei	In search of simplicity: a case study in ML and LLM assisted applications of ATP in mathematics
M
Mansinghka, Vikash	Autoformalization and autoinformalization via probabilistic reasoning
Melkonian, Orestis	Structure-Aware Neural Representations of Agda Programs
Mežnar, Sebastian	Kernel-level expression generator
Milanese Jr., Roberto	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
N
Nagashima, Yutaka	Proof By Abduction in Isabelle/HOL
Naskręcki, Bartosz	From Mathematical Theory to Machine Learning: Detecting Symmetry Groups in Crystallographic Tilings
Niehaus, Lukas	Reinforcement Learning for Term Rewrite Systems
O
O'Donnell, Timothy	Autoformalization and autoinformalization via probabilistic reasoning
Obua, Steven	Abstraction Logic Is All You Need
P
Pantsar, Markus	The need for ethical guidelines in mathematical research in the time of generative AI
Pasetto, Luca	The Fatio Protocol for Formal Dialogue in Isabelle/HOL
Pease, Adam	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
Petrovčič, Job	Kernel-level expression generator
Podkopaev, Anton	CoqPilot benchmarking framework Are LLMs Ready for Software Verification?
R
Rawiel, Robin	Reinforcement Learning for Term Rewrite Systems
S
Schulz, Stephan	Automated Theorem Provers as the Hub of the AI Math Ecosystem
Shafiq, Uzma	Transformers to Predict the Applicability of Symbolic Integration Routines
Shefer, Aleksandr	Are LLMs Ready for Software Verification?
Silvi, Andrea	Intrinsic Motivation To Construct Terms In A Dependent Type Theory
Singley, Jarrad	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
Sinkarovs, Artjoms	Correct by Construction Machine Learning
Skarpelos, Foivos	On Abstract Logics for Interacting Provers
Smallbone, Nicholas	Neuro-Symbolic Lemma Conjecturing
Solovev, Gleb	CoqPilot benchmarking framework
Starikova, Irina	Mathematics and Creative AI
Stefaneas, Petros	On Abstract Logics for Interacting Provers
T
Teodorescu, Laetitia	NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving
Teuber, Samuel	Towards LLM-support for Deductive Verification of Java Programs
Thompson, Richard	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
Todorovski, Ljupčo	Kernel-level expression generator
Toutsios, Angelos	Formalizing Natural Language: Cultivating LLM Translations Using Automated Theorem Proving
V
Verbitskaia, Ekaterina	Are LLMs Ready for Software Verification?
Viennot, Jules	MiniF2F in Rocq: Automatic Translation Between Proof Assistants — A Case Study
X
Xin, Huajian	Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover
Z
Zyskin, Maxim	Chessboard covers and AI.

Disclaimer | Powered by EasyChair Smart Program