arXiv subjects

Seth Ahrenbach

Publications and source records attributed to Seth Ahrenbach.

3 recordsLinked to original sources

arXiv2024

Löb-Safe Logics for Reflective Agents

Epistemic and doxastic logics are modal logics for knowledge and belief, and serve as foundational models for rational agents in game theory, philosophy, and computer science. We examine the consequences of modeling agents capable of a certain sort of reflection. Such agents face a formal difficulty due to Löb's Theorem, called Löb's Obstacle in the literature. We show how the most popular axiom schemes of epistemic and doxastic logics suffer from Löb's Obstacle, and present two axiom schemes that that avoid Löb's Obstacle, which we call Reasonable Löb-Safe Epistemic Doxastic logic (${LSED}^R$) and Supported Löb-Safe Epistemic Doxastic logic (${LSED}^S$).

cs.LO↗

arXiv2024

DafnyBench: A Benchmark for Formal Software Verification

We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough hints for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.

cs.SE↗

arXiv2018

Reasoning About Safety-Critical Information Flow Between Pilot and Computer

This paper presents research results that develop a dynamic logic for reasoning about safety-critical information flow among humans and computers. The logic advances previous efforts to develop logics of agent knowledge, which make assumptions that are too strong for realistic human agents. We introduce Dynamic Agent Safety Logic (DASL), based on Dynamic Epistemic Logic (DEL), with extensions to account for safe actions, belief, and the logical relationships among knowledge, belief, and safe action. With this logic we can infer which safety-critical information a pilot is missing when executing an unsafe action. We apply the logic to the Air France 447 incident as a case study and provide a mechanization of the case study in the Coq proof assistant.

cs.LO↗