7 citations · 18 across the 19 of their papers we have counts for
10 papers · 1 filter
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Prithwish Jana, Viet Bach Hoang, Logan Luna +9
Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, re…
Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization
Piyush Jha, Aishik Ghosh, Vijay Ganesh
The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerat…
Learning Scattering Amplitudes with Transformer Reinforcement Learning
Philip Velie, Tianji Cai, Piyush Jha +2
We introduce a transformer reinforcement learning algorithm that learns to solve high loop-level scattering amplitudes in planar N = 4 Super Yang-Mills theory. Our algorithm improv…
CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery
Piyush Jha, Jake Rudolph, Victoria Knapp-Pérez +3
Many scientific discovery problems require searching combinatorial hypothesis spaces under complex domain constraints. Reinforcement learning (RL) offers a promising approach, but…
Making Embodied AI Reliable: A Community Agenda from Testing to Formal Verification
Xi Zheng, Dulanga Weerakoon, Yintong Huo +8
Embodied AI systems are increasingly deployed in open-world environments, yet ensuring their reliability remains a fundamental challenge. Drawing on discussions from the AAAI'26 Br…
Symbolic Regression via Latent Iterative Refinement
Xieting Chu, Sriram Vishwanath, Vijay Ganesh
Symbolic regression (SR) seeks closed-form mathematical expressions that fit observed data. Neural SR methods amortize the search by training an encoder to map observations directl…
MathConstraint: Automated Generation of Verified Combinatorial Reasoning Instances for LLMs
Viresh Pati, Zhengyu Li, Piyush Jha +3
We introduce MathConstraint, a hard, adaptive benchmark for evaluating the combinatorial reasoning capabilities of LLMs. We combine constraint satisfaction problems with rigorous s…
Understanding CDCL Solvers via Scalability Studies and Proofdoors
Shimin Zhang, Yechuan Xia, Chunxiao Li +3
Over the past several decades, CDCL SAT solvers have proven remarkably effective on large industrial formulas, despite SAT being NP-complete and widely believed to be intractable.…
Proofdoors and Efficiency of CDCL Solvers
Sunidhi Singh, Vincent Liew, Marc Vinyals +1
We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over a certain class of formulas derived from circuit (esp., arithmetic) ver…
An Exponential Separation between Deterministic CDCL and DPLL Solvers
Sahil Samar, Marc Vinyals, Vijay Ganesh
We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instance…