Greg Durrett

Reinforcement learning with verifiable rewards (RLVR) typically optimizes for outcome rewards without imposing constraints on intermediate reasoning. This leaves training susceptible to reward hacking, where models exploit loopholes (e.g., spurious patterns in training data) in the reward function to achieve high scores without solving the intended task. These reward-hacking behaviors are often implicit, as the intermediate chain-of-thought (CoT) may appear plausible on the surface, limiting the effectiveness of purely text-based monitoring. We propose Gradient Fingerprint(GRIFT), a method for detecting reward hacking behavior through models' internal computation. Given a prompt and a model-generated CoT, GRIFT computes gradients of the CoT conditioned on the prompt and compresses them into a compact representation, which is then used to assess whether the CoT reflects reward hacking behavior. Across verifiable reasoning benchmarks spanning math, code, and logical reasoning, GRIFT substantially outperforms strong baselines, including CoT Monitor and TRACE, achieving over 25% relative improvement in detecting reward hacking behavior. Moreover, integrating GRIFT into the rejection fine-tuning pipeline for reasoning tasks reduces reward hacking and improves performance on the true task objective. Our results highlight a promising direction of leveraging gradient-level representations for assessing the quality of CoT reasoning traces.

Large language models have recently achieved striking results in interactive theorem proving, particularly in Lean. While most benchmarks for LLM-based proof automation are drawn from mathematics and involve the Mathlib ecosystem, many proofs in software verification and programming-languages semantics are developed inside sizable codebases that define their own core abstractions and involve substantial project-specific libraries. In this setting, progress often depends on locating and using a small set of relevant local definitions and lemmas amid a large amount of surrounding context. This paper introduces VeriSoftBench, a benchmark of 500 Lean 4 proof obligations drawn from open-source formal-methods developments and that are packaged to preserve project context and cross-file dependencies. We evaluate frontier LLMs and specialized provers on VeriSoftBench and find that success rates drop sharply as contextual dependency increases. This highlights the difficulty that current systems face when proofs are grounded in project-specific libraries rather than a single shared ecosystem like Mathlib.