In this paper, we present our research on building computing machines consciousness about intuitive geometry based on mathematics experiments and statistical inference. The investigation consists of the following five...In this paper, we present our research on building computing machines consciousness about intuitive geometry based on mathematics experiments and statistical inference. The investigation consists of the following five steps. At first, we select a set of geometric configurations and for each configuration we construct a large amount of geometric data as observation data using dynamic geometry programs together with the pseudo-random number generator. Secondly, we refer to the geometric predicates in the algebraic method of machine proof of geometric theorems to construct statistics suitable for measuring the approximate geometric relationships in the observation data. In the third step, we propose a geometric relationship detection method based on the similarity of data distribution, where the search space has been reduced into small batches of data by pre-searching for efficiency, and the hypothetical test of the possible geometric relationships in the search results has be performed. In the fourth step, we explore the integer relation of the line segment lengths in the geometric configuration in addition. At the final step, we do numerical experiments for the pre-selected geometric configurations to verify the effectiveness of our method. The results show that computer equipped with the above procedures can find out the hidden geometric relations from the randomly generated data of related geometric configurations, and in this sense, computing machines can actually attain certain consciousness of intuitive geometry as early civilized humans in ancient Mesopotamia.展开更多
We present a symbolic-numeric hybrid method, based on sum-of-squares （SOS） relaxation and rational vec- tor recovery, to compute inequality invariants and ranking functions for proving total correctness and generati...We present a symbolic-numeric hybrid method, based on sum-of-squares （SOS） relaxation and rational vec- tor recovery, to compute inequality invariants and ranking functions for proving total correctness and generating pre- conditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate rank- ing functions with floating point coefficients. Then Gauss- Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several exam- ples are given to show the effectiveness of our method.展开更多
文摘In this paper, we present our research on building computing machines consciousness about intuitive geometry based on mathematics experiments and statistical inference. The investigation consists of the following five steps. At first, we select a set of geometric configurations and for each configuration we construct a large amount of geometric data as observation data using dynamic geometry programs together with the pseudo-random number generator. Secondly, we refer to the geometric predicates in the algebraic method of machine proof of geometric theorems to construct statistics suitable for measuring the approximate geometric relationships in the observation data. In the third step, we propose a geometric relationship detection method based on the similarity of data distribution, where the search space has been reduced into small batches of data by pre-searching for efficiency, and the hypothetical test of the possible geometric relationships in the search results has be performed. In the fourth step, we explore the integer relation of the line segment lengths in the geometric configuration in addition. At the final step, we do numerical experiments for the pre-selected geometric configurations to verify the effectiveness of our method. The results show that computer equipped with the above procedures can find out the hidden geometric relations from the randomly generated data of related geometric configurations, and in this sense, computing machines can actually attain certain consciousness of intuitive geometry as early civilized humans in ancient Mesopotamia.
文摘We present a symbolic-numeric hybrid method, based on sum-of-squares （SOS） relaxation and rational vec- tor recovery, to compute inequality invariants and ranking functions for proving total correctness and generating pre- conditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate rank- ing functions with floating point coefficients. Then Gauss- Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several exam- ples are given to show the effectiveness of our method.
