5 papers
Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning
Olivia Peiyu Wang, Sanna Wong-Toropainen, Daneshvar Amrollahi +4
Large Language Models (LLMs) achieve strong performance on reasoning tasks, but whether this reflects faithful logical inference or heuristic approximation remains unclear. We stud…
Faithful Autoformalization via Roundtrip Verification and Repair
Daneshvar Amrollahi, Jerry Lopez, Clark Barrett
When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formal…
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi +5
We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs…
Towards SMT Solver Stability via Input Normalization
Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz +4
In many applications, SMT solvers are utilized to solve similar or identical tasks over time. Significant variations in performance due to small changes in the input are not uncomm…
(Un)Solvable Loop Analysis
Daneshvar Amrollahi, Ezio Bartocci, George Kenison +3
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the…