Python code translated deterministically into Lean for verification
PastaLean: Deterministic transpilation from Python to Lean for Verification
Programming Languages
Summary
Verifying that Python programs work correctly is hard because Python is flexible and often untyped. The authors created PastaLean, a tool that automatically converts Python code into Lean, a language designed for formal proofs, allowing rigorous checking of program correctness. Their system also includes TypeInfer, which guesses types in untyped Python code, helping with the translation. Tests show the tool works on a wide range of real Python programs and passes most of their test cases.
What this means in practice
- •For software verification teams: Translate Python code into Lean to formally verify program correctness using theorem proving tools.
- •For software development teams using ai: Check correctness of auxiliary AI Python scripts by converting them into verifiable Lean programs.
Authors
Anirudh Gupta, Petros Markopoulos, Siddhartha Gadgil
Abstract
We present PastaLean, an extensible system for deterministic translation from Python to Lean via the Abstract Syntax Tree of Python. This allows for verification of Python code, especially auxiliary code used by AI. Every program is translated into a provable twin written in the form Lean's verification tooling can reason about, and a runnable twin that gives a fast and correct computation support. We also introduce our Type Inference engine TypeInfer which provides static typing support for untyped Python code. Our tool provides coverage of more than 92\% for LeetCode and HumanEval\textsuperscript{+} and more than 98\% for LiveCodeBench ground truth Python files. Further, at least 97\% of each dataset's (numerical) test cases pass, with 100\% on HumanEval\textsuperscript{+} and LiveCodeBench. The TypeInfer engine is the best-scoring tool on the TypeEvalPy static leaderboard, and on a repository-level TypyBench benchmark it scores above every competing repository-level inference tool.