| 7 | from evaluate_results import monte_carlo_evaluate |
| 8 | |
| 9 | def parse_args(): |
| 10 | parser = argparse.ArgumentParser(description="Pipeline for Lean theorem proof (generation, verification, and evaluation)") |
| 11 | |
| 12 | # File paths |
| 13 | parser.add_argument("--input_file", default=None, |
| 14 | help="Path to the initial input file") |
| 15 | parser.add_argument("--generated_file", default=None, |
| 16 | help="Path to the output file containing generated answers") |
| 17 | parser.add_argument("--verification_file", default=None, |
| 18 | help="Path to the output file containing verification results") |
| 19 | parser.add_argument("--evaluation_file", default=None, |
| 20 | help="Path to the output file containing evaluation results") |
| 21 | |
| 22 | # Task control |
| 23 | parser.add_argument("--auto_dl", action="store_true", default=True, |
| 24 | help="Automatically download dataset") |
| 25 | parser.add_argument("--generate", action="store_true", default=False, |
| 26 | help="Enable generation of answers") |
| 27 | parser.add_argument("--verify", action="store_true", default=False, |
| 28 | help="Enable verification of generated answers") |
| 29 | parser.add_argument("--evaluate", action="store_true", default=False, |
| 30 | help="Enable evaluation of verification results") |
| 31 | parser.add_argument("--datasets", default="FomaMATH-All", |
| 32 | help="Choose dataset version: FomaMATH-All or FomaMATH-Lite") |
| 33 | |
| 34 | # Generation parameters - Add all parameters from the first script |
| 35 | parser.add_argument("--model", default=None, |
| 36 | help="Path to the model used for generating answers.") |
| 37 | parser.add_argument("--n", type=int, default=200, |
| 38 | help="Number of answers to generate per process via vllm.") |
| 39 | parser.add_argument("--nums_answer", type=int, default=3200, |
| 40 | help="Number of answers to generate per question.") |
| 41 | |
| 42 | # Verification parameters |
| 43 | parser.add_argument("--repl_path", default="./repl", |
| 44 | help="Path to the Lean REPL used for verification") |
| 45 | parser.add_argument("--lean_env_path", default="./repl/test/Mathlib", |
| 46 | help="Path to the Lean environment used for verification") |
| 47 | parser.add_argument("--num_batches", default=32, type=int, |
| 48 | help="Number of parallel batches for verification") |
| 49 | parser.add_argument("--session_timeout", default=600, type=int, |
| 50 | help="Timeout for interactive sessions in seconds") |
| 51 | parser.add_argument("--expect_timeout", default=120, type=int, |
| 52 | help="Timeout for the expect command in seconds") |
| 53 | |
| 54 | # Evaluation parameters |
| 55 | parser.add_argument("--n_simulations", default=50, type=int, |
| 56 | help="Number of Monte Carlo simulations") |
| 57 | parser.add_argument("--n_processes", default=50, type=int, |
| 58 | help="Number of parallel processes for Monte Carlo simulation") |
| 59 | parser.add_argument("--custom_sample_sizes", default=None, type=str, |
| 60 | help="Custom sampling sizes as a comma-separated list (e.g., '1,5,10,50,100')") |
| 61 | |
| 62 | return parser.parse_args() |
| 63 | def set_up_logging(level=logging.INFO): |
| 64 | """Set up logging with the specified level.""" |
| 65 | logging.basicConfig(level=level, format='%(asctime)s - %(levelname)s - %(message)s') |