1 citations · 1 across the 4 of their papers we have counts for
9 papers
ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
Jiayi Wu, Robert Joseph George, Anima Anandkumar
Formal theorem proving has emerged as a frontier challenge for machine learning, yet the ecosystem is fragmented: proofs remain siloed across incompatible systems, limiting both tr…
QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs
Santiago Gonzalez, Alireza Amiri Bavandpour, Peter Ye +48
As Large Language Models (LLMs) saturate elementary benchmarks, the research frontier has shifted from generation to the reliability of automated evaluation. We demonstrate that st…
TorchLean: Formalizing Neural Networks in Lean
Robert Joseph George, Jennifer Cruden, Will Adkisson +3
Neural networks are increasingly deployed in scientific, safety critical, and mission critical pipelines, yet verification and analysis are often performed outside the programming…
BRIDGE: Building Representations In Domain Guided Program Synthesis
Robert Joseph George, Carson Eisenach, Udaya Ghai +3
Large language models can generate plausible code, but remain brittle for formal verification in proof assistants such as Lean. A central scalability challenge is that verified syn…
A Library for Learning Neural Operators
Jean Kossaifi, Nikola Kovachki, Zongyi Li +8
We present NeuralOperator, an open-source Python library for operator learning. Neural operators generalize neural networks to maps between function spaces instead of finite-dimens…
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Robert Joseph George, Suozhi Huang, Peiyang Song +1
Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucina…