Part of the book series:Lecture Notes in Computer Science ((LNAI,volume 14101))
Included in the following conference series:
480Accesses
Abstract
We contribute a new dataset composed of more than 41K MetiTarski challenges that can be used to investigate applications of machine learning (ML) in determining efficient variable orderings in Cylindrical Algebraic Decomposition. The proposed dataset aims to address inadvertent bias issues present in prior benchmarks, paving the way to development of robust, easy-to-generalize ML models.
This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. HR00112290064. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Government or DARPA.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 8579
- Price includes VAT (Japan)
- Softcover Book
- JPY 10724
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reasoning44, 175–205 (2010)
England, M., Florescu, D.: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS (LNAI), vol. 11617, pp. 93–108. Springer, Cham (2019).https://doi.org/10.1007/978-3-030-23250-4_7
Geirhos, R., Rubisch, P., Michaelis, C., Bethge, M., Wichmann, F.A., Brendel, W.: Imagenet-trained CNNs are biased towards texture; increasing shape bias improves accuracy and robustness. In: International Conference on Learning Representations (2019).https://openreview.net/forum?id=Bygh9j09KX
Geirhos, R., Temme, C.R., Rauber, J., Schütt, H.H., Bethge, M., Wichmann, F.A.: Generalisation in humans and deep neural networks. Adv. Neur. Inf. Proc.31 (2018)
Huang, Z., England, M., Wilson, D.J., Bridge, J., Davenport, J.H., Paulson, L.C.: Using machine learning to improve CAD. Maths. in C.S.13(4), 461–488 (2019)
Kawaguchi, K., Kaelbling, L.P., Bengio, Y.: Generalization in deep learning. arXiv preprintarXiv:1710.05468 (2017)
Passmore, G.O., Paulson, L.C., de Moura, L.: Real algebraic strategies for metitarski proofs. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 358–370. Springer, Heidelberg (2012).https://doi.org/10.1007/978-3-642-31374-5_24
Scarselli, F., Gori, M., Tsoi, A.C., Hagenbuchner, M., Monfardini, G.: The graph neural network model. IEEE Trans. Neural Netw.20(1), 61–80 (2009)
Vaswani, A., et al.: Attention is all you need. In: Advances in Neural Information Processing Systems, vol. 30 (2017)
Author information
Authors and Affiliations
Imandra Inc., Austin, TX, 78704, USA
John Hester & Grant Passmore
SRI International, Menlo Park, CA, 94025, USA
Briland Hitaj, Sam Owre, Natarajan Shankar & Eric Yeh
- John Hester
You can also search for this author inPubMed Google Scholar
- Briland Hitaj
You can also search for this author inPubMed Google Scholar
- Grant Passmore
You can also search for this author inPubMed Google Scholar
- Sam Owre
You can also search for this author inPubMed Google Scholar
- Natarajan Shankar
You can also search for this author inPubMed Google Scholar
- Eric Yeh
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toGrant Passmore.
Editor information
Editors and Affiliations
ENSIIE, Evry, France
Catherine Dubois
University of Birmingham, Birmingham, UK
Manfred Kerber
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Hester, J., Hitaj, B., Passmore, G., Owre, S., Shankar, N., Yeh, E. (2023). An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning. In: Dubois, C., Kerber, M. (eds) Intelligent Computer Mathematics. CICM 2023. Lecture Notes in Computer Science(), vol 14101. Springer, Cham. https://doi.org/10.1007/978-3-031-42753-4_21
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-031-42752-7
Online ISBN:978-3-031-42753-4
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative