6 citations · 13 across the 9 of their papers we have counts for
5 papers · 1 filter
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…