Showing 1–8 of 8 results for author: Bentkamp, A

Verified reductions for optimization

Authors: Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad

Abstract: Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more r… ▽ More Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them. △ Less

Submitted 22 February, 2023; v1 submitted 23 January, 2023; originally announced January 2023.

MSC Class: 90C25; 68V15

HHLPy: Practical Verification of Hybrid Systems using Hoare Logic

Authors: Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan

Abstract: We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof rules for reasoning about ordinary differential equations. Verification conditions are generated from the annotations following the rules of hybrid Hoare logic. We… ▽ More We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP programs with pre- and postconditions, invariants, and proof rules for reasoning about ordinary differential equations. Verification conditions are generated from the annotations following the rules of hybrid Hoare logic. We designed labeling and highlighting mechanisms to distinguish and visualize different verification conditions. The tool is implemented in Python and has a web-based user interface. We evaluated the effectiveness of the tool on translations of Simulink/Stateflow models and on KeYmaera X benchmarks. △ Less

Submitted 21 February, 2023; v1 submitted 31 October, 2022; originally announced October 2022.

Privacy accounting $\varepsilon$conomics: Improving differential privacy composition via a posteriori bounds

Authors: Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp, Robert West

Abstract: Differential privacy (DP) is a widely used notion for reasoning about privacy when publishing aggregate data. In this paper, we observe that certain DP mechanisms are amenable to a posteriori privacy analysis that exploits the fact that some outputs leak less information about the input database than others. To exploit this phenomenon, we introduce output differential privacy (ODP) and a new compo… ▽ More Differential privacy (DP) is a widely used notion for reasoning about privacy when publishing aggregate data. In this paper, we observe that certain DP mechanisms are amenable to a posteriori privacy analysis that exploits the fact that some outputs leak less information about the input database than others. To exploit this phenomenon, we introduce output differential privacy (ODP) and a new composition experiment, and leverage these new constructs to obtain significant privacy budget savings and improved privacy-utility tradeoffs under composition. All of this comes at no cost in terms of privacy; we do not weaken the privacy guarantee. To demonstrate the applicability of our a posteriori privacy analysis techniques, we analyze two well-known mechanisms: the Sparse Vector Technique and the Propose-Test-Release framework. We then show how our techniques can be used to save privacy budget in more general contexts: when a differentially private iterative mechanism terminates before its maximal number of iterations is reached, and when the output of a DP mechanism provides unsatisfactory utility. Examples of the former include iterative optimization algorithms, whereas examples of the latter include training a machine learning model with a large generalization error. Our techniques can be applied beyond the current paper to refine the analysis of existing DP mechanisms or guide the design of future mechanisms. △ Less

Submitted 19 June, 2023; v1 submitted 6 May, 2022; originally announced May 2022.

Comments: 25 pages, 2 figures. The formal proof and the code for generating the plots can be found at https://doi.org/10.6084/m9.figshare.19330649 Current version: fixed a mistake in the legend of Fig. 1

Journal ref: Proceedings on Privacy Enhancing Technologies 3 (2022) 222-246

An Impossible Asylum

Authors: Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

Abstract: In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzz… ▽ More In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle's hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist. △ Less

Submitted 23 April, 2022; v1 submitted 3 December, 2021; originally announced December 2021.

MSC Class: 03-01 (Primary); 03B35; 68V15 (Secondary)

Verified Optimization

Authors: Alexander Bentkamp, Jeremy Avigad

Abstract: Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards develo** a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways. Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards develo** a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways. △ Less

Submitted 12 November, 2021; originally announced November 2021.

Superposition with Lambdas

Authors: Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann

Abstract: We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $βη$-equivalence classes of $λ$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle b… ▽ More We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $βη$-equivalence classes of $λ$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning. △ Less

Submitted 31 January, 2021; originally announced February 2021.

ACM Class: F.4.1; I.2.3

Efficient Full Higher-Order Unification

Authors: Petar Vukmirović, Alexander Bentkamp, Visa Nummelin

Abstract: We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our… ▽ More We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure, together with new higher-order term indexing data structures, is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski's procedure. △ Less

Submitted 13 December, 2021; v1 submitted 18 November, 2020; originally announced November 2020.

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 4 (December 14, 2021) lmcs:6919

Superposition for Lambda-Free Higher-Order Logic

Authors: Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann

Abstract: We introduce refutationally complete superposition calculi for intentional and extensional clausal $λ$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $λ$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calcu… ▽ More We introduce refutationally complete superposition calculi for intentional and extensional clausal $λ$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $λ$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a step** stone towards complete, highly efficient automatic theorem provers for full higher-order logic. △ Less

Submitted 9 April, 2021; v1 submitted 5 May, 2020; originally announced May 2020.

Comments: arXiv admin note: text overlap with arXiv:2102.00453

ACM Class: F.4.1; I.2.3

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 2 (April 12, 2021) lmcs:6455