Jocelyn Qiaochu Chen

Text-to-SQL over large analytical databases requires navigating complex schemas, resolving ambiguous queries, and grounding decisions in actual data. Most current systems follow a fixed pipeline where schema elements are retrieved once upfront and the database is only revisited for post-hoc repair, limiting recovery from early mistakes. We present FlexSQL, a text-to-SQL agent whose core design principle is flexible database interaction: the agent can explore schema structure, inspect data values, and run verification queries at any point during reasoning. FlexSQL generates diverse execution plans to cover multiple query interpretations, implements each plan in either SQL or Python depending on the task, and uses a two-tiered repair mechanism that can backtrack from code-level errors to plan-level revisions. On Spider2-Snow, using gpt-oss-120b, FlexSQL achieves a 65.4\% score, outperforming strong open-source baselines that use stronger, larger models such as gpt-o3 and DeepSeek-R1. When integrated into a general-purpose coding agent (as skills in Claude Code), our approach yields over 10\% relative improvement on Spider2-Snow. Further analysis shows that flexible exploration and flexible execution jointly contribute to the effectiveness of our approach, highlighting flexibility as a key design principle. Our code is available at: \url{https://github.com/StringNLPLAB/FlexSQL}.

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.