10 papers
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal +6
AI coding agents are increasingly used to write real-world software, but ensuring that their outputs are correct remains a fundamental challenge. Formal verification offers a promi…
Reasoning over mathematical objects: on-policy reward modeling and test time aggregation
Pranjal Aggarwal, Marjan Ghazvininejad, Seungone Kim +18
The ability to precisely derive mathematical objects is a core requirement for downstream STEM applications, including mathematics, physics, and chemistry, where reasoning must cul…
Propose, Solve, Verify: Self-Play Through Formal Verification
Alex Wilf, Pranjal Aggarwal, Bryan Parno +4
Training models through self-play alone (without any human data) has been a longstanding goal in AI, but its effectiveness for training large language models remains unclear, parti…
OptimalThinkingBench: Evaluating Over and Underthinking in LLMs
Pranjal Aggarwal, Seungone Kim, Jack Lanchantin +4
Thinking LLMs solve complex tasks at the expense of increased compute and overthinking on simpler problems, while non-thinking LLMs are faster and cheaper but underthink on harder…
L1: Controlling How Long A Reasoning Model Thinks With Reinforcement Learning
Pranjal Aggarwal, Sean Welleck
Reasoning language models have shown an uncanny ability to improve performance at test-time by ``thinking longer''-that is, by generating longer chain-of-thought sequences and henc…
Programming with Pixels: Can Computer-Use Agents do Software Engineering?
Pranjal Aggarwal, Sean Welleck
Computer-use agents (CUAs) hold the promise of performing a wide variety of general tasks, but current evaluations have primarily focused on simple scenarios. It therefore remains…