Search

In recent years, portfolio problem solving found many applications in automated reasoning, primarily in SAT solving and in automated and interactive theorem proving. Portfolio problem solving is an approach in which for an individual instance of a specific problem, one particular, hopefully most appropriate, solving technique is automatically selected among several available ones and used. The selection usually employs machine learning methods. To our knowledge, this approach has not been used in automated theorem proving in geometry so far and it poses a number of new challenges. In this paper we propose a set of features which characterize a specific geometric theorem, so that machine learning techniques can be used in geometry. Relying on these features and using different machine learning techniques, we constructed several portfolios for theorem proving in geometry and also runtime prediction models for provers involved. The evaluation was performed on two corpora of geometric theorems: one coming from geometric construction problems and one from a benchmark set of the GeoGebra tool. The obtained results show that machine learning techniques can be useful in automated theorem proving in geometry, while there is still room for further progress.

Artificial intelligence is steadily increasing its impact on everyday life. Therefore, the societal issues of artificial intelligence have become an important concern in the AI research. The presence of data that reflects human biases towards historically discriminated groups defined by sensitive features such as race and gender, results in machine learning models which discriminate against these groups. In order to tackle the impact of bias in data, researchers developed a variety of specialized machine learning algorithms which are able to satisfy different fairness constraints imposed on the model. Group fairness constraints do not fit standard machine learning formulations easily due to their non-differentiable nature. In this paper we developed a technique for learning a fair classifier by Monte Carlo policy gradient method which naturally deals with such non-differentiable constraints. Our methodology focuses on direct optimization of both group fairness metric and predictive performance of the model. In addition, we propose two different variance reduction techniques of gradient estimation. We compare our models to seven other related and state-of-the-art models and demonstrate that they are able to achieve better trade-off between accuracy and unfairness. To the best of our knowledge, this is the first fair classification algorithm which solves the issue of non-differentiable constraints by reinforcement learning techniques.

This paper discusses research results with regard to energy-efficient transmission of serialised data between servers and mobile devices. A test environment was created in which the research authors primarily measured electricity consumption during communication between a mobile device and server. Numerical results were used to determine how well data serialisation was performed on a dedicated server and its effects on the power consumption of a mobile device. The time spent in data serialisation and the size of the serialised file were found to significantly influence energy consumption. Based on that fact, results have been used to create a mathematical model which was later introduced with functional forms. The main variables in those functional forms were time of serialisation and size of a serialised file. The data collected through this research has been used for an experimental API-CB Saver, which based on mathematical models chooses the most favourable manner of serialisation and compression in real time. The results collected during the tests show that the CBSaver-Api approach performs with greater energy efficiency than current techniques. Furthermore, with optimal selection of data serialisation type and compression level in real time the considered system shows better performance in power saving. According to the results, the API-CBSaver tests indicate the direction which one should take for the purposes of improving energy efficiency.

Evaluating improvements to modern SAT solvers and comparison of two arbitrary solvers is a challenging and important task. Relative performance of two solvers is usually assessed by running them on a set of SAT instances and comparing the number of solved instances and their running time in a straightforward manner. In this paper we point to shortcomings of this approach and advocate more reliable, statistically founded methodologies that could discriminate better between good and bad ideas. We present one such methodology and illustrate its application.

Context: The number of students enrolled in universities at standard and on-line programming courses is rapidly increasing. This calls for automated evaluation of students assignments. Objective: We aim to develop methods and tools for objective and reljable automated grading that can also provide substantial and comprehensible feedback. Our approach targets introductory programming courses, which have a number of specific features and goals. The benefits are twofold: reducing the workload for teachers, and providing helpful feedback to students in the process of learning. Method: For sophisticated automated evaluation of students' programs, our grading framework combines results of three approaches (i) testing, (ii) software verification, and (iii) control flow graph similarity measurement. We present our tools for software verification and control flow graph similarity measurement, which are publicly available and open source. The tools are based on an intermediate code representation, so they could be applied to a number of programming languages. Results: Empirical evaluation of the proposed grading framework is performed on a corpus of programs written by university students in programming language C within an introductory programming course. Results of the evaluation show that the synergy of proposed approaches improves the quality and precision of automated grading and that automatically generated grades are highly correlated with instructor-assigned grades. Also, the results show that our approach can be trained to adapt to teacher's grading style. Conclusions: In this paper we integrate several techniques for evaluation of student's assignments. The obtained results suggest that the presented tools can find real-world applications in automated grading. (C) 2012 Elsevier B.V. All rights reserved.

Execution of most of the modern DPLL-based SAT solvers is guided by a number of heuristics. Decisions made during the search process are usually driven by some fixed heuristic policies. Despite the outstanding progress in SAT solving in recent years, there is still an appealing lack of techniques for selecting policies appropriate for solving specific input formulae. In this paper we present a methodology for instance-based selection of solver's policies that uses a data-mining classification technique. The methodology also relies on analysis of relationships between formulae, their families, and their suitable solving strategies. The evaluation results are very good, demonstrate practical usability of the methodology, and encourage further efforts in this direction.