Autoformalization evaluation harness
Nine-constraint symbolic evaluator · F1-vs-N sweep
The tooling behind my UROP fellowship: prompt-condition sweeps across nine models, symbolic scoring of generated Prolog, and a grid-size stress test that catches enumeration masquerading as rule induction.