{"id":"W1537398137","doi":"10.4230/lipics.rta.2011.21","title":"Automated Certified Proofs with CiME3","year":2011,"lang":"en","type":"preprint","venue":"DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":29,"is_retracted":false,"has_abstract":true,"ca_institutions":"Prevention of Organ Failure","funders":"Agence Nationale de la Recherche","keywords":"Mathematical proof; Proof assistant; Rewriting; Computer science; Programming language; Certification; Scripting language; Automated theorem proving; Automation; Confluence; Mathematics; Engineering","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.005313697,0.0008169292,0.0007765109,0.001517134,0.0007812213,0.003485115,0.002727162,0.001438107,0.02421631],"category_scores_gemma":[0.01908994,0.0012043,0.002031514,0.001095401,0.002112341,0.003866698,0.005336081,0.002929606,0.007660095],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001376186,"about_ca_system_score_gemma":0.001549041,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001517231,"about_ca_topic_score_gemma":0.001696702,"domain_scores_codex":[0.9935607,0.001913012,0.000449851,0.0009662848,0.002640058,0.0004700789],"domain_scores_gemma":[0.9899213,0.003961971,0.0004267832,0.004636737,0.0008639101,0.0001892725],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0004884056,0.0001931375,0.001310613,0.001176363,0.0001966536,0.0010281,0.000929443,0.03188504,0.0233413,0.6444481,0.05845065,0.2365523],"study_design_scores_gemma":[0.0003426741,0.000092802,0.0004610579,0.0002351957,0.00009446501,0.001271062,0.00007809043,0.1713306,0.06538238,0.2623306,0.4982189,0.0001621181],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.003529185,0.0003520632,0.9307411,0.0005841316,0.00020381,0.0001676886,0.0008073979,0.0480587,0.01555598],"genre_scores_gemma":[0.1367275,0.0005264686,0.8367413,0.0005966524,0.0001880125,0.0004371047,0.002595441,0.00824276,0.01394476],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02421631,"threshold_uncertainty_score":0.08101159,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0355182454461572,"score_gpt":0.2575704401851536,"score_spread":0.2220521947389964,"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."}}