-
Notifications
You must be signed in to change notification settings - Fork 2
/
prompts.py
41 lines (30 loc) · 8.25 KB
/
prompts.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
system_message = "You are a logician with background in mathematics that translates natural language reasoning text to Lean code so that these natural language reasoning problems can be solved. During the translation, please keep close attention to the predicates and entities. There is an additional requirement: I also want you to try to prove the theorem you translated to Lean. If you can prove the theorem, give me True at the end of the answer. If you can prove the negation of the theorem, write False at the end of the answer. If you can neither prove whether the original theorem or the negation of the theorem, please give me Unknown at the end of the answer."
ProofWriter_example_true_textual_input = "Textual context: Charlie is cold. Charlie is smart. Dave is smart. Fiona is green. Fiona is smart. Fiona is young. Harry is red. If Charlie is round and Charlie is big then Charlie is smart. If something is smart and not red then it is round. All red, young things are round. Big things are young. Red things are big. If something is red then it is smart. All round, red things are cold. All round, green things are cold. If something is red and cold then it is green.\nQuestion: Based on the above information, is the following statement true, false, or unknown? Harry is green."
ProofWriter_example_false_textual_input = "Textual context: The cat is blue. The cat is nice. The cat likes the cow. The cat needs the cow. The cat needs the rabbit. The cow does not need the rabbit. The cow needs the tiger. The rabbit is round. The tiger is nice. The tiger does not like the cow. If someone likes the cat and they chase the cat then they are blue. If someone likes the cow and they are red then the cow is round. If someone needs the tiger and they need the cat then they do not chase the cow. If someone needs the cat and the cat is blue then the cat is red. If someone is round then they need the cat. If someone likes the cat and the cat needs the rabbit then the cat chases the tiger. If the rabbit needs the tiger then the rabbit is not round.\nQuestion: Based on the above information, is the following statement true, false, or unknown? The cow chases the cow."
ProofWriter_example_unknown_textual_input = "Textual context: Anne is furry. Anne is round. Anne is smart. Anne is white. Erin is furry. Erin is kind. Erin is round. Gary is cold. Harry is cold. Harry is kind. Harry is rough. Harry is white. Round, cold things are white. If Gary is cold then Gary is kind. If something is kind and cold then it is white. Rough things are smart. If something is kind and white then it is rough. If Gary is rough and Gary is white then Gary is round. Kind, smart things are furry. Rough things are kind.\nQuestion: Based on the above information, is the following statement true, false, or unknown? Anne is not kind."
ProofWriter_example_true_all_output = "".join(open("output_prompt/output_true.lean").readlines())
ProofWriter_example_false_all_output = "".join(open("output_prompt/output_false.lean").readlines())
ProofWriter_example_unknown_all_output = "".join(open("output_prompt/output_unknown.lean").readlines())
ProofWriter_example_true_all_COT_output = "".join(open("output_prompt/output_true_COT.lean").readlines())
ProofWriter_example_false_all_COT_output = "".join(open("output_prompt/output_false_COT.lean").readlines())
ProofWriter_example_unknown_all_COT_output = "".join(open("output_prompt/output_unknown_COT.lean").readlines())
ProofWriter_example_true_all_COT_comment_output = "".join(open("output_prompt/output_true_COT_comment.lean").readlines())
ProofWriter_example_false_all_COT_comment_output = "".join(open("output_prompt/output_false_COT_comment.lean").readlines())
ProofWriter_example_unknown_all_COT_comment_output = "".join(open("output_prompt/output_unknown_COT_comment.lean").readlines())
ProofWriter_example_true_formalization = "".join(open("output_prompt/output_true_formalization.lean").readlines())
ProofWriter_example_false_formalization = "".join(open("output_prompt/output_false_formalization.lean").readlines())
ProofWriter_example_unknown_formalization = "".join(open("output_prompt/output_unknown_formalization.lean").readlines())
ProofWriter_example_true_proof = "".join(open("output_prompt/output_true_proof.lean").readlines())
ProofWriter_example_false_proof = "".join(open("output_prompt/output_false_proof.lean").readlines())
ProofWriter_example_unknown_proof = "".join(open("output_prompt/output_unknown_proof.lean").readlines())
ProofWriter_example_true_proof_COT = "".join(open("output_prompt/output_true_proof_COT.lean").readlines())
ProofWriter_example_false_proof_COT = "".join(open("output_prompt/output_false_proof_COT.lean").readlines())
ProofWriter_example_unknown_proof_COT = "".join(open("output_prompt/output_unknown_proof_COT.lean").readlines())
FOLIO_example_textual_input_1 = "Textual context: All people who regularly drink coffee are dependent on caffeine. People either regularly drink coffee or joke about being addicted to caffeine. No one who jokes about being addicted to caffeine is unaware that caffeine is a drug. Rina is either a student and unaware that caffeine is a drug, or neither a student nor unaware that caffeine is a drug. If Rina is not a person dependent on caffeine and a student, then Rina is either a person dependent on caffeine and a student, or neither a person dependent on caffeine nor a student.\nQuestion 1: Based on the above information, is the following statement true, false, or uncertain? Rina is a person who jokes about being addicted to caffeine or unaware that caffeine is a drug.\nQuestion 2: Based on the above information, is the following statement true, false, or uncertain? Rina is either a person who jokes about being addicted to caffeine or is unaware that caffeine is a drug.\nQuestion 3: Based on the above information, is the following statement true, false, or uncertain? Rina is either a person who regularly drinks coffee or a person who is unaware that caffeine is a drug.\nQuestion 4: Based on the above information, is the following statement true, false, or uncertain? If Rina is either a person who jokes about being addicted to caffeine and a person who is unaware that caffeine is a drug, or neither a person who jokes about being addicted to caffeine nor a person who is unaware that caffeine is a drug, then Rina jokes about being addicted to caffeine and regularly drinks coffee."
FOLIO_example_textual_input_2 = "Textual context: There are six types of wild turkeys: Eastern wild turkey, Osceola wild turkey, Gould’s wild turkey, Merriam’s wild turkey, Rio Grande wild turkey, and Ocellated wild turkey. Tom is not an Eastern wild turkey. Tom is not an Osceola wild turkey. Tom is also not a Gould's wild turkey, or a Merriam's wild turkey, or a Rio Grande wild turkey. Tom is a wild turkey.\nQuestion 1: Based on the above information, is the following statement true, false, or uncertain? Tom is an Ocellated wild turkey.\nQuestion 2: Based on the above information, is the following statement true, false, or uncertain? Tom is an Eastern wild turkey.\nQuestion 3: Based on the above information, is the following statement true, false, or uncertain? Joey is a wild turkey."
FOLIO_example_textual_input_3 = "Textual context: A La Liga soccer team ranks higher than another if it receives more points. If two La Liga soccer teams recieve the same points, the team which recieves more points from the games between the two teams ranks higher. Real Madrid and Barcelona are both La Liga soccer teams. In La Liga 2021-2022, Real Madrid recieves 86 points and Barcelon recieves 73 points. In La Liga 2021-2022, Real Madrid and Barcelona both recieve 3 points from the games between them.\nQuestion 1: Based on the above information, is the following statement true, false, or uncertain? In La Liga 2021-2022, Real Madrid ranks higher than Barcelona.\nQuestion 2: Based on the above information, is the following statement true, false, or uncertain? In La Liga 2021-2022, Barcelona ranks higher than Real Madrid."
import os
if os.path.exists("output_prompt_FOLIO"):
FOLIO_example_outputs_True = "".join(open("output_prompt_FOLIO/FOLIO_train_multi_1.lean").readlines())
FOLIO_example_outputs_False = "".join(open("output_prompt_FOLIO/FOLIO_train_multi_2.lean").readlines())
FOLIO_example_outputs_Unknown = "".join(open("output_prompt_FOLIO/FOLIO_train_multi_3.lean").readlines())