init

evaluation/few_shot_prompts/__init__.py

@@ -0,0 +1,11 @@
+from .cot_minerva_math_4_shot import MinervaMathPrompt
+from .cot_gsm_8_shot import CoTGSMPrompt
+from .cot_math_sat_4_shot import CoTSATPrompt
+from .cot_mmlu_stem_4_shot import MMLUSTEMPrompt
+from .cot_ocwcourses_4_shot import OCWCoursesPrompt
+from .pal_gsm_8_shot import PALGSMPrompt
+from .pal_math_4_shot import PALMathPrompt
+from .minif2f_isabelle import MiniF2FIsabellePrompt
+from .cot_cmath_6_shot import CoTCMATHPrompt
+from .cot_gaokao_mathcloze_5_shot import CoTGaoKaoMathClozePrompt
+from .cot_gaokao_mathqa_5_shot import CoTGaoKaoMathQAPrompt

evaluation/few_shot_prompts/cot_cmath_6_shot.py

@@ -0,0 +1,37 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+问题：芳芳买了一本书有99页，看了90页，她还剩多少页没有看？
+答案：还剩的没有看的页数=书的总页数-芳芳看了的页数，99-90=9。所以答案是：9。
+
+
+问题：张师傅上午修了18把椅子，下午修了29把椅子，一天共修了多少把椅子？
+答案：一天共修的椅子数量=上午修的椅子数量+下午修的椅子数量，18+29=47。所以答案是：47。
+
+
+问题：小猴摘了84个桃子，平均分给6只猴子，每只猴子能吃到几个桃子？
+答案：每只猴子能吃到的桃子数=总桃子数/猴子的数量，84/6=14。所以答案是：14。
+
+
+问题：用面包机烤面包时，第一面烤2分钟，第二面只要烤1分钟，即烤一片面包需要3分钟，小勤的面包机一次只能放2片，他每天早上吃3片面包，至少需要烤多少分钟？
+答案：可以现将两片面包放入面包机烤2分钟，再将其中一片拿出来，将第三片面包放进去，烤1分钟，这样第一片面包就烤好了，将第一片面包拿出来将第二片面包放进去，继续烤1分钟，于是第二片面包也烤好了将其拿出来，第三片面包再烤1分钟也就烤好了，一共是2+1+1=5。所以答案是：5。
+
+
+问题：一组学生植树，每人栽6棵还剩4棵；如果其中3人各栽5棵，其余每人各栽7棵，正好栽完。这一组学生有多少人？
+答案：假设学生的数量是x，每人栽6棵还剩4棵，也就是说树苗的数量=6x+4，又知道如果其中3人各栽5棵，其余每人各栽7棵，正好栽完，即6x+4=3*5+(x-3)*7，化简方程得到：x=10。所以答案是：10。
+
+
+问题：某小学在“献爱心--为汶川地震区捐款”活动中，六年级五个班共捐款8000元，其中一班捐款1500元，二班比一班多捐款200元，三班捐款1600元，四班与五班捐款数之比是3：5．四班捐款多少元？
+答案：一班捐款1500元，而二班比一班多捐200元，所以二班捐款1500+200=1700元，又知道六年级五个班一共捐款8000元，所以四班和五班捐款之和 = 一共捐款 - 一班和二班和三班捐款之和，即8000-1500-1700-1600=3200元，而题目说四班与五班捐款数之比是3：5，则四班捐款了3200/(3+5)*3=1200元。所以答案是：1200。
+""".strip()
+
+class CoTCMATHPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\n\n问题：{task_input}\n答案：{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\n问题："]

evaluation/few_shot_prompts/cot_gaokao_mathcloze_5_shot.py

@@ -0,0 +1,57 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+问题 1.   设数列 $\\left\\{a_{n}\\right\\}$ 的前 $n$ 项和为 $S_{n}$, 且 $a_{1}=-1, a_{n+1}=S_{n+1} S_{n}$, 则 $S_{n}=(\\quad)$.
+问题 1的解析:   让我们写出这个数列的前n项和：
+$S_n = a_1 + a_2 + ... + a_n$
+$S_n = -1 + (S_2 S_1) + (S_3 S_2) + ... + (S_{n+1} S_n)$
+$S_n = -1 + (S_2 S_1) + (S_3 S_2) + ... + (S_n S_{n-1}) + (S_{n+1} S_n)$
+$S_n = -1 + S_n (S_{n+1} - S_1)$
+$S_n - S_n S_{n+1} = -1 - S_n$
+$S_n (1 - S_{n+1}) = -1 - S_n$
+$S_n = -\\frac{1}{1 - S_{n+1}}$
+因为这个数列后面的所有项都是0，我们可以看到对于所有$n\\geq 1$，$S_{n+1} = 0$。因此，我们有：
+$S_n = -\\frac{1}{1 - S_{n+1}} = -\\frac{1}{1 - 0} = -1$
+这个数列前n项和的公式是$S_n = -\\frac{1}{n}$。
+答案是 $-\\frac{1}{n}$
+
+
+问题 2.   若 $\\left(x+\\frac{1}{x}\\right)^{n}$ 的展开式中第 3 项与第 7 项的二项式系数相等, 则该展 开式中 $\\frac{1}{x^{2}}$ 的系数为 $(\\quad)$.
+问题 2的解析:   由题意可得, $c_{n}^{2}=c_{n}^{6}$
+$\\therefore n=8$
+展开式的通项 T_{r+1}=C_8^r x^{8-r}\\left(\\frac{1}{x}\\right)^r=C_8^r x^{8-2 r}$
+令 $8-2 r=-2$ 可得 $r=5$
+此时系数为 $c_{8}^{5}=56$
+答案是 56
+
+
+问题 3.   函数 $\\mathrm{f}(\\mathrm{x})=\\sin (\\mathrm{x}+2 \\phi)-2 \\sin \\phi \\cos (\\mathrm{x}+\\phi)$ 的最大值为 $(\\quad)$.
+问题 3的解析:   函数 $f(x)=\\sin (x+2 \\phi)-2 \\sin \\phi \\cos (x+\\phi)=\\sin [(x+\\phi)+\\phi]-$ $2 \\sin \\phi \\cos (x+\\phi)$
+$=\\sin (x+\\phi) \\cos \\phi+\\cos (x+\\phi) \\sin \\phi-2 \\sin \\phi \\cos (x+\\phi)=\\sin (x+\\phi) \\cos \\phi-\\cos$ $(x+\\phi) \\sin \\phi$ $=\\sin [(x+\\phi)-\\phi]=\\sin x$
+故函数 $f(x)$ 的最大值为 1
+答案是 1
+
+
+问题 4.   已知向量 $\\vec{a}=(3,1), \\vec{b}=(1,0), \\vec{c}=\\vec{a}+k \\vec{b}$. 若 $\\vec{a} \\perp \\vec{c}$, 则 $k=(\\quad)$
+问题 4的解析:   \\because \\vec{a}=(3,1), \\vec{b}=(1,0), \\therefore \\vec{c}=\\vec{a}+k \\vec{b}=(3+k, 1)$ ，
+$\\because \\vec{a} \\perp \\vec{c}, \\therefore \\vec{a} \\square \\vec{c}=3(3+k)+1 \\times 1=0$, 解得 $k=-\\frac{10}{3}$
+答案是 $-\\frac{10}{3}$
+
+
+问题 5.   设向量 $\\vec{a}, \\vec{b}$ 不平行, 向量 $\\lambda \\vec{a}+\\vec{b}$ 与 $\\vec{a}+2 \\vec{b}$ 平行, 则实数 $\\lambda=(\\quad)$.
+问题 5的解析:   $\\because$ 向量 $\\vec{a}, \\vec{b}$ 不平行, 向量 $\\lambda \\vec{a}+\\vec{b}$ 与 $\\vec{a}+2 \\vec{b}$ 平行,
+$\\therefore \\lambda \\vec{a}+\\vec{b}=t(\\vec{a}+2 \\vec{b})=t \\vec{a}+2 t \\vec{b}$
+$\\therefore\\left\\{\\begin{array}{c}\\lambda=\\mathrm{t} \\\\ 1=2 \\mathrm{t},\\end{array}\\right.$ 解得实数 $\\lambda=\\frac{1}{2}$.
+答案是 $\\frac{1}{2}$
+""".strip()
+
+class CoTGaoKaoMathClozePrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\n\n问题 6.   {task_input}\n问题 6的解析:   {task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\n问题 "]

evaluation/few_shot_prompts/cot_gaokao_mathqa_5_shot.py

@@ -0,0 +1,57 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+问题 1.    已知 $\\alpha, \\beta, \\gamma$ 是互不相同的锐角, 则在 $\\sin \\alpha \\cos \\beta, \\sin \\beta \\cos \\gamma, \\sin \\gamma \\cos \\alpha$ 三个值中, 大于 $\\frac{1}{2}$ 的个数的最大值是 ($\\quad$)
+从以下选项中选择:    (A)0 (B)1 (C)2 (D)3
+问题 1的解析:   1. 如果 $\\alpha, \\beta, \\gamma$ 均小于 $60^\\circ$，那么他们的正弦值都小于 $\\frac{1}{2}$，因此三个值中不可能有大于 $\\frac{1}{2}$ 的值。
+2. 如果有一个角大于 $60^\\circ$，假设为 $\\alpha$，那么对应的正弦值大于 $\\frac{1}{2}$。此时，由于三角形内角和为 $180^\\circ$，所以 $\\beta + \\gamma < 120^\\circ$。这意味着 $\\beta, \\gamma$ 的余弦值均大于 $\\frac{1}{2}$，所以此时 $\\sin \\alpha \\cos \\beta > \\frac{1}{2}, \\sin \\beta \\cos \\gamma > \\frac{1}{2}$。
+3. 如果有两个角大于 $60^\\circ$，例如 $\\alpha$ 和 $\\beta$，那么由于三角形内角和为 $180^\\circ$，我们可以得到 $\\gamma < 60^\\circ$，此时 $\\sin \\gamma < \\frac{1}{2}$。由于 $\\alpha$ 和 $\\beta$ 
+的余弦值都小于 $\\frac{1}{2}$，因此三个值中不可能有大于 $\\frac{1}{2}$ 的值。
+4. 如果三个角都大于 $60^\\circ$，显然不符合题意。
+综上所述，当有一个角大于 $60^\\circ$ 时，大于 $\\frac{1}{2}$ 的个数的最大值是 2。
+答案是 C
+
+
+问题 2.    正方体 $A B C D-A_{1} B_{1} C_{1} D_{1}$ 中, $B B_{1}$ 与平面 $A C D_{1}$ 所成角的余弦值为 ($\\qquad$)
+从以下选项中选择:    (A)$\\frac{\\sqrt{2}}{3}$ (B)$\\frac{\\sqrt{3}}{3}$ (C)$\\frac{2}{3}$ (D)$\\frac{\\sqrt{6}}{3}$
+问题 2的解析:   设上下底面的中心分别为 $\\mathrm{O}_{1}, \\mathrm{O}$, 设正方体的棱长等于 1 , 则 $O_{1} O$ 与平面 $A C D_{1}$ 所成角就是 $B B_{1}$ 与平面 $A C D_{1}$ 所成角, 即 $\\angle O_{1} O D_{1}$,
+直角三角形 $\\mathrm{OO}_{1} \\mathrm{D}_{1}$ 中, $\\cos \\angle \\mathrm{O}_{1} \\mathrm{OD}_{1}=\\frac{\\mathrm{O}_{1} \\mathrm{O}}{\\mathrm{OD}_{1}}=\\frac{\\frac{1}{\\sqrt{6}}}{2}=\\frac{\\sqrt{6}}{3}$. 
+答案是 C
+
+
+问题 3.    设函数 $f(x)=\\left\\{\\begin{array}{ll}1+\\log _{2}(2-x), & x<1 \\ 2^{x-1}, & x \\geqslant 1,\\end{array}\\right.$ 则 $f(-2)+f\\left(\\log _{2} 12\\right)=$ ($\\qquad$)
+从以下选项中选择:    (A)3 (B)6 (C)9 (D)12
+问题 3的解析:   首先，我们可以根据定义计算 $f(-2)$ 和 $f(\\log_2 12)$：
+$f(-2)=1+\\log_2(2-(-2))=1+\\log_2 4=3$
+$f(\\log_2 12)=2^{\\log_2 12-1}=6$
+因此，$f(-2)+f(\\log_2 12)=3+6=9$。
+答案是 C
+
+
+问题 4.    已知函数 $f(x)=a x^{3}-3 x^{2}+1$, 若 $f(x)$ 存在唯一的零点 $x_{0}$, 且 $x_{0}>$ 0 , 则实数 $\\mathrm{a}$ 的取值范围是 ($\\qquad$)
+从以下选项中选择:    (A)$(1,+\\infty)$ (B)$(2,+\\infty)$ (C)$(-\\infty,-1)$ (D)$(-\\infty,-2)$
+问题 4的解析:   首先，我们可以通过求出函数的导函数 $f'(x)$ 来判断函数在 $x>0$ 区间内的单调性。在这里，我们求出导函数 $f'(x)$ 为 $f'(x)=3ax^2-6x$。
+然后，我们需要求出导函数 $f'(x)$ 的零点，以确定函数 $f(x)$ 在 $x>0$ 区间内的单调性。导函数 $f'(x)$ 的零点为 $x=0$ 和 $x=\\frac{2}{\\sqrt{a}}$。注意到 $x>0$，所以我们得到 $a<0$。此外，由于函数 $f(x)$ 在 $x=0$ 处的函数值为 $1$，因此不能有 $a=\\frac{4}{3}$。
+综上所述，当 $a$ 的取值范围为 $a<-\\frac{4}{3}$ 时，函数 $f(x)$ 在 $x>0$ 区间内是单调递减的，此时存在唯一的零点 $x_0$。因此，答案为 $(-\\infty,-2)$。
+答案是 D
+
+
+问题 5.    设 $\\left\\{a_{n}\\right\\}$ 是公差不为 0 的无穷等差数列, 则“ $\\left\\{a_{n}\\right\\}$ 为递增数列”是“存在正整数 $N_{0}$, 当 $n>N_{0}$ 时, $a_{n}>0$ ”的 ($\\quad$)
+从以下选项中选择:    (A)充分而不必要条件 (B)必要而不充分条件 (C)充分必要条件 (D)既不充分也不必要条件
+问题 5的解析:   首先，我们可以通过举例来判断该条件是充分还是必要条件。如果一个数列递增，那么它的公差一定大于 0，也就是存在正整数 $N_{0}$，当 $n>N_{0}$ 时，$a_{n}>0$。因此，“ $\\left\\{a_{n}\\right\\}$ 为递增数列”是“存在正整数 $N_{0}$, 当 $n>N_{0}$ 时, $a_{n}>0$ ”的必要条件。
+接下来，我们需要判断是否充分。也就是说，如果存在正整数 $N_{0}$，当 $n>N_{0}$ 时，$a_{n}>0$，那么能否得出“ $\\left\\{a_{n}\\right\\}$ 为递增数列”这一结论。
+答案是肯定的。因为如果 $a_{n}>0$，那么 $a_{n+1}-a_{n}>0$，即公差大于 0，因此该数列是递增的。因此，该条件是充分条件。
+综上所述，选项为 (C) 充分必要条件。
+答案是 C
+""".strip()
+
+class CoTGaoKaoMathQAPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\n\n问题 6.    {task_input}\n问题 6的解析:   {task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\n问题 "]

evaluation/few_shot_prompts/cot_gsm_8_shot.py

@@ -0,0 +1,45 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+Q: There are 15 trees in the grove. Grove workers will plant trees in the grove today. After they are done, there will be 21 trees. How many trees did the grove workers plant today?
+A: There are 15 trees originally. Then there were 21 trees after some more were planted. So there must have been 21 - 15 = 6. The answer is 6.
+
+
+Q: If there are 3 cars in the parking lot and 2 more cars arrive, how many cars are in the parking lot?
+A: There are originally 3 cars. 2 more cars arrive. 3 + 2 = 5. The answer is 5.
+
+
+Q: Leah had 32 chocolates and her sister had 42. If they ate 35, how many pieces do they have left in total?
+A: Originally, Leah had 32 chocolates. Her sister had 42. So in total they had 32 + 42 = 74. After eating 35, they had 74 - 35 = 39. The answer is 39.
+
+
+Q: Jason had 20 lollipops. He gave Denny some lollipops. Now Jason has 12 lollipops. How many lollipops did Jason give to Denny?
+A: Jason started with 20 lollipops. Then he had 12 after giving some to Denny. So he gave Denny 20 - 12 = 8. The answer is 8.
+
+
+Q: Shawn has five toys. For Christmas, he got two toys each from his mom and dad. How many toys does he have now?
+A: Shawn started with 5 toys. If he got 2 toys each from his mom and dad, then that is 4 more toys. 5 + 4 = 9. The answer is 9.
+
+
+Q: There were nine computers in the server room. Five more computers were installed each day, from monday to thursday. How many computers are now in the server room?
+A: There were originally 9 computers. For each of 4 days, 5 more computers were added. So 5 * 4 = 20 computers were added. 9 + 20 is 29. The answer is 29.
+
+
+Q: Michael had 58 golf balls. On tuesday, he lost 23 golf balls. On wednesday, he lost 2 more. How many golf balls did he have at the end of wednesday?
+A: Michael started with 58 golf balls. After losing 23 on tuesday, he had 58 - 23 = 35. After losing 2 more, he had 35 - 2 = 33 golf balls. The answer is 33.
+
+
+Q: Olivia has $23. She bought five bagels for $3 each. How much money does she have left?
+A: Olivia had 23 dollars. 5 bagels for 3 dollars each will be 5 x 3 = 15 dollars. So she has 23 - 15 dollars left. 23 - 15 is 8. The answer is 8.
+""".strip()
+
+class CoTGSMPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\n\nQ: {task_input}\nA: {task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nQ:"]

evaluation/few_shot_prompts/cot_math_sat_4_shot.py

@@ -0,0 +1,59 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+Problem:
+Find the domain of the expression $\\frac{\\sqrt{x-2}}{\\sqrt{5-x}}$.
+What of the following is the right choice? Explain your answer.
+(A) [-5,-2), (B) [2,5), (C) [-2,-5), (D) [5,2)
+Solution:
+The expressions inside each square root must be non-negative. Therefore, $x-2 \\ge 0$, so $x\\ge2$, and $5 - x \\ge 0$, so $x \\le 5$. Also, the denominator cannot be equal to zero, so $5-x>0$, which gives $x<5$.
+Therefore, the domain of the expression is $\\boxed{[2,5)}$.
+Final Answer: The final answer is (B). I hope it is correct.
+
+Problem:
+If $\\det \\mathbf{A} = 2$ and $\\det \\mathbf{B} = 12,$ then find $\\det (\\mathbf{A} \\mathbf{B}).$
+What of the following is the right choice? Explain your answer.
+(A) 14, (B) 4, (C) 2, (D) 24
+Solution:
+We have that $\\det (\\mathbf{A} \\mathbf{B}) = (\\det \\mathbf{A})(\\det \\mathbf{B}) = (2)(12) = \\boxed{24}.$
+Final Answer: The final answer is (D). I hope it is correct.
+
+Problem:
+Terrell usually lifts two 20-pound weights 12 times. If he uses two 15-pound weights instead, how many times must Terrell lift them in order to lift the same total weight?
+What of the following is the right choice? Explain your answer.
+(A) 12, (B) 20, (C) 16, (D) 15
+Solution:
+If Terrell lifts two 20-pound weights 12 times, he lifts a total of $2\\cdot 12\\cdot20=480$ pounds of weight. If he lifts two 15-pound weights instead for $n$ times, he will lift a total of $2\\cdot15\\cdot n=30n$ pounds of weight. Equating this to 480 pounds, we can solve for $n$: \\begin{align*}
+30n&=480\\\\
+\\Rightarrow\\qquad n&=480/30=\\boxed{16}
+\\end{align*}
+Final Answer: The final answer is (C). I hope it is correct.
+
+Problem:
+If the system of equations
+
+\\begin{align*}
+6x-4y&=a,\\\\
+6y-9x &=b.
+\\end{align*}has a solution $(x, y)$ where $x$ and $y$ are both nonzero, find $\\frac{a}{b},$ assuming $b$ is
+nonzero.
+What of the following is the right choice? Explain your answer.
+(A) $-\\frac{2}{3}$, (B) $\\frac{2}{3}$, (C) $\\frac{1}{3}$, (D) $\\frac{4}{9}$
+Solution:
+If we multiply the first equation by $-\\frac{3}{2}$, we obtain
+$$6y-9x=-\\frac{3}{2}a.$$Since we also know that $6y-9x=b$, we have
+
+$$-\\frac{3}{2}a=b\\Rightarrow\\frac{a}{b}=\\boxed{-\\frac{2}{3}}.$$
+Final Answer: The final answer is (A). I hope it is correct.
+""".strip()
+
+class CoTSATPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\nProblem:\n{task_input}\nSolution:\n{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nProblem:"]

evaluation/few_shot_prompts/cot_minerva_math_4_shot.py

@@ -0,0 +1,55 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """Problem:
+Find the domain of the expression $\\frac{\\sqrt{x-2}}{\\sqrt{5-x}}$.}
+
+Solution:
+The expressions inside each square root must be non-negative.
+Therefore, $x-2 \\ge 0$, so $x\\ge2$, and $5 - x \\ge 0$, so $x \\le 5$.
+Also, the denominator cannot be equal to zero, so $5-x>0$, which gives $x<5$.
+Therefore, the domain of the expression is $\\boxed{[2,5)}$.
+Final Answer: The final answer is $[2,5)$. I hope it is correct.
+
+Problem:
+If $\\det \\mathbf{A} = 2$ and $\\det \\mathbf{B} = 12,$ then find $\\det (\\mathbf{A} \\mathbf{B}).$
+
+Solution:
+We have that $\\det (\\mathbf{A} \\mathbf{B}) = (\\det \\mathbf{A})(\\det \\mathbf{B}) = (2)(12) = \\boxed{24}.$
+Final Answer: The final answer is $24$. I hope it is correct.
+
+Problem:
+Terrell usually lifts two 20-pound weights 12 times. If he uses two 15-pound weights instead, how many times must Terrell lift them in order to lift the same total weight?
+
+Solution:
+If Terrell lifts two 20-pound weights 12 times, he lifts a total of $2\\cdot 12\\cdot20=480$ pounds of weight.  If he lifts two 15-pound weights instead for $n$ times, he will lift a total of $2\\cdot15\\cdot n=30n$ pounds of weight.  Equating this to 480 pounds, we can solve for $n$: \\begin{align*}
+30n&=480\\\\
+\\Rightarrow\\qquad n&=480/30=\\boxed{16}
+\\end{align*}
+Final Answer: The final answer is $16$. I hope it is correct.
+
+Problem:
+If the system of equations
+
+\\begin{align*}
+6x-4y&=a,\\\\
+6y-9x &=b.
+\\end{align*}has a solution $(x, y)$ where $x$ and $y$ are both nonzero, find $\\frac{a}{b},$ assuming $b$ is nonzero.
+
+Solution:
+If we multiply the first equation by $-\\frac{3}{2}$, we obtain
+
+$$6y-9x=-\\frac{3}{2}a.$$Since we also know that $6y-9x=b$, we have
+
+$$-\\frac{3}{2}a=b\\Rightarrow\\frac{a}{b}=\\boxed{-\\frac{2}{3}}.$$
+Final Answer: The final answer is $-\\frac{2}{3}$. I hope it is correct."""
+
+class MinervaMathPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\nProblem:\n{task_input}\n\nSolution:\n{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nProblem:"]

evaluation/few_shot_prompts/cot_mmlu_stem_4_shot.py

@@ -0,0 +1,57 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """Problem:
+Find the domain of the expression $\\frac{\\sqrt{x-2}}{\\sqrt{5-x}}$.
+What of the following is the right choice? Explain your answer.
+(A) [-5,-2), (B) [2,5), (C) [-2,-5), (D) [5,2)
+Solution:
+The expressions inside each square root must be non-negative. Therefore, $x-2 \\ge 0$, so $x\\ge2$, and $5 - x \\ge 0$, so $x \\le 5$. Also, the denominator cannot be equal to zero, so $5-x>0$, which gives $x<5$.
+Therefore, the domain of the expression is $\\boxed{[2,5)}$.
+Final Answer: The final answer is (B). I hope it is correct.
+
+Problem:
+If $\\det \\mathbf{A} = 2$ and $\\det \\mathbf{B} = 12,$ then find $\\det (\\mathbf{A} \\mathbf{B}).$
+What of the following is the right choice? Explain your answer.
+(A) 14, (B) 4, (C) 2, (D) 24
+Solution:
+We have that $\\det (\\mathbf{A} \\mathbf{B}) = (\\det \\mathbf{A})(\\det \\mathbf{B}) = (2)(12) = \\boxed{24}.$
+Final Answer: The final answer is (D). I hope it is correct.
+
+Problem:
+Terrell usually lifts two 20-pound weights 12 times. If he uses two 15-pound weights instead, how many times must Terrell lift them in order to lift the same total weight?
+What of the following is the right choice? Explain your answer.
+(A) 12, (B) 20, (C) 16, (D) 15
+Solution:
+If Terrell lifts two 20-pound weights 12 times, he lifts a total of $2\\cdot 12\\cdot20=480$ pounds of weight. If he lifts two 15-pound weights instead for $n$ times, he will lift a total of $2\\cdot15\\cdot n=30n$ pounds of weight. Equating this to 480 pounds, we can solve for $n$: \\begin{align*}
+30n&=480\\\\
+\\Rightarrow\\qquad n&=480/30=\\boxed{16}
+\\end{align*}
+Final Answer: The final answer is (C). I hope it is correct.
+
+Problem:
+If the system of equations
+
+\\begin{align*}
+6x-4y&=a,\\\\
+6y-9x &=b.
+\\end{align*}has a solution $(x, y)$ where $x$ and $y$ are both nonzero, find $\\frac{a}{b},$ assuming $b$ is
+nonzero.
+What of the following is the right choice? Explain your answer.
+(A) $-\\frac{2}{3}$, (B) $\\frac{2}{3}$, (C) $\\frac{1}{3}$, (D) $\\frac{4}{9}$
+Solution:
+If we multiply the first equation by $-\\frac{3}{2}$, we obtain
+$$6y-9x=-\\frac{3}{2}a.$$Since we also know that $6y-9x=b$, we have
+
+$$-\\frac{3}{2}a=b\\Rightarrow\\frac{a}{b}=\\boxed{-\\frac{2}{3}}.$$
+Final Answer: The final answer is (A). I hope it is correct."""
+
+class MMLUSTEMPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\nProblem:\n{task_input}\nSolution:\n{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nProblem:"]

evaluation/few_shot_prompts/cot_ocwcourses_4_shot.py

@@ -0,0 +1,120 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """
+Problem:                                                                                
+Subproblem 0: What is the net charge of arginine in a solution of $\\mathrm{pH} 1.0$? 
+Please format your answer as +n or -n.                           
+Solution:
+The answer is +2.                                                     
+Final answer: The final answer is $\\boxed{+2}$. I hope it is correct.
+
+Problem:
+Subproblem 0: Let $z = 1 + \\sqrt{3} i$. Find $a, b$ that satisfy the equation 
+$z^4 = a + bi$. Express your answer as the ordered pair $(a,b)$.         
+Solution:
+$z^{4}$ has argument $4 \\pi / 3$ and radius 16 , so it's equal to $-8-8 \\sqrt{3} i$. 
+Thus $a = -8, b = -8\\sqrt 3$, and our answer is $(-8, -8\\sqrt{3})$.
+Final answer: The final answer is $\\boxed{(-8, -8\\sqrt{3})}$. I hope it is correct.
+
+Problem:
+Preamble: For each Laplace Transform \\(Y(s)\\), find the function \\(y(t)\\):
+Subproblem 0: 
+\\[Y(s)=\\frac{1}{(s+a)(s+b)}\\]
+Solution:
+We can simplify with partial fractions:
+\\[Y(s)=\\frac{1}{(s+a)(s+b)}=\\frac{C}{s+a}+\\frac{D}{s+b}\\]
+find the constants 
+\\(C\\) and \\(D\\) by setting \\(s=-a\\) and \\(s=-b\\)
+\\[
+  \\begin{aligned}
+  \\frac{1}{(s+a)(s+b)} &=\\frac{C}{s+a}+\\frac{D}{s+b} \\\\
+  1 &=C(s+b)+D(s+a) \\\\
+  C &=\\frac{1}{b-a} \\\\
+  D &=\\frac{1}{a-b}
+  \\end{aligned}
+\\]
+therefore
+\\[
+Y(s)=\\frac{1}{b-a} \\frac{1}{s+a}-\\frac{1}{b-a} \\frac{1}{s+b}
+\\]
+By looking up the inverse Laplace Transform of \\(\\frac{1}{s+b}\\), we find the total 
+solution \\(y(t)\\)
+\\[
+  y(t)=\\frac{e^{-a t}-e^{-b t}}{b-a}
+\\].
+Final answer: The final answer is $\\boxed{\\frac{e^{-a t}-e^{-b t}}{b-a}}$. I hope it is correct.
+
+Problem:
+Preamble: The following subproblems refer to the differential equation 
+$\\ddot{x}+b \\dot{x}+x=0$.
+Subproblem 0: What is the characteristic polynomial $p(s)$ of 
+$\\ddot{x}+b \\dot{x}+x=0$?
+Solution:
+The characteristic polynomial is $p(s)=s^{2}+b s+1$.
+Final answer: The final answer is $\\boxed{s^{2}+b s+1}$. I hope it is correct.
+""".strip()
+
+few_shot_prompt = """
+Problem:                                                                                
+Subproblem 0: What is the net charge of arginine in a solution of $\\mathrm{pH} 1.0$? 
+Please format your answer as +n or -n.                           
+Solution:
+The answer is +2.                                                     
+Final answer: The final answer is +2. I hope it is correct.
+
+Problem:
+Subproblem 0: Let $z = 1 + \\sqrt{3} i$. Find $a, b$ that satisfy the equation 
+$z^4 = a + bi$. Express your answer as the ordered pair $(a,b)$.         
+Solution:
+$z^{4}$ has argument $4 \\pi / 3$ and radius 16 , so it's equal to $-8-8 \\sqrt{3} i$. 
+Thus $a = -8, b = -8\\sqrt 3$, and our answer is $\\boxed{(-8, -8\\sqrt{3})}$.
+Final answer: The final answer is (-8, -8\\sqrt{3}). I hope it is correct.
+
+Problem:
+Preamble: For each Laplace Transform \\(Y(s)\\), find the function \\(y(t)\\):
+Subproblem 0: 
+\\[Y(s)=\\boxed{\\frac{1}{(s+a)(s+b)}}\\]
+Solution:
+We can simplify with partial fractions:
+\\[Y(s)=\\frac{1}{(s+a)(s+b)}=\\frac{C}{s+a}+\\frac{D}{s+b}\\]
+find the constants 
+\\(C\\) and \\(D\\) by setting \\(s=-a\\) and \\(s=-b\\)
+\\[
+  \\begin{aligned}
+  \\frac{1}{(s+a)(s+b)} &=\\frac{C}{s+a}+\\frac{D}{s+b} \\\\
+  1 &=C(s+b)+D(s+a) \\\\
+  C &=\\frac{1}{b-a} \\\\
+  D &=\\frac{1}{a-b}
+  \\end{aligned}
+\\]
+therefore
+\\[
+Y(s)=\\frac{1}{b-a} \\frac{1}{s+a}-\\frac{1}{b-a} \\frac{1}{s+b}
+\\]
+By looking up the inverse Laplace Transform of \\(\\frac{1}{s+b}\\), we find the total 
+solution \\(y(t)\\)
+\\[
+  y(t)=\\boxed{\\frac{1}{b-a}\\left(e^{-a t}-e^{-b t}\\right)}
+\\].
+Final answer: The final answer is \\[\\frac{1}{b-a}\\left(e^{-a t}-e^{-b t}\\right)\\]. I hope it is correct.
+
+Problem:
+Preamble: The following subproblems refer to the differential equation 
+$\\ddot{x}+b \\dot{x}+x=0$.
+Subproblem 0: What is the characteristic polynomial $p(s)$ of 
+$\\ddot{x}+b \\dot{x}+x=0$?
+Solution:
+The characteristic polynomial is $p(s)=\\boxed{s^{2}+b s+1}$.
+Final answer: The final answer is $s^{2}+b s+1$. I hope it is correct.
+""".strip()
+
+class OCWCoursesPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\nProblem:\n{task_input}\nSolution:\n{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nProblem:"]

evaluation/few_shot_prompts/few_shot_prompting.py

@@ -0,0 +1,9 @@
+class FewShotPrompting:
+    def __init__(self):
+        pass
+
+    def format_prompt(self, task_input, task_output):
+        pass
+
+    def stop_words(self):
+        pass

evaluation/few_shot_prompts/minif2f_isabelle.py

@@ -0,0 +1,418 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = {
+    'numbertheory': """Informal:
+(*### Problem
+
+Find the minimum value of $\\frac{9x^2\\sin^2 x + 4}{x\\sin x}$ for $0 < x < \\pi$. Show that it is 12.
+
+### Solution
+
+Let $y = x \\sin x$. It suffices to show that $12 \\leq \\frac{9y^2 + 4}{y}.
+It is trivial to see that $y > 0$. 
+Then one can multiply both sides by $y$ and it suffices to show $12y \\leq 9y^2 + 4$.
+This can be done by the sum of squares method.*)
+
+Formal:
+theorem aime_1983_p9:
+  fixes x::real
+  assumes "0<x" "x<pi"
+  shows "12 \\<le> ((9 * (x^2 * (sin x)^2)) + 4) / (x * sin x)"
+proof -
+  (* Let $y = x \\sin x$. *)
+  define y where "y=x * sin x"
+  (* It suffices to show that $12 \\leq \\frac{9y^2 + 4}{y}. *)
+  have "12 \\<le> (9 * y^2 + 4) / y"
+  proof -
+    (* It is trivial to see that $y > 0$. *)
+    have c0: "y > 0"
+      sledgehammer
+    (* Then one can multiply both sides by $y$ and it suffices to show $12y \\leq 9y^2 + 4$. *)
+    have "(9 * y^2 + 4) \\<ge> 12 * y" 
+      sledgehammer
+    then show ?thesis
+      sledgehammer
+  qed
+  then show ?thesis
+    sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+Find the greatest common factor of 180 and 168. Show that it is 12.
+
+### Solution
+
+This is true by simple evaluation.*)
+
+Formal:
+theorem mathd_numbertheory_188:
+  "gcd 180 168 = (12::nat)"
+  sledgehammer
+
+
+
+Informal:
+(*### Problem
+
+Show that for positive integer n, 2 divides $4^n$.
+
+### Solution
+
+Since n is positive, we can find a natural number m where $m+1=n$.
+Then we can show that 2 divides $4^{m+1}$. The conclusion thus follows.*)
+
+Formal:
+theorem numbertheory_2dvd4expn:
+  fixes n :: nat
+  assumes h0 : "n \\<noteq> 0"
+  shows "(2::nat) dvd 4^n"
+proof -
+  obtain m::nat where c0: "m+1=n"
+    sledgehammer
+  have "(2::nat) dvd 4^(m+1)" sledgehammer
+  then show ?thesis unfolding c0 sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+What is the remainder when $1 + 2 + 3 + 4 + \\dots + 9 + 10$ is divided by 9? Show that it is 1.
+
+### Solution
+
+This is true by simple evaluation.*)
+
+Formal:
+theorem mathd_numbertheory_466:
+  "(\\<Sum> k< 11. k) mod 9 = (1::nat)"
+  sledgehammer
+
+
+
+Informal:
+(*### Problem
+
+If $321_{b}$ is equal to the base 10 integer 57, find $b$ given that $b>0$. Show that it is 4.
+
+### Solution
+
+Converting $321_{b}$ to base 10 and setting it equal to 57, we find that  \\begin{align*} 3(b^2)+2(b^1)+1(b^0)&=57
+\\\\ 3b^2+2b+1&=57
+\\\\\\Rightarrow\\qquad 3b^2+2b-56&=0
+\\\\\\Rightarrow\\qquad (3b+14)(b-4)&=0
+\\end{align*}This tells us that $b$ is either $-\\frac{14}{3}$ or $4$. We know that $b>0$, so $b=4$.*)
+
+Formal:
+theorem mathd_numbertheory_48:
+  fixes b :: real
+  assumes h0 : "0<b"
+    and h1 : "3 * b^2 + 2 * b + 1 = 57"
+  shows "b=4"
+proof -
+  (* Converting $321_{b}$ to base 10 and setting it equal to 57, we find that  \\begin{align*} 3(b^2)+2(b^1)+1(b^0)&=57
+  \\\\ 3b^2+2b+1&=57
+  \\\\\\Rightarrow\\qquad 3b^2+2b-56&=0
+  \\\\\\Rightarrow\\qquad (3b+14)(b-4)&=0
+  \\end{align*} *)
+  have "0 = 3 * b^2 + 2 * b -56" using h1 sledgehammer
+  also have "... = (3*b+14)*(b-4)" sledgehammer
+  finally have "0 = (3*b+14)*(b-4)" sledgehammer
+  (* This tells us that $b$ is either $-\\frac{14}{3}$ or $4$. *)
+  then have "b = -14/3 ∨ b=4" sledgehammer
+  (* We know that $b>0$, so $b=4$. *)
+  then show ?thesis using h0 sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+When Rachel divides her favorite number by 7, she gets a remainder of 5. What will the remainder be if she multiplies her favorite number by 5 and then divides by 7? Show that it is 4.
+
+### Solution
+
+Let $n$ be Rachel's favorite number. 
+Then $n \\equiv 5 \\pmod{7}$, so $5n \\equiv 5 \\cdot 5 \\equiv 25 \\equiv 4 \\pmod{7}$.
+*)
+
+Formal:
+theorem mathd_numbertheory_335:
+  fixes n :: nat
+  assumes h0 : "n mod 7 = 5"
+  shows "(5 * n) mod 7 = 4"
+proof -
+  (* Then $n \\equiv 5 \\pmod{7}$, so $5n \\equiv 5 \\cdot 5 \\equiv 25 \\equiv 4 \\pmod{7}$. *)
+  have c0:"(5 * n) mod 7 = (5 * 5) mod 7" using h0
+    sledgehammer
+  then have "\\<dots> = 4" sledgehammer
+  then have "(5 * n) mod 7 = 4" using c0 sledgehammer
+  then show ?thesis sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+What positive two-digit integer is exactly twice the sum of its digits? Show that it is 18.
+
+### Solution
+
+We simplify $10a + b = 2(a+b)$ to get $8a = b$.
+Since $a$ is at least 1, $b$ is at least 8.
+We know $b$ is 8 since $8a = b$ and $a$ is a natural number.
+Hence $a$ is 1.
+The two-digit integer is hence $18$.
+*)
+
+Formal:
+theorem mathd_numbertheory_284:
+  fixes a b :: nat
+  assumes h0 : "1\\<le>a \\<and> a \\<le>9 \\<and> b \\<le>9"
+    and h1 : "10 * a + b = 2 * (a+b)"
+  shows "10 * a + b = 18"
+proof -
+  (* We simplify $10a + b = 2(a+b)$ to get $8a = b$. *)
+  have c0: "8 * a = b" using h1 sledgehammer
+  (* Since $a$ is at least 1, $b$ is at least 8. *)
+  hence "b \\<ge> 8" using h0 sledgehammer
+  (* We know $b$ is 8 since $8a = b$ and $a$ is a natural number. *)
+  hence c1:"b = 8" using h0 c0
+    sledgehammer
+  (* Hence $a$ is 1. *)
+  hence "a = 1" using c0 sledgehammer
+  (* The two-digit integer is hence $18$. *)
+  then show ?thesis using c1 sledgehammer
+qed
+
+
+
+""".strip(),
+    "other": """Informal:
+(*### Problem
+
+Find the minimum value of $\\frac{9x^2\\sin^2 x + 4}{x\\sin x}$ for $0 < x < \\pi$. Show that it is 12.
+
+### Solution
+
+Let $y = x \\sin x$. It suffices to show that $12 \\leq \\frac{9y^2 + 4}{y}.
+It is trivial to see that $y > 0$. 
+Then one can multiply both sides by $y$ and it suffices to show $12y \\leq 9y^2 + 4$.
+This can be done by the sum of squares method.*)
+
+Formal:
+theorem aime_1983_p9:
+  fixes x::real
+  assumes "0<x" "x<pi"
+  shows "12 \\<le> ((9 * (x^2 * (sin x)^2)) + 4) / (x * sin x)"
+proof -
+  (* Let $y = x \\sin x$. *)
+  define y where "y=x * sin x"
+  (* It suffices to show that $12 \\leq \\frac{9y^2 + 4}{y}. *)
+  have "12 \\<le> (9 * y^2 + 4) / y"
+  proof -
+    (* It is trivial to see that $y > 0$. *)
+    have c0: "y > 0"
+      sledgehammer
+    (* Then one can multiply both sides by $y$ and it suffices to show $12y \\leq 9y^2 + 4$. *)
+    have "(9 * y^2 + 4) \\<ge> 12 * y" 
+      sledgehammer
+    then show ?thesis
+      sledgehammer
+  qed
+  then show ?thesis
+    sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+Show that for any four complex numbers a, b, c, and d, $(a-d)(a-c)(a-b) = -(((a^2 - a(b+c)) + bc) * d) + (a^2 - a(b+c) + bc) * a$.
+
+### Solution
+
+We first see that $a^2 = a * a$ trivially.
+Unfolding this, the main equation holds true when terms are rearranged.*)
+
+Formal:
+theorem algebra_3rootspoly_amdtamctambeqnasqmbpctapcbtdpasqmbpctapcbta:
+  fixes a b c d :: complex
+  shows "(a-d) * (a-c) * (a-b) = -(((a^2 - (b+c) * a) + c * b) * d) + (a^2 - (b+c) * a + c * b) * a"
+proof -
+  (* We first see that $a^2 = a * a$ trivially. *)
+  have t0: "a^2 = a * a"
+    using power2_eq_square
+      sledgehammer
+  (* Unfolding this, the main equation holds true when terms are rearranged. *)
+  show ?thesis unfolding t0
+    sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+Find the greatest common factor of 180 and 168. Show that it is 12.
+
+### Solution
+
+This is true by simple evaluation.*)
+
+Formal:
+theorem mathd_numbertheory_188:
+  "gcd 180 168 = (12::nat)"
+  sledgehammer
+
+
+
+Informal:
+(*### Problem
+
+For how many positive integers $n$ is $n^2 - 3n + 2$ a [[prime]] number?
+
+$\\mathrm{(A)}\\ \\text{none}
+\\qquad\\mathrm{(B)}\\ \\text{one}
+\\qquad\\mathrm{(C)}\\ \\text{two}
+\\qquad\\mathrm{(D)}\\ \\text{more\\ than\\ two,\\ but\\ finitely\\ many}
+\\qquad\\mathrm{(E)}\\ \\text{infinitely\\ many}$ Show that it is \\mathrm{(B)}\\ \\text{one}.
+
+### Solution
+
+Factoring, we get $n^2 - 3n + 2 = (n-2)(n-1)$. 
+Either $n-1$ or $n-2$ is odd, and the other is even.  
+Their product must yield an even number.  
+The only prime that is even is $2$, which is when $n$ is $3$ or $0$. 
+Since $0$ is not a positive number, the answer is $\\mathrm{(B)}\\ \\text{one}$.*)
+
+Formal:
+theorem amc12b_2002_p3:
+  fixes n ::nat
+  assumes "n>0"
+    and prime:"prime (n^2+2-3*n)"
+  shows "n=3"
+proof -
+  have "n>2" 
+  proof (rule ccontr)
+    assume "\\<not> 2 < n"
+    then have "n=1 \\<or> n=2" using \\<open>n>0\\<close> sledgehammer
+    then show False using prime[THEN prime_gt_1_nat]
+      sledgehammer
+  qed
+  (* Factoring, we get $n^2 - 3n + 2 = (n-2)(n-1)$. *)
+  then have "n^2+2-3*n  = (n-1) * (n-2)"
+    unfolding power2_eq_square
+    sledgehammer
+  (* Either $n-1$ or $n-2$ is odd, and the other is even.  
+  Their product must yield an even number.  
+  The only prime that is even is $2$, which is when $n$ is $3$ or $0$. 
+  Since $0$ is not a positive number, the answer is $\\mathrm{(B)}\\ \\text{one}$.*)
+  then have "prime ((n-1) * (n-2))"
+    using prime sledgehammer
+  then have "n-1=1 \\<or> n-2 = 1"
+    using prime_product sledgehammer
+  with \\<open>n>2\\<close>
+  show "n=3" sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+For a positive real number a, show that $10a\\leq 28a^2+1$.
+
+### Solution
+
+It suffices to show $0\\leq 28a^2 - 10a + 1$.
+First, consider completing the square for $28a^2 - 10a$ and observe that $(a - \\frac{5}{28})^2 = a^2 - \\frac{10}{28}a + (5/28)^2$.
+Since $0\\leq (a - \\frac{5}{28})^2$, we have $0\\leq a^2 - \\frac{10}{28}a + (5/28)^2$.
+Multiplying by 28 and simplifying terms gives $0\\leq 28*a^2 - 10*a + (25/28)$.
+Since $25/28 < 1$, the result follows.*)
+
+Formal:
+theorem algebra_binomnegdiscrineq_10alt28asqp1:
+  fixes a :: real
+  shows "10 * a \\<le> 28 * a^2 + 1"
+proof -
+(* it suffices to show $0\\leq 28a^2 - 10a + 1$ *)
+  have c0: "0 \\<le> 28*a^2 - 10*a + 1"
+  proof -
+    (* observe that $(a - \\frac{5}{28})^2 = a^2 - \\frac{10}{28}a + (5/28)^2$ *)
+    have c1: "(a - (5/28))^2 = a^2 - 10/28*a + (5/28)^2"
+      sledgehammer
+    (* we have $0\\leq a^2 - \\frac{10}{28}a + (5/28)^2$ *)
+    then have c2: "0 \\<le> a^2 - 10/28*a + (5/28)^2" using c1
+      sledgehammer
+    (* Multiplying by 28 and simplifying terms gives $0\\leq 28*a^2 - 10*a + (25/28)$ *)
+    then have c3: "0 \\<le> 28*a^2 - 10*a + 28*((5/28)^2)" using c2
+      sledgehammer
+    then have c4: "0 \\<le> 28*a^2 - 10*a + 28*((5/28)*(5/28))" using c3
+      sledgehammer
+    then have c5: "0 \\<le> 28*a^2 - 10*a + (25/28)" using c4
+      sledgehammer
+    (* Since $25/28 < 1$, the result follows. *)
+    then show ?thesis using c5
+      sledgehammer
+  qed
+  then show ?thesis
+    sledgehammer
+qed
+
+
+
+Informal:
+(*### Problem
+
+Show that for any complex number a, $(a-10)(a+11) = a^2 + a - 110$.
+
+### Solution
+
+We first expand all terms of the left hand side to get $a^2 - 10a + 11a - 10*11$.
+This equals $a^2 + a - 10*11 = a^2 + a - 110$.*)
+
+Formal:
+theorem algebra_2rootsintpoly_am10tap11eqasqpam110:
+  fixes a :: complex
+  shows "(a-10) * (a+11) = a^2 + a -110"
+proof -
+  (* We first expand all terms of the left hand side to get $a^2 - 10a + 11a - 10*11$. *)
+  have "(a-10) * (a+11) = a^2 - 10*a + 11*a - 10 *11"
+    sledgehammer
+  (* This equals $a^2 + a - 10*11 = a^2 + a - 110$. *)
+  also have "\\<dots> = a^2 + a - 10 * 11"
+    sledgehammer
+  also have "\\<dots> = a^2 + a - 110"
+    sledgehammer
+  finally show ?thesis
+    sledgehammer
+qed
+
+
+
+""".strip()
+}
+
+class MiniF2FIsabellePrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        if 'numbertheory' in task_input.split("Formal:", 1)[1]:
+            tag = 'numbertheory'
+        else:
+            tag = 'other'
+        prompt = f"{few_shot_prompt[tag].strip()}\n\n\n\nInformal:\n{task_input.strip()}\n{task_output.strip()}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nInformal:"]

evaluation/few_shot_prompts/pal_gsm_8_shot.py

@@ -0,0 +1,155 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = '''
+Q: Olivia has $23. She bought five bagels for $3 each. How much money does she have left?
+
+# solution in Python:
+
+
+def solution():
+    """Olivia has $23. She bought five bagels for $3 each. How much money does she have left?"""
+    money_initial = 23
+    bagels = 5
+    bagel_cost = 3
+    money_spent = bagels * bagel_cost
+    money_left = money_initial - money_spent
+    result = money_left
+    return result
+
+
+
+
+
+Q: Michael had 58 golf balls. On tuesday, he lost 23 golf balls. On wednesday, he lost 2 more. How many golf balls did he have at the end of wednesday?
+
+# solution in Python:
+
+
+def solution():
+    """Michael had 58 golf balls. On tuesday, he lost 23 golf balls. On wednesday, he lost 2 more. How many golf balls did he have at the end of wednesday?"""
+    golf_balls_initial = 58
+    golf_balls_lost_tuesday = 23
+    golf_balls_lost_wednesday = 2
+    golf_balls_left = golf_balls_initial - golf_balls_lost_tuesday - golf_balls_lost_wednesday
+    result = golf_balls_left
+    return result
+
+
+
+
+
+Q: There were nine computers in the server room. Five more computers were installed each day, from monday to thursday. How many computers are now in the server room?
+
+# solution in Python:
+
+
+def solution():
+    """There were nine computers in the server room. Five more computers were installed each day, from monday to thursday. How many computers are now in the server room?"""
+    computers_initial = 9
+    computers_per_day = 5
+    num_days = 4  # 4 days between monday and thursday
+    computers_added = computers_per_day * num_days
+    computers_total = computers_initial + computers_added
+    result = computers_total
+    return result
+
+
+
+
+
+Q: Shawn has five toys. For Christmas, he got two toys each from his mom and dad. How many toys does he have now?
+
+# solution in Python:
+
+
+def solution():
+    """Shawn has five toys. For Christmas, he got two toys each from his mom and dad. How many toys does he have now?"""
+    toys_initial = 5
+    mom_toys = 2
+    dad_toys = 2
+    total_received = mom_toys + dad_toys
+    total_toys = toys_initial + total_received
+    result = total_toys
+    return result
+
+
+
+
+
+Q: Jason had 20 lollipops. He gave Denny some lollipops. Now Jason has 12 lollipops. How many lollipops did Jason give to Denny?
+
+# solution in Python:
+
+
+def solution():
+    """Jason had 20 lollipops. He gave Denny some lollipops. Now Jason has 12 lollipops. How many lollipops did Jason give to Denny?"""
+    jason_lollipops_initial = 20
+    jason_lollipops_after = 12
+    denny_lollipops = jason_lollipops_initial - jason_lollipops_after
+    result = denny_lollipops
+    return result
+
+
+
+
+
+Q: Leah had 32 chocolates and her sister had 42. If they ate 35, how many pieces do they have left in total?
+
+# solution in Python:
+
+
+def solution():
+    """Leah had 32 chocolates and her sister had 42. If they ate 35, how many pieces do they have left in total?"""
+    leah_chocolates = 32
+    sister_chocolates = 42
+    total_chocolates = leah_chocolates + sister_chocolates
+    chocolates_eaten = 35
+    chocolates_left = total_chocolates - chocolates_eaten
+    result = chocolates_left
+    return result
+
+
+
+
+
+Q: If there are 3 cars in the parking lot and 2 more cars arrive, how many cars are in the parking lot?
+
+# solution in Python:
+
+
+def solution():
+    """If there are 3 cars in the parking lot and 2 more cars arrive, how many cars are in the parking lot?"""
+    cars_initial = 3
+    cars_arrived = 2
+    total_cars = cars_initial + cars_arrived
+    result = total_cars
+    return result
+
+
+
+
+
+Q: There are 15 trees in the grove. Grove workers will plant trees in the grove today. After they are done, there will be 21 trees. How many trees did the grove workers plant today?
+
+# solution in Python:
+
+
+def solution():
+    """There are 15 trees in the grove. Grove workers will plant trees in the grove today. After they are done, there will be 21 trees. How many trees did the grove workers plant today?"""
+    trees_initial = 15
+    trees_after = 21
+    trees_added = trees_after - trees_initial
+    result = trees_added
+    return result
+'''.strip()
+
+class PALGSMPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\n\n\n\n\nQ: {task_input}\n\n# solution in Python:"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nQ:", "Q: "]

evaluation/few_shot_prompts/pal_math_4_shot.py

@@ -0,0 +1,114 @@
+from .few_shot_prompting import FewShotPrompting
+
+few_shot_prompt = """Problem:
+Find the value of $x$ that satisfies $\\frac{\\sqrt{3x+5}}{\\sqrt{6x+5}}=\\frac{\\sqrt{5}}{3}$. Express your answer as a common fraction.
+
+You are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.
+```
+# Initialize x
+x = symbols('x')
+
+# Define the equation
+equation = Eq(sqrt(3*x + 5)/sqrt(6*x + 5), sqrt(5)/3)
+
+# Solve for x
+answer = solve(equation, x)
+```
+The imports required for this program are
+```
+from sympy import symbols, Eq, solve, sqrt
+```
+I hope my solution is correct.
+
+Problem:
+If $\\det \\mathbf{A} = 2$ and $\\det \\mathbf{B} = 12,$ then find $\\det (\\mathbf{A} \\mathbf{B}).$
+
+You are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.
+```
+# Given det(A) = 2 and det(B) = 12
+det_A = 2
+det_B = 12
+
+# Use the property det(AB) = det(A)*det(B)
+det_AB = det_A * det_B
+
+answer = det_AB
+```
+The imports required for this program are
+```
+
+```
+I hope my solution is correct. 
+
+Problem:
+Terrell usually lifts two 20-pound weights 12 times. If he uses two 15-pound weights instead, how many times must Terrell lift them in order to lift the same total weight?
+
+You are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.
+```
+# Calculate the total weight lifted initially, which is 2*20*12 pounds
+total_weight = 2 * 20 * 12
+
+# Since Terrell lifts two 15-pound weights, divide the total weight by 2 * 15
+repetitions = total_weight / (2*15)
+
+answer = n_value 
+```
+The imports required for this program are
+```
+
+```
+I hope my solution is correct. 
+
+Problem:
+If Anna flips 8 coins, what is the probability that she gets more heads than tails?
+
+You are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.
+```
+# There are 2**8 possible outcomes
+n = 8
+total_outcomes = 2 ** n
+
+# There are binom(n, k) ways to get k heads
+favorable_outcomes = 0
+for k in range((n // 2) + 1, n + 1):
+    favorable_outcomes += math.comb(n, k)
+    
+probability = favorable_outcomes / total_outcomes
+
+answer = probability
+```
+The imports required for this program are
+```
+import math
+```
+I hope my solution is correct.
+
+Problem:
+Evaluate $\\left\\lceil3\\left(6-\\frac12\\right)\\right\\rceil$.
+
+You are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.
+```
+# Calculate 3 * (6 - 1/2)
+result = 3 * (6 - 0.5)
+
+# Apply the ceiling function
+ceiling_result = math.ceil(result)
+
+answer = ceiling_result
+```
+The imports required for this program are
+```
+import math
+```
+I hope my solution is correct."""
+
+class PALMathPrompt(FewShotPrompting):
+    def __init__(self):
+        super().__init__()
+
+    def format_prompt(self, task_input, task_output):
+        prompt = f"{few_shot_prompt}\n\nProblem:\n{task_input}\n\nYou are an expert programmer. Solve the above mathematical problem by writing a Python program. Express your answer as a numeric type or a SymPy object.\n{task_output}"
+        return prompt.rstrip()
+
+    def stop_words(self):
+        return ["\nProblem:", "Problem:"]