add some notes to the automated section (teorth#919)

amirlb · Nov 25, 2024 · dbc459b · dbc459b
1 parent 11f0dba
commit dbc459b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/paper/automated.tex b/paper/automated.tex
@@ -25,3 +25,5 @@ \section{Automated Theorem Proving}\label{automated-sec}
 Make a note of the possible alternate strategy to prove implications outlined \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Ideas.20for.20unknown.20implications}{here}.
 
 Talk about how ATPs have been important to guide counterexample strategy by testing what simplifying hypotheses can be safely added without eliminating the possibility of a refutation.
+
+Framing: as we likely do not have experts in carefully evaluating and benchmarking ATP performance, do not present our work as definitively establishing performance of ATPs on ETP problems; instead, present our work as a more informal ``field report'' documenting our experiences but not necessarily drawing firm conclusions.  To quote from Jose Brox: ``center on what we can contribute to novice ATP users, algebra (or perhaps general) researchers who, as some of us at the start of this project, want to use ATPs for the first time on problems that need them, and may be at a loss of what to use, what parameters may be important... in summary, what may make a difference. Here we can be more informal, throw a couple of "benchmarking" tables for the same ATP with different parameters and for different ATPs, talk about some relative gains in time (changing parameters we saw a 500 times speedup on this particular problem), etc. This is knowledge I think we have gained to some extent, and certainly I would have been glad to receive this kind of hints before we started!''.  Then leave it as an interesting open problem to properly develop and measure benchmarks for ATPs based on this project.
diff --git a/paper/main.pdf b/paper/main.pdf
Original file line number	Diff line number	Diff line change
Expand Up		@@ -25,3 +25,5 @@ \section{Automated Theorem Proving}\label{automated-sec}
		Make a note of the possible alternate strategy to prove implications outlined \href{https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Ideas.20for.20unknown.20implications}{here}.

		Talk about how ATPs have been important to guide counterexample strategy by testing what simplifying hypotheses can be safely added without eliminating the possibility of a refutation.

		Framing: as we likely do not have experts in carefully evaluating and benchmarking ATP performance, do not present our work as definitively establishing performance of ATPs on ETP problems; instead, present our work as a more informal ``field report'' documenting our experiences but not necessarily drawing firm conclusions. To quote from Jose Brox: ``center on what we can contribute to novice ATP users, algebra (or perhaps general) researchers who, as some of us at the start of this project, want to use ATPs for the first time on problems that need them, and may be at a loss of what to use, what parameters may be important... in summary, what may make a difference. Here we can be more informal, throw a couple of "benchmarking" tables for the same ATP with different parameters and for different ATPs, talk about some relative gains in time (changing parameters we saw a 500 times speedup on this particular problem), etc. This is knowledge I think we have gained to some extent, and certainly I would have been glad to receive this kind of hints before we started!''. Then leave it as an interesting open problem to properly develop and measure benchmarks for ATPs based on this project.