ARC: Automated Reasoning in The Class [Erasmus+ Project]

@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{RISC6677,
author = {Diego Dominici and Francisco Marcellan},
title = {{Linear functionals and $Delta$- coherent pairs of the second kind}},
language = {english},
abstract = {We classify all the emph{$Delta$-}coherent pairs of measures of the secondkind on the real line. We obtain $5$ cases, corresponding to all the familiesof discrete semiclassical orthogonal polynomials of class $sleq1.$},
number = {23-02},
year = {2023},
month = {February},
keywords = { Discrete orthogonal polynomials, discrete semiclassical functionals, discrete Sobolev inner products, coherent pairs of discrete measures, coherent pairs of second kind for discrete measures.},
length = {24},
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{RISC6687,
author = {Diego Dominici },
title = {{Recurrence relations for the moments of discrete semiclassical functionals of class $sleq2.$}},
language = {english},
abstract = {We study recurrence relations satisfied by the moments $lambda_{n}left(zright) $ of discrete linear functionals whose first moment satisfies aholonomic differential equation. We consider all cases when the order of theODE is less or equal than $3$.},
number = {23-05},
year = {2023},
month = {March},
keywords = {Discrete orthogonal polynomials, discrete semiclassical functionals, moments.},
length = {81},
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{RISC6683,
author = {M. Kauers and P. Nuspl and V. Pillwein},
title = {{Order bounds for $C^2$-finite sequences}},
language = {english},
abstract = {A sequence is called $C$-finite if it satisfies a linear recurrence with constant coefficients. We study sequences which satisfy a linear recurrence with $C$-finite coefficients. Recently, it was shown that such $C^2$-finite sequences satisfy similar closure properties as $C$-finite sequences. In particular, they form a difference ring. In this paper we present new techniques for performing these closure properties of $C^2$-finite sequences. These methods also allow us to derive order bounds which were not known before. Additionally, they provide more insight in the effectiveness of these computations. The results are based on the exponent lattice of algebraic numbers. We present an iterative algorithm which can be used to compute bases of such lattices.},
number = {23-03},
year = {2023},
month = {February},
keywords = {Difference equations, holonomic sequences, closure properties, algorithms},
length = {16},
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{RISC6682,
author = {C. Schneider},
title = {{Refined telescoping algorithms in $R\Pi\Sigma$-extensions to reduce the degrees of the denominators}},
language = {english},
abstract = {We present a general framework in the setting of difference ring extensions that enables one to find improved representations of indefinite nested sums such that the arising denominators within the summands have reduced degrees. The underlying (parameterized) telescoping algorithms can be executed in $R\Pi\Sigma$-ring extensions that are built over general $\Pi\Sigma$-fields. An important application of this toolbox is the simplification of d'Alembertian and Liouvillian solutions coming from recurrence relations where the denominators of the arising sums do not factor nicely.},
number = {23-01},
year = {2023},
month = {February},
note = {arXiv:2302.03563 [cs.SC]},
keywords = {telescoping, difference rings, reduced denominators, nested sums},
length = {18},
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)}
}