VeriBench (Python → Lean 4)

  • Focus: End-to-end benchmark for translating Python into the Lean 4 proof assistant (code, tests, theorems, machine-checked proofs).
  • Status: Ongoing. See the ICML virtual entry: icml.cc/virtual/2025/52376.
  • Interests: Self-improvement and reasoning in large language models with a focus on mathematical verification.

Research Focus: AI Code Verification

As AI-generated code becomes increasingly prevalent in software development, there’s a growing need for robust verification methods that go beyond traditional testing approaches. My research explores neuro-symbolic techniques that can bridge the gap between AI-generated Python code and formal mathematical guarantees.

VeriBench represents a comprehensive approach to this challenge, focusing on translating real-world Python implementations into the Lean 4 proof assistant. The benchmark includes practical examples from the Python standard library (such as heapq) and security-critical components inspired by educational materials like MIT 6.858.

A key aspect of this work involves developing reliable evaluation methodologies for AI-generated formal specifications, ensuring that automated theorem generation maintains logical consistency and mathematical rigor. This research contributes to the broader goal of making AI-generated code more trustworthy and verifiable.