Publications

2023

1. TACAS

   Neural Network-Guided Synthesis of Recursive List Functions

   Naoki Kobayashi, and Minchao Wu

   In Tools and Algorithms for the Construction and Analysis of Systems, 2023

   Abs HTML PDF

   Kobayashi et al. have recently proposed NeuGuS, a framework of neural-network-guided synthesis of logical formulas or simple program fragments, where a neural network is first trained based on data, and then a logical formula over integers is constructed by using the weights and biases of the trained network as hints. The previous method was, however, restricted the class of formulas of quantifier-free linear integer arithmetic. In this paper, we propose a NeuGuS method for the synthesis of recursive predicates over lists definable by using the left fold function. To this end, we design and train a special-purpose recurrent neural network (RNN), and use the weights of the trained RNN to synthesize a recursive predicate. We have implemented the proposed method and conducted preliminary experiments to confirm the effectiveness of the method.

2022

1. JAR

   A Bi-directional Extensible Interface between Lean and Mathematica

   Robert Lewis, and Minchao Wu

   Journal of Automated Reasoning, 2022

   Abs HTML PDF

   We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other and providing a flexible interface for extending translation, our connection allows for the exchange of arbitrary information between the two systems. We show how to make use of the Lean metaprogramming framework to verify certain Mathematica computations, so that the rigor of the proof assistant is not compromised. We also use Mathematica as an untrusted oracle to guide proof search in the proof assistant and interact with a Mathematica notebook from within a Lean session. In the other direction, we import and process Lean declarations from within Mathematica. The proof assistant library serves as a database of mathematical knowledge that the CAS can display and explore.

2021

1. NeurIPS

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

   Minchao Wu, Michael Norrish, Christian Walder, and 1 more author

   Thirty-fifth Annual Conference on Neural Information Processing Systems, 2021

   PDF
2. AITP

   Latent Action Space for Efficient Planning in Theorem Proving

   Minchao Wu, and Yuhuai* Wu

   In 6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021

   PDF

2020

1. AITP

   Reinforcement Learning for Interactive Theorem Proving in HOL4

   Minchao Wu, Michael Norrish, Christian Walder, and 1 more author

   In 5th Conference on Artificial Intelligence and Theorem Proving (AITP), 2020

   PDF
2. CPP

   The Lean Mathematical Library

   The mathlib Community (contributed to code base and paper writing)

   In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

   Abs HTML PDF

   This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.

2019

1. ITP

   Verified Decision Procedures for Modal Logics

   Minchao Wu, and Rajeev Goré

   In 10th International Conference on Interactive Theorem Proving (ITP 2019), 2019

   Abs HTML PDF

   We describe a formalization of modal tableaux with histories for the modal logics K, KT and S4 in Lean. We describe how we formalized the static and transitional rules, the non-trivial termination and the correctness of loop-checks. The formalized tableaux are essentially executable decision procedures with soundness and completeness proved. Termination is also proved in order to define them as functions in Lean. All of these decision procedures return a concrete Kripke model in cases where the input set of formulas is satisfiable, and a proof constructed via the tableau rules witnessing unsatisfiability otherwise. We also describe an extensible formalization of backjumping and its verified implementation for the modal logic K. As far as we know, these are the first verified decision procedures for these modal logics.

2017

1. Thesis

   A Formally Verified Proof of Kruskal’s Tree Theorem in Lean

   Minchao Wu

   Master’s Thesis, 2017

   PDF