Author name cluster

Michael Norrish

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

2 author rows

NeurIPS Conference 2025 Conference Paper

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes

Sean Lamont
Christian Walder
Amir Dezfouli
Paul Montague
Michael Norrish

A key challenge in automated formal reasoning is the intractable search space, which grows exponentially with the depth of the proof. This branching is caused by the large number of candidate proof tactics which can be applied to a given goal. Nonetheless, many of these tactics are semantically similar or lead to an execution error, wasting valuable resources in both cases. We address the problem of effectively pruning this search, using only synthetic data generated from previous proof attempts. We first demonstrate that it is possible to generate semantically aware tactic representations which capture the effect on the proving environment, likelihood of success, and execution time. We then propose a novel filtering mechanism which leverages these representations to select semantically diverse and high quality tactics, using Determinantal Point Processes. Our approach, 3D-Prover, is designed to be general, and to augment any underlying tactic generator. We demonstrate the effectiveness of 3D-Prover on the miniF2F and LeanDojo benchmarks by augmenting popular open source proving LLMs. We show that our approach leads to an increase in the overall proof rate, as well as a significant improvement in the tactic success rate, execution time and diversity. We make our code available at https: //github. com/sean-lamont/3D-Prover.

PDF Details

AAAI Conference 2024 Conference Paper

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving

Sean Lamont
Michael Norrish
Amir Dezfouli
Christian Walder
Paul Montague

Artificial Intelligence for Theorem Proving (AITP) has given rise to a plethora of benchmarks and methodologies, particularly in Interactive Theorem Proving (ITP). Research in the area is fragmented, with a diverse set of approaches being spread across several ITP systems. This presents a significant challenge to the comparison of methods, which are often complex and difficult to replicate. Addressing this, we present BAIT, a framework for the fair and streamlined comparison of learning approaches in ITP. We demonstrate BAIT’s capabilities with an in-depth comparison, across several ITP benchmarks, of state-of-the-art architectures applied to the problem of formula embedding. We find that Structure Aware Transformers perform particularly well, improving on techniques associated with the original problem sets. BAIT also allows us to assess the end-to-end proving performance of systems built on interactive environments. This unified perspective reveals a novel end-to-end system that improves on prior work. We also provide a qualitative analysis, illustrating that improved performance is associated with more semantically-aware embeddings. By streamlining the implementation and comparison of Machine Learning algorithms in the ITP context, we anticipate BAIT will be a springboard for future research.

PDF Details DOI

NeurIPS Conference 2021 Conference Paper

TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning

Minchao Wu
Michael Norrish
Christian Walder
Amir Dezfouli

We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart the derivation from promising alternatives. We implement the framework in the HOL theorem prover. Experimental results show that the framework using learned search strategies outperforms existing automated theorem provers (i. e. , hammers) available in HOL when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.

PDF Details

FormaliSE Conference 2019 Conference Paper

Modular synthesis of verified verifiers of computation with STV algorithms

Milad K. Ghale
Dirk Pattinson
Michael Norrish

Single transferable vote (STV) is a family of preferential voting systems, different instances of which are used in binding elections throughout the world. We give a formal specification of this family, from which we derive fully verified tools that verify the computation for various instances of STV vote counting. These tools validate an execution of an STV vote counting algorithm, based on a transcript of the count. Our framework distils the similarities and differences of various instances of STV and gives a uniform and modular way of synthesising verifiers for its various instances, and provides the flexibility and ease for adapting and extending it to a variety of STV schemes. We minimise the trusted base in correctness of the tools produced by using the HOL4 and CakeML as the technical basis. We first formally specify and verify the tools in HOL4 and then obtain the machine executable versions for the tools by relying on the verified proof translator and the compiler of CakeML. Moreover, proofs that we establish in HOL4 and CakeML are almost completely automated so that new verified instances of STV can be created with no (or minimal) extra proof. Finally, our experimental results with executable code demonstrate feasibility of deploying the framework for verifying real size elections having an STV counting algorithm.

Details

ICAPS Conference 2017 Conference Paper

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds

Mohammad Abdulaziz
Charles Gretton
Michael Norrish

We investigate compositional bounding of transition system diameters, with application in bounding the lengths of plans. We establish usefully-tight bounds by exploiting acyclicity in state-spaces. We provide mechanised proofs in HOL4 of the validity of our approach. Evaluating our bounds in a range of benchmarks, we demonstrate exponentially tighter upper bounds compared to existing methods. Treating both solvable and unsolvable benchmark problems, we also demonstrate the utility of our bounds in boosting planner performance. We enhance an existing planning procedure to use our bounds, and demonstrate significant coverage improvements, both compared to the base planner, and also in comparisons with state-of-the-art systems.

Details

IJCAI Conference 2015 Conference Paper

Exploiting Symmetries by Planning for a Descriptive Quotient

Mohammad Abdulaziz
Michael Norrish
Charles Gretton

We eliminate symmetry from a problem before searching for a plan. The planning problem with symmetries is decomposed into a set of isomorphic subproblems. One plan is computed for a small planning problem posed by a descriptive quotient, a description of any such subproblem. A concrete plan is synthesized by concatenating instantiations of that one plan for each subproblem. Our approach is sound.

PDF Details

CSL Conference 2010 Conference Paper

A Formalisation of the Normal Forms of Context-Free Grammars in HOL4

Aditi Barthwal
Michael Norrish

Abstract We describe the formalisation of the Chomsky and Greibach normal forms for context-free grammars (CFGs) using the HOL4 theorem prover. We discuss the varying degrees to which proofs that are straightforward on pen and paper, turn out to be much harder to mechanise. While both proofs are of similar length in their informal presentations, the mechanised proofs for Greibach normal form blow-up considerably.

Details