Formal Methods

@techreport{RISC6684,
author = {Bruno Buchberger},
title = {{Is ChatGPT Smarter Than Master’s Applicants?}},
language = {English},
abstract = {During the selection procedure for a particular informatics fellowship program sponsored by Upper Austrian companies, I ask the applicants a couple of simple technical questions about programming, etc., in a Zoom meeting. I put the same questions to the dialogue system ChatGPT, [ChatGPT]. The result surprised me: Nearly all answers of ChatGPT were totally correct and nicely explained. Also, in the dialogues to clarify some critical points in the answers, the explanations by ChatGPT were amazingly clear and goal-oriented.In comparison: I tried out the same questions in the personal Zoom interviews with approximately 30 applicants from five countries. Only the top three candidates (with a GPA of 1.0, i.e., the highest possible GPA in their bachelor’s study) performed approximately equally well in the interview. All the others performed (far) worse than ChatGPT. And, of course, all answers from ChatGPT came within 1 to 10 seconds, whereas most of the human applicants' answers needed lengthy and arduous dialogues.I am particularly impressed by the ability of ChatGPT to extract meaningful and well-structured programs from problem specifications in natural language. In this experiment, I also added some questions that ask for proofs for simple statements in natural language, which I do not ask in the student's interviews. The performance of ChatGPT was quite impressive as far as formalization and propositional logic are concerned. In examples where predicate logic reasoning is necessary, the ChatGPT answers are not (yet?) perfect. I am pleased to see that ChatGPT tries to present the proofs in a “natural style” This is something that I had as one of my main goals when I initiated the Theorema project in 1995. I think we already achieved this in the early stage of Theorema, and we performed this slightly better and more systematically than ChatGPT does.I also tried to develop a natural language input facility for Theorema in 2017, i.e., a tool to formalize natural language statements in predicate logic. However, I could not continue this research for a couple of reasons. Now I see that ChatGPT achieved this goal. Thus, I think that the following combination of methods could result in a significant leap forward:- the “natural style” proving methods that we developed within Theorema (for the automated generation of programs from specifications, the automated verification of programs in the frame of knowledge, and the automated proof of theorems in theories), in particular, my “Lazy Thinking Method” for algorithm synthesis from specifications- and the natural language formalization techniques of ChatGPT.I propose this as a research project topic and invite colleagues and students to contact me and join me in this effort: Buchberger.bruno@gmail.com.},
number = {23-04},
year = {2023},
month = {January},
keywords = {ChatGPT, automated programming, program synthesis, automated proving, formalization of natural language, master's screening},
length = {30},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6749,
author = {Wolfgang Schreiner and William Steingartner},
title = {{The SLANG Semantics-Based Language Generator}},
language = {english},
abstract = {This report documents the SLANG semantics-based language generator. SLANG is a software for generating rapid prototype implementations of programming languages from their formal specifications. Its input is a text file that describes the abstract syntax of a language and its concrete text representation; from this, a parser is generated (utilizing the ANTLR4 tool) that transforms the text representation of a program into its abstract syntax tree and a printer that generates from the abstract syntax tree its text representation. Furthermore, one can equip the language with a formal type system (by logical inference rules) from which a type checker is generated. Finally, one can give the language a formal semantics, in the denotational style (by function equations) and/or in the big-step operational style (by transition steps); from this, a language interpreter is generated. SLANG is implemented in Java and produces Java source code; it should be easy to extend the software also to other target languages.},
number = {23-13},
year = {2023},
month = {September},
keywords = {formal semantics of programming languages, denotational semantics, operational semantics, type systems, interpreters},
sponsor = {Supported by the Slovak Academic Information Agency SAIA project 2023-03-15-001 “Semantics-Based Rapid Prototyping of Domain-Specific Languages”},
length = {59},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6517,
author = {Wolfgang Schreiner},
title = {{The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)}},
language = {english},
abstract = {This report documents the RISCTP theorem proving interface. RISCTP consists of alanguage for specifying proof problems and of an associated software for solving theseproblems. The RISCTP language is a typed variant of first-order logic whose level ofabstraction is between that of higher level formal specification languages (such as thelanguage of the RISCAL model checker) and lower level theorem proving languages (such asthe language SMT-LIB supported by various satisfiability modulo theories solvers such as Z3).Thus the RISCTP language can serve as an intermediate layer that simplifies the connectionof specification and verification systems to theorem provers; in fact, it was developed toequip the RISCAL model checker with theorem proving capabilities. The RISCTP softwareis implemented in Java with an API that enables the implementation of such connections;however, RISCTP also provides a text-based frontend that allows its use as a theorem proveron its own. RISCTP already implements a backend that translates a proving problem intoSMT-LIB and solves it by the "black box" application of Z3; in the future, RISCTP shall alsoprovide built-in proving capabilities with greater transparency.},
number = {22-07},
year = {2022},
month = {June},
keywords = {automated reasoning, theorem proving, model checking, first-order logic, RISCAL, SMT-LIB, Z3},
length = {31},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

@techreport{RISC6328,
author = {Wolfgang Schreiner and Franz-Xaver Reichl},
title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},
language = {english},
abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},
number = {21-11},
year = {2021},
month = {June},
keywords = {model checking, satisfiability solving, formal specification, formal verficiation},
sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},
length = {30},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}