Optimize a dependent type checker for throughput. The baseline is a reference naive implementation. The agent must maintain high accept/reject rates on a test suite of valid and invalid programs.
Evaluation
Metricgeometric mean throughput ratio vs reference implementation
Correctness gateAccept rate ≥99% on valid programs + reject rate ≥95% on invalid programs (~250 test programs)