{"id":"W4388723135","doi":"10.4204/eptcs.396.3","title":"Semi-Automation of Meta-Theoretic Proofs in Beluga","year":2023,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Calculus (dental); Computer science; Natural deduction; Simple (philosophy); Gas meter prover; Beluga; Normalization (sociology); Programming language; Automated theorem proving; Theoretical computer science; Mathematics; Algebra over a field; Pure mathematics; Epistemology; Medicine; Philosophy; Ecology","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.009806256,0.0006186586,0.0008634828,0.001824299,0.001766433,0.003864483,0.002775831,0.0008950325,0.004473614],"category_scores_gemma":[0.01984301,0.001565813,0.002096753,0.000935217,0.00501162,0.00699146,0.007506093,0.003337989,0.00136161],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002061984,"about_ca_system_score_gemma":0.003121269,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006437236,"about_ca_topic_score_gemma":0.008977514,"domain_scores_codex":[0.9903513,0.003997131,0.0004784565,0.001117981,0.003077113,0.0009780448],"domain_scores_gemma":[0.9850734,0.009813821,0.000599789,0.002396923,0.001593366,0.0005227024],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0002869988,0.0001326281,0.001190502,0.0005102458,0.00008862634,0.0006654707,0.005595415,0.01448291,0.01824586,0.8602914,0.003294456,0.0952154],"study_design_scores_gemma":[0.0002194904,0.0002301142,0.000981089,0.0002766171,0.0001712394,0.0007951991,0.000589369,0.1404846,0.04797656,0.7336174,0.07446382,0.0001944201],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.02021678,0.0003519427,0.9655021,0.0003730225,0.00006021846,0.00009275212,0.00007323553,0.005114675,0.008215227],"genre_scores_gemma":[0.4416082,0.000370522,0.5515426,0.0004918401,0.00008293258,0.0001568567,0.0002154911,0.000785839,0.004745697],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.009806256,"threshold_uncertainty_score":0.05186111,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01369331765022819,"score_gpt":0.2534848166654141,"score_spread":0.2397914990151859,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}