Shafi Goldwasser, Orr Paradise

Self Proving Model Training

&

Building Harnesses for Evaluating Math definitions

​

1. Implement the probabilistic-consistency proof system. We recently constructed a proof system with which a predictive model can prove that its probabilistic claims are self-consistent, with the verifier explicitly designed for implementation. The goal of this project is to build that verifier, then train a small prover (order 10M-100M parameters) against it via Transcript Learning or RLVF, and measure verifiability, i.e., the fraction of outputs the verifier accepts. This connects to the aforementioned collaboration with Cambridge, which the scholar could join.
2. Verifier hacking, in theory. RLVR as used in practice trains models against verifiers with no soundness guarantees. When does training against such a "verifier" result in a model that games it? In a stylized model, I have preliminary results showing that even benign training dynamics can inadvertently select a cheating prover, and that which prover is selected depends on fine features of the training setup (for instance, the noise structure). The direction is concrete but wide open: one could relax the fairly stringent assumptions the current theory asks for, or go empirical and test whether the phenomenon occurs in actual RLVR training. The destination is a characterization of when verifier-based training is sound: a theory of reward hacking for verifier-based training.
3. Universal Self-Proving models. The theoretical guarantees of Self-Proving models currently hold when trained against one fixed verifier. Can a single model prove its answers to verifiers specified in-context, including ones unseen during training? Mostly empirical (train across a family of proof systems, test generalization to new ones), with theory questions available close-by: what does in-context generalization over verifiers require? Presumably, a restricted class of verifiers (e.g. low-depth circuits) but can we say something more?

​

The list above is a suggested menu, certainly not a mandate. I am a strong believer in projects driven by the student's curiosity. My preferred mode of advising, and the way my advisors have advised me, is to be of service to the student: to let them follow the directions they find most interesting, mysterious, or promising, and to be there as a sounding board, friendly critic, verifier, etc. That is, I will say something if a student is headed down a path I see no way out of, but I have been humbled before (a wonderful experience) by students whose intuition or other senses were sharper than mine, and who ended up with results that genuinely surprised me.