{"id":"W7015220610","doi":"","title":"Semi-Automation of Meta-Theoretic Proofs","year":2023,"lang":"en","type":"dissertation","venue":"eScholarship@McGill (McGill)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; Natural deduction; Sequent calculus; Gas meter prover; Soundness; Calculus (dental); Automated theorem proving; Automated proof checking; Curry–Howard correspondence","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":["metaepi_narrow","insufficient_payload"],"consensus_categories":[],"category_scores_codex":[0.002023917,0.0007727084,0.001281456,0.0006353029,0.0005758214,0.0002135079,0.002042232,0.0008047373,0.00009953688],"category_scores_gemma":[0.0006789758,0.0006832752,0.0008050155,0.001450445,0.00007325163,0.0009501778,0.0002759939,0.0008758146,0.001046032],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002681639,"about_ca_system_score_gemma":0.00008639398,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002289865,"about_ca_topic_score_gemma":0.0003652988,"domain_scores_codex":[0.9947112,0.0005844115,0.001322635,0.001314824,0.001323502,0.0007434118],"domain_scores_gemma":[0.9959121,0.0003216549,0.001312647,0.00152719,0.0006757405,0.0002506498],"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.00001924999,0.0001194148,0.000006959954,0.0009030748,0.0008013762,0.00004159814,0.0000510545,0.00003458908,0.002928016,0.9184898,0.00001524502,0.07658959],"study_design_scores_gemma":[0.001074945,0.0005889215,0.0007171006,0.0002392806,0.001995778,0.00006439701,0.0003572993,0.001323446,0.1209235,0.827666,0.04279209,0.002257261],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.5125755,0.004082771,0.0008764014,0.0001151152,0.02091997,0.008530312,0.0005803934,0.00800625,0.4443133],"genre_scores_gemma":[0.9794918,0.00009065714,0.001464766,0.00005279975,0.00005705149,0.0004282649,0.0004346,0.0001414193,0.01783863],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.4669163,"threshold_uncertainty_score":0.9997318,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02973873265478744,"score_gpt":0.2580544613430447,"score_spread":0.2283157286882573,"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."}}