11 papers
An AI Approach to Verified Production Cryptographic Libraries
Chuyue Sun, Su Fong, Zhiyi Kuang +5
Cryptographic code is critical infrastructure that must be correct, yet formally verifying production libraries remains difficult. Existing language-model proof systems solve isola…
Not All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
Ido Pinto, Yizhak Yisrael Elboher, Haoze Wu +2
The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue…
Viverra: Text-to-Code with Guarantees
Haoze Wu, Rocky Klopfenstein, Keith Farkas +1
A fundamental limitation of Text-to-Code is that no guarantee can be obtained about the correctness of the generated code. Therefore, to ensure its correctness, the generated code…
SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints
Andrew Tremante, Yang He, Rocky Klopfenstein +3
We present SpotIt+, an open-source tool for evaluating Text-to-SQL systems via bounded equivalence verification. Given a generated SQL query and the ground truth, SpotIt+ actively…
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
Rocky Klopfenstein, Yang He, Andrew Tremante +3
Community-driven Text-to-SQL evaluation platforms play a pivotal role in tracking the state of the art of Text-to-SQL performance. The reliability of the evaluation process is crit…
HONEYBEE: Efficient Role-based Access Control for Vector Databases via Dynamic Partitioning[Technical Report]
Hongbin Zhong, Matthew Lentz, Nina Narodytska +2
Enterprise deployments of vector databases require access control policies to protect sensitive data. These systems often implement access control through hybrid vector queries tha…