{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.005516859,0.0002474941,0.0004842584,0.0008815177,0.0001280281,0.0002572228,0.002469735,0.0001049399,0.00001531763],"category_scores_gemma":[0.000265188,0.0001956867,0.0001123883,0.006271531,0.001236163,0.0008908163,0.0007593668,0.0003915242,0.00004953257],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002393693,"about_ca_system_score_gemma":0.0002588467,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000008310487,"about_ca_topic_score_gemma":0.000004121302,"domain_scores_codex":[0.9962673,0.0000634495,0.0006237505,0.0009086739,0.0008925719,0.001244273],"domain_scores_gemma":[0.9989185,0.0001749986,0.0001888751,0.000374868,0.0002188818,0.0001238235],"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.000005640428,0.00006441928,0.0005743647,0.00005447757,0.00001312095,0.000005624692,0.001159024,0.0001096059,0.000540444,0.9912146,0.00002092864,0.006237726],"study_design_scores_gemma":[0.0002396374,0.0002756431,0.0008950559,0.00001484841,0.00001098842,0.00002311825,0.00001970125,0.3408158,0.005766267,0.6516759,0.00007684208,0.0001862888],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.2018297,0.0003713351,0.7850718,0.001354642,0.0005302494,0.001185306,4.319271e-7,0.0007286714,0.008927787],"genre_scores_gemma":[0.9956986,0.00002166974,0.004030626,0.00007353144,0.00004906815,0.00009261684,6.842028e-7,0.00001121554,0.00002202574],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.7938688,"threshold_uncertainty_score":0.7979874,"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."}}