all_code.py

import json

# from mariana.repl.pass_rate_new import main

def handle():

    data = json.load(open('pass_rate_results/lean4_basic_test/lean4_random_15k_all.jsonl'))
    # data['results'] += json.load(open('pass_rate_results/gsm8k_train/lean4_random_15k_all.jsonl'))['results']


    PROMPT_DICT = {
        "wild": (
            "# Problem:\n{question}\n\n"
            "# Proof:\n{answer}."
        ),
        "lean4": (
            "Statement and proof in natural language:\n\n"
            "{statement_text}\n\n"
            "Translate the statement and proof in natural language to lean4:"
        ),
        "prompt_no_input": (
        "Below is an instruction that describes a task. "
        "Write a response that appropriately completes the request.\n\n"
        "### Instruction:\n{instruction}\n\n### Response:"
        ),
    }
    training_data  = []
    ratio = []
    for item in data['results']:
        if item['status'] == 'pass':
            if  not len(item['stderr']):
                ratio.append(1)
                # training_data.append(
                #     {
                #         "statement_poof":item['statement'],
                #         "model_response":PROMPT_DICT["wild"].format(question= item['content']['question'], answer = item['content']['answer']),
                #         "task": "statementproof_inform",
                #     }
                # )
            else:
                ratio.append(0)
                print ( item['stderr'])


    # with open("pass_rate_results/combined_lean4_random_15k_all_passed.jsonl", "w") as f:
    #     json.dump(training_data, f, ensure_ascii=False, indent=2)


    print("false positives: ", 1 - sum(ratio)/len(ratio))


def savetojson():

    import_statements = '''import algebra.algebra.basic
import algebra.order.floor
import algebra.associated
import algebra.big_operators.basic
import algebra.big_operators.enat
import algebra.big_operators.order
import algebra.big_operators.pi
import algebra.geom_sum
import algebra.group.pi
import algebra.group.commute
import algebra.group_power.basic
import algebra.group_power.identities
import algebra.order.floor
import algebra.quadratic_discriminant
import algebra.ring.basic
import analysis.asymptotics.asymptotic_equivalent
import analysis.mean_inequalities
import analysis.normed_space.basic
import analysis.inner_product_space.basic
import analysis.inner_product_space.euclidean_dist
import analysis.normed_space.pi_Lp
import analysis.special_functions.exp
import analysis.special_functions.exp_deriv
import analysis.special_functions.log
import analysis.special_functions.logb
import analysis.special_functions.log_deriv
import analysis.special_functions.pow
import analysis.special_functions.sqrt
import analysis.special_functions.trigonometric.basic
import analysis.special_functions.trigonometric.complex
import combinatorics.simple_graph.basic
import data.complex.basic
import data.complex.exponential
import data.finset.basic
import data.fintype.card
import data.int.basic
import data.int.gcd
import data.int.modeq
import data.int.parity
import data.list.intervals
import data.list.palindrome
import data.multiset.basic
import data.nat.basic
import data.nat.choose.basic
import data.nat.digits
import data.nat.factorial.basic
import data.nat.fib
import data.nat.modeq
import data.nat.multiplicity
import data.nat.parity
import data.nat.prime
import data.pnat.basic
import data.pnat.prime
import data.polynomial
import data.polynomial.basic
import data.polynomial.eval
import data.rat.basic
import data.real.basic
import data.real.ennreal
import data.real.irrational
import data.real.nnreal
import data.real.sqrt
import data.real.golden_ratio
import data.set.finite
import data.sym.sym2
import data.zmod.basic
import dynamics.fixed_points.basic
import field_theory.finite.basic
import geometry.euclidean.basic
import geometry.euclidean.circumcenter
import geometry.euclidean.monge_point
import geometry.euclidean.sphere
import init.data.nat.gcd
import linear_algebra.affine_space.affine_map
import linear_algebra.affine_space.independent
import linear_algebra.affine_space.ordered
import linear_algebra.finite_dimensional
import logic.equiv.basic
import measure_theory.integral.interval_integral
import number_theory.arithmetic_function
import number_theory.legendre_symbol.quadratic_reciprocity
import number_theory.primes_congruent_one
import order.bounds
import order.filter.basic
import order.well_founded
import topology.basic
import topology.instances.nnreal
'''

    data = {
        "working_file": import_statements
    }

    with open('data/notlean_dependency.json', 'w', encoding='utf-8') as f:
        json.dump(data, f, indent=4)
    

def load_to_atp():
    data_path = 'pass_rate_results/math_train/1/10pass10.jsonl'
    data = json.load(open(data_path, "r", encoding='utf-8'))
    import pdb
    pdb.set_trace()
if __name__ == '__main__':
    load_to_atp()
    # get_novel_premises()
    # savetojson()