6 citations · 13 across the 9 of their papers we have counts for
11 papers
L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents
Carson Eisenach, Robert Joseph George, Vincent Quenneville-Belair +2
The lasting gains in AI have come from methods that absorb more computation, and language models already scale computation within a call. Useful work, though, happens across calls:…
FloatLib: Verified Floating-Point Arithmetic in Lean
Robert Joseph George, Will Adkisson, Anima Anandkumar
We present FloatLib, a verified arbitrary-precision floating-point arithmetic library in Lean 4 that combines broad format coverage, machine-checked correctness, and efficient cert…
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…
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…
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…
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…
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…
TensorGRaD: Tensor Gradient Robust Decomposition for Memory-Efficient Neural Operator Training
Sebastian Loeschcke, David Pitt, Robert Joseph George +5
Scientific problems require resolving multi-scale phenomena across different resolutions and learning solution operators in infinite-dimensional function spaces. Neural operators p…
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…
LeanAgent: Lifelong Learning for Formal Theorem Proving
Adarsh Kumarappan, Mo Tiwari, Peiyang Song +3
Large Language Models (LLMs) have been successful in mathematical reasoning tasks such as formal theorem proving when integrated with interactive proof assistants like Lean. Existi…
Pretraining Codomain Attention Neural Operators for Solving Multiphysics PDEs
Md Ashiqur Rahman, Robert Joseph George, Mogab Elleithy +9
Existing neural operator architectures face challenges when solving multiphysics problems with coupled partial differential equations (PDEs) due to complex geometries, interactions…