COSMOS
UCLA · Summer research
At COSMOS, I tested whether AI theorem provers solve different problems with a stable strategy, not only whether they get the right answer.
The question
Success rate hides the route an agent takes. One system may use a repeatable plan across problems while another arrives through a scattered process. I wanted a way to tell those behaviors apart.
Working with Prof. HTB at UCLA, I adapted the Behavioral Consistency Metric to Lean theorem-proving agents and turned each proof into a fingerprint of its tactics, structure, and errors.
260,103
Lean proofs analyzed
0.923
Macro F1 on mutation recovery
6
Robustness checks
Field notes
01
Represent
I extracted structural features from Lean proof attempts and converted them into attribution vectors. Those vectors made it possible to compare strategies geometrically across a large collection of problems.
02
Validate
Before trusting the metric, I tested it on 260,103 APRIL proofs with known mutation labels. A LightGBM classifier recovered those mutation types at 0.923 macro F1, showing that the fingerprints captured meaningful structure.
03
Compare
The analysis found DeepSeek-Prover-V1 substantially more consistent across tasks than a large human Mathlib corpus, then separated it from Goedel-Prover-SFT across six robustness checks.
The summer around the work
The program mixed long sessions of debugging and analysis with a cohort living, learning, and exploring UCLA together. The result was equal parts research sprint and shared summer experience.
Visual archive
A research summer that changed how I think about evaluating intelligent systems.
Return to the full portfolio