Related papers: TableauxRocq: A Deep Embedding of Free-Variable Ta…
The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and…
{log} ('setlog') is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FSTRA). As such, it can be used as an automated theorem prover (ATP) for this theory. {log} is able to automatically…
Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…
G\"odel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction…
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP…
As machine learning is increasingly used in essential systems, it is important to reduce or eliminate the incidence of serious bugs. A growing body of research has developed machine learning algorithms with formal guarantees about…
Foundational verification considers the functional correctness of programming languages with formalized semantics and uses proof assistants (e.g., Coq, Isabelle) to certify proofs. The need for verifying complex programs compels it to…
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the…
We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. All of our proofs have been…
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and…
Sharing of notations and theories across an inheritance hierarchy of mathematical structures, e.g., groups and rings, is important for productivity when formalizing mathematics in proof assistants. The packed classes methodology is a…
We describe a "top down" approach for automated theorem proving (ATP). Researchers might usefully investigate the forms of the theorems mathematicians use in practice, carefully examine how they differ and are proved in practice, and code…
Cell injection is an approach used for the delivery of small sample substances into a biological cell and is widely used in drug development, gene injection, intracytoplasmic sperm injection (ICSI) and in-virto fertilization (IVF). Robotic…
Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…
Hallucination remains a major challenge for the safe and trustworthy deployment of large language models (LLMs) in factual content generation. Prior work has explored confidence estimation as an effective approach to hallucination…
The output of an automated theorem prover is usually presented by using a text format, they are often too heavy to be understood. In model checking setting, it would be helpful if one can observe the structure of models and the verification…
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This…
While Large Language Models (LLMs) have demonstrated strong math reasoning abilities through Reinforcement Learning with *Verifiable Rewards* (RLVR), many advanced mathematical problems are proof-based, with no guaranteed way to determine…
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained…
We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional methods that rely on run-time generation and checking of proofs, we use verified-correct procedures with…