Jiaqi Huang


2 Positive Bias and Length Bias in Deep Neural Networks for Premises Selection

Authors: Jiaqi Huang, Yuheng Wang


Premises selection, the task of selecting a set of axioms for proving a given conjecture, is a major bottleneck in automated theorem proving. An array of deep-learning-based methods has been established for premises selection, but a perfect performance remains challenging. Our study examines the inaccuracy of deep neural networks in premises selection. Through training network models using encoded conjecture and axiom pairs from the Mizar Mathematical Library, two potential biases are found: the network models classify more premises as necessary than unnecessary, referred to as the ‘positive bias’, and the network models perform better in proving conjectures that paired with more axioms, referred to as ‘length bias’. The ‘positive bias’ and ‘length bias’ discovered could inform the limitation of existing deep neural networks.

Keywords: Deep learning, Automated Theorem Proving, premises selection, interpreting deep learning

Procedia PDF Downloads 11
1 Convergence Analysis of a Gibbs Sampling Based Mix Design Optimization Approach for High Compressive Strength Pervious Concrete

Authors: Jiaqi Huang, Lu Jin


Pervious concrete features with high water permeability rate. However, due to the lack of fine aggregates, the compressive strength is usually lower than other conventional concrete products. Optimization of pervious concrete mix design has long been recognized as an effective mechanism to achieve high compressive strength while maintaining desired permeability rate. In this paper, a Gibbs Sampling based algorithm is proposed to approximate the optimal mix design to achieve a high compressive strength of pervious concrete. We prove that the proposed algorithm efficiently converges to the set of global optimal solutions. The convergence rate and accuracy depend on a control parameter employed in the proposed algorithm. The simulation results show that, by using the proposed approach, the system converges to the optimal solution quickly and the derived optimal mix design achieves the maximum compressive strength while maintaining the desired permeability rate.

Keywords: Convergence, pervious concrete, Gibbs Sampling, high compressive strength, optimal mix design

Procedia PDF Downloads 35