20 citations · 53 across the 17 of their papers we have counts for
20 papers
Verifier-Grounded Agentic RL for Provably Correct Code
George Ma, Yuhao Zhang, Bing He +5
Reinforcement learning for code usually rewards passing tests, which a model can do while remaining wrong on the inputs the tests do not cover. A program verifier instead decides w…
Instruct, Not Answer: Using Instruction Privileges in On-Policy Context Distillation
Hantao Yu, Sandy Han, Xiaoxue Han +6
On-Policy Context Distillation (OPCD) has recently emerged as a powerful technique for transferring context to student models and for self-improvement. In OPCD, the teacher is cond…
SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
George Ma, Benjamin Mikek, Haoyu Li +9
Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suit…
Beyond Solver Verdicts: Generative Reward Models for Autoformalization
Vikash Singh, Debargha Ganguly, Aman Goel +5
Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict referenc…
Stratified Consistency Distillation for Natural Language Formalization
Zhichao Hou, Ferhat Erata, Joe Lilien +1
Neurosymbolic reasoning has shown promising success in addressing complex reasoning tasks by combining large language models (LLMs) and symbolic solvers. While this approach shows…
Fidelity Probes for Specification--Code Alignment
Ferhat Erata, Hao Zhou, Jun Huan +1
Software modernization often relies on natural-language specifications recovered from an existing implementation. Incorrect or missing requirements can lead to defects in the moder…
Learning How to Cube
Ferhat Erata, Sam Kouteili, Thanos Typaldos +4
Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn e…
A Neurosymbolic Approach to Natural Language Formalization and Verification
Chenyang An, Sam Bayless, Stefano Buliani +27
Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries l…
Learning Randomized Reductions
Ferhat Erata, Orr Paradise, Thanos Typaldos +4
Randomized self-reductions (RSRs) express using evaluated at random correlated points, enabling self-correcting programs, instance-hiding protocols, and applications in…
Scheherazade: Evaluating Chain-of-Thought Math Reasoning in LLMs with Chain-of-Problems
Stephen Miner, Yoshiki Takashima, Simeng Han +4
Benchmarks are critical for measuring Large Language Model (LLM) reasoning capabilities. Some benchmarks have even become the de facto indicator of such capabilities. However, as L…
Systematic Use of Random Self-Reducibility against Physical Attacks
Ferhat Erata, TingHung Chiu, Anthony Etim +7
This work presents a novel, black-box software-based countermeasure against physical attacks including power side-channel and fault-injection attacks. The approach uses the concept…
A Tool for Automated Reasoning About Traces Based on Configurable Formal Semantics
Ferhat Erata, Arda Goknil, Bedir Tekinerdogan +1
We present Tarski, a tool for specifying configurable trace semantics to facilitate automated reasoning about traces. Software development projects require that various types of tr…
Integrating Static Code Analysis Toolchains
Matthias Kern, Ferhat Erata, Markus Iser +4
This paper proposes an approach for a tool-agnostic and heterogeneous static code analysis toolchain in combination with an exchange format. This approach enhances both traceabilit…
AlloyInEcore: Embedding of First-Order Relational Logic into Meta-Object Facility for Automated Model Reasoning
Ferhat Erata, Arda Goknil, Ivan Kurtev +1
We present AlloyInEcore, a tool for specifying metamodels with their static semantics to facilitate automated, formal reasoning on models. Software development projects require tha…
ModelWriter: Text & Model-Synchronized Document Engineering Platform
Ferhat Erata, Claire Gardent, Bikash Gyawali +5
The ModelWriter platform provides a generic framework for automated traceability analysis. In this paper, we demonstrate how this framework can be used to trace the consistency and…
Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers
Ferhat Erata, Chuanqi Xu, Ruzica Piskac +1
The interest in quantum computing has grown rapidly in recent years, and with it grows the importance of securing quantum circuits. A novel type of threat to quantum circuits that…
Classification of Quantum Computer Fault Injection Attacks
Chuanqi Xu, Ferhat Erata, Jakub Szefer
The rapid growth of interest in quantum computing has brought about the need to secure these powerful machines against a range of physical attacks. As qubit counts increase and qua…
Exploration of Quantum Computer Power Side-Channels
Chuanqi Xu, Ferhat Erata, Jakub Szefer
With the rapidly growing interest in quantum computing also grows the importance of securing these quantum computers from various physical attacks. Constantly increasing qubit coun…
Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code
Ferhat Erata, Ruzica Piskac, Victor Mateu +1
Although cryptographic algorithms may be mathematically secure, it is often possible to leak secret information from the implementation of the algorithms. Timing and power side-cha…
ETAP: Energy-aware Timing Analysis of Intermittent Programs
Ferhat Erata, Arda Goknil, Eren Yıldız +4
Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs whe…