Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.
OriginalsprogEngelsk
TitelIntelligent Computer Mathematics : Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015)
RedaktørerManfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
ForlagSpringer
Publikationsdato2015
Sider55-70
ISBN (Trykt)978-3-319-20614-1
ISBN (Elektronisk)978-3-319-20615-8
DOI
StatusUdgivet - 2015
Begivenhed8th International Conference on Intelligent Computer Mathematics - Washington, USA
Varighed: 13. jul. 201517. jul. 2015

Konference

Konference8th International Conference on Intelligent Computer Mathematics
LandUSA
ByWashington
Periode13/07/201517/07/2015
NavnLecture Notes in Computer Science
Vol/bind9150
ISSN0302-9743

Fingeraftryk

Sorting
Program processors
Data storage equipment

Citer dette

Cruz-Filipe, L., & Schneider-Kamp, P. (2015). Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. I M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, & V. Sorge (red.), Intelligent Computer Mathematics: Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015) (s. 55-70). Springer. Lecture Notes in Computer Science, Bind. 9150 https://doi.org/10.1007/978-3-319-20615-8_4
Cruz-Filipe, Luís ; Schneider-Kamp, Peter. / Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. Intelligent Computer Mathematics: Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015). red. / Manfred Kerber ; Jacques Carette ; Cezary Kaliszyk ; Florian Rabe ; Volker Sorge. Springer, 2015. s. 55-70 (Lecture Notes in Computer Science, Bind 9150).
@inproceedings{16ee8c23ebf1482e95263b40862c464e,
title = "Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof",
abstract = "In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.",
author = "Lu{\'i}s Cruz-Filipe and Peter Schneider-Kamp",
year = "2015",
doi = "10.1007/978-3-319-20615-8_4",
language = "English",
isbn = "978-3-319-20614-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "55--70",
editor = "Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge",
booktitle = "Intelligent Computer Mathematics",
address = "Germany",

}

Cruz-Filipe, L & Schneider-Kamp, P 2015, Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. i M Kerber, J Carette, C Kaliszyk, F Rabe & V Sorge (red), Intelligent Computer Mathematics: Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015). Springer, Lecture Notes in Computer Science, bind 9150, s. 55-70, 8th International Conference on Intelligent Computer Mathematics, Washington, USA, 13/07/2015. https://doi.org/10.1007/978-3-319-20615-8_4

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. / Cruz-Filipe, Luís; Schneider-Kamp, Peter.

Intelligent Computer Mathematics: Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015). red. / Manfred Kerber; Jacques Carette; Cezary Kaliszyk; Florian Rabe; Volker Sorge. Springer, 2015. s. 55-70 (Lecture Notes in Computer Science, Bind 9150).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof

AU - Cruz-Filipe, Luís

AU - Schneider-Kamp, Peter

PY - 2015

Y1 - 2015

N2 - In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.

AB - In recent work, we formalized the theory of optimal-size sorting networks with the goal of extracting a verified checker for the large-scale computer-generated proof that 25 comparisons are optimal when sorting 9 inputs, which required more than a decade of CPU time and produced 27 GB of proof witnesses. The checker uses an untrusted oracle based on these witnesses and is able to verify the smaller case of 8 inputs within a couple of days, but it did not scale to the full proof for 9 inputs. In this paper, we describe several non-trivial optimizations of the algorithm in the checker, obtained by appropriately changing the formalization and capitalizing on the symbiosis with an adequate implementation of the oracle. We provide experimental evidence of orders of magnitude improvements to both runtime and memory footprint for 8 inputs, and actually manage to check the full proof for 9 inputs.

U2 - 10.1007/978-3-319-20615-8_4

DO - 10.1007/978-3-319-20615-8_4

M3 - Article in proceedings

SN - 978-3-319-20614-1

T3 - Lecture Notes in Computer Science

SP - 55

EP - 70

BT - Intelligent Computer Mathematics

A2 - Kerber, Manfred

A2 - Carette, Jacques

A2 - Kaliszyk, Cezary

A2 - Rabe, Florian

A2 - Sorge, Volker

PB - Springer

ER -

Cruz-Filipe L, Schneider-Kamp P. Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof. I Kerber M, Carette J, Kaliszyk C, Rabe F, Sorge V, red., Intelligent Computer Mathematics: Proceedings of the 8th Conference on Intelligent Computer Mathematics (CICM 2015). Springer. 2015. s. 55-70. (Lecture Notes in Computer Science, Bind 9150). https://doi.org/10.1007/978-3-319-20615-8_4