Leni Aniva

Current Research and Scholarly Interests

My main research interest is Machine-Assisted Theorem Proving, which refers to using machine-learning agents to find proofs of mathematical theorems and conduct reasoning. We are pursuing a hybrid algorithm between neural networks and SMT solvers to solve some of the long standing problems facing machine learning models today such as opaqueness, hallucinations, and information leakage. For this goal, I built the Pantograph library for Lean 4, which provides an uncompromising interface for machine-learning agents to conduct MCTS-like proof search on theorems. This library provides a flexible solution to the metavariable coupling problem, which happens when a theorem requires two conditions which are interdependent on each other. For example, if you want to provide there exists an odd perfect number, you would have to exhibit a number and prove that the particular number is odd and perfect. I built Trillium, a tool for evaluating theorem proving algorithms, and designed it to be compatible with all previous theorem proving algorithms to provide a fair benchmark for all of them.

I also do research on SMT solvers and automatic verifications of programs.

Projects

• Pantograph, Centaur Lab (March 1, 2023 - Present)

  Pantograph is a platform providing a gym-link machine learning for interface for Lean 4. It provides the following features:
  1. Access of all of Lean's tactics, including `have`, `let`, `calc`, `conv`, which are not supported well in preceding works such as LeanDojo or REPL
  2. Customized handling of coupling between goals. The user (or ML agent) can choose to make progress on one goal, pause, and switch to another goal. This is not a feature supported in vanilla Lean.
  3. Read existing Lean files to generate training data
  4. An interface for tree search on the Lean proof environment

  Location

  Palo Alto

  Collaborators

  • Livia Sun, Ph.D. Student in Computer Science, admitted Autumn 2022, School of Engineering
  • Clark Barrett, Professor (Research) of Computer Science, Centaur Lab
  • Brando Miranda, Ph.D. Student in Computer Science, admitted Autumn 2022, School of Engineering

  For More Information:

  • PyPantograph
  • Pantograph

Lab Affiliations

• Clark Barrett, Center for Automated Reasoning (9/26/2022)