QuantumLean-Bench: A Unified Benchmark for Informal and Formal Quantum Reasoning

Isha Goswami1, Anushka Paulchoudhury1, Robert Joseph George 1, Anima Anandkumar1
1California Institute of Technology
ICML 2026 AI4Physics Workshop
Workshop

Abstract

QuantumLean-Bench is a unified benchmark for quantum-science reasoning across informal natural-language solutions and Lean-oriented formal representations. It contains 931 problems spanning chemistry, computing, information theory, physics, and quantum machine learning, with paired response slots for explanation and formalization.


  • Domains: chemistry, computing, information theory, physics, and quantum machine learning.
  • Tasks: informal reasoning and Lean-oriented formal representation.
  • Goal: evaluate whether models preserve mathematical structure when moving from explanation to formalization.

Benchmark

  • 931 quantum-science problems with both informal and formal response fields.
  • Lean scaffolds and evaluation scripts for checking generated formal artifacts.
  • Coverage of linear algebra, probability, circuits, states, operators, and measurement.