Kasus jaminan

Kasus jaminan adalah argumen tim Anda bahwa sistem cukup baik untuk penggunaan yang dinyatakan: setiap klaim, penggunaannya, dan bukti yang menjadi dasarnya. Kasus ini berada di samping kebijakan rilis dalam assurance.yaml, sehingga ditinjau dalam pull request, dan Oloproof membaca setiap klaim terhadap bukti yang dimilikinya. Oloproof tidak pernah menyatakan sebuah klaim terbukti: ia menyebut klaim mana yang bertumpu pada bukti terkini yang lolos, mana yang pada bukti yang gagal, usang, atau tidak ada, dan mana yang hanya pada asumsi.

Menulis kasus

version: 1
goals:
  - id: G1
    statement: The assistant routes tickets well enough for first-line support
    scope: first-line support tickets in English
    strategy: argue over label accuracy and the misrouting hazard
    reassess_when: [the model changes, a new language is supported]
    goals:
      - id: G1.1
        statement: Labels are accurate
        evidence:
          - rule: label-floor
      - id: G1.2
        statement: Misrouting stays rare
        evidence:
          - hazard: missed-label
          - record: records/release-42.json
        defeaters:
          - id: D1
            statement: Tickets in other languages misroute
            resolved_by:
              - rule: label-floor
                suite: multilingual
      - id: G1.3
        statement: The deployment runs the model that was evaluated
        assumptions: [the model is pinned by digest in the deployment manifest]

Sebuah tujuan adalah klaim. Tujuan tingkat atas menyatakan scope-nya, yaitu penggunaan yang dimaksud untuk klaim tersebut; sub-tujuan mewarisinya. strategy menjelaskan dengan kata-kata bagaimana sub-tujuan mendukung argumen tujuannya. Setiap bagian evidence menyebut tepat satu dari:

• rule: sebuah aturan dari release.yaml, dibaca pada run terakhir setiap sistem di setiap suite; system dan suite mempersempit run mana yang dihitung;
• hazard: sebuah bahaya dari hazards.yaml (Daftar bahaya);
• proof: sebuah properti formal, dibaca sebagaimana aturan bukti membacanya (Bukti formal): hasil terakhir yang diterima untuk properti itu, dengan DISPROVED untuk model yang sama yang menang; model (sebuah digest) mempersempitnya ke satu model yang diformalkan; selama proyek belum memiliki hasil, tautan ini tidak mendukung apa pun;
• record: berkas rekaman keputusan yang ditulis oleh oloproof record export, relatif terhadap root proyek.

assumptions adalah hal yang dianggap benar oleh tujuan. defeater adalah alasan tujuan itu mungkin salah; ia tetap terbuka sampai setiap bagian bukti dalam resolved_by-nya memberi dukungan. reassess_when menyebut apa yang semestinya membawa tim kembali ke tujuan itu.

Memeriksanya

oloproof assurance check

Pemeriksaan menolak kasus yang menyebut aturan yang tidak ada di kebijakan atau bahaya yang tidak ada di daftar, atau yang tujuan tingkat atasnya tidak menyatakan cakupan, dan keluar dengan 2. Jika tidak, pemeriksaan mencetak pohonnya, setiap tujuan dengan salah satu dari empat status:

• supported: setiap bagian buktinya dan setiap sub-tujuan mendukungnya, berdasarkan bukti terkini, dan tidak ada sanggahan yang terbuka;
• undermined: sebagian bukti gagal, usang, atau dibantah, sebuah sub-tujuan dilemahkan, atau ada sanggahan yang terbuka;
• assumptions_only: tidak ada yang mendukungnya, dan ia bertumpu pada asumsi yang dinyatakan;
• unsupported: selain itu semua, dengan setiap celah disebutkan. Tujuan yang punya sebagian dukungan dan sebuah celah tetap tidak didukung: sebuah klaim hanya sekuat hal terlemah yang menjadi dasarnya.

Sebuah aturan mendukung tujuan ketika setiap run terakhir yang memutuskannya menyatakan PASS, dan melemahkannya ketika salah satunya menyatakan FAIL; INSUFFICIENT_EVIDENCE dan MANUAL_REVIEW tidak mendukung apa pun. Sebuah bahaya mendukung ketika setiap aturan yang mengukurnya lolos. Hasil formal mendukung ketika properti itu PROVED, dan melemahkan ketika DISPROVED atau ketika dua hasil untuk satu model saling bertentangan; sebuah hasil menyatakan apa yang dibuktikannya tentang model yang diformalkan, tidak pernah tentang deployment. Sebuah rekaman mendukung ketika digest isinya masih sama dengan id-nya dan keputusannya PASS. Bukti dari run yang tidak lagi cocok dengan proyek (sistem, suite, evaluator, atau kebijakannya berubah) dianggap usang dan melemahkan. Status-status ini milik kasus, bukan keputusan, dan tidak pernah mengubah kode keluar. --json menulis laporan yang sama untuk pipeline.

Di mana ia tampil

oloproof run mencatat kasus bersama run, oloproof push membawa kasus run itu ke ruang kerja Anda beserta hasil formal yang disebut tautan buktinya, dan oloproof export menulis pembacaan mesin atas kasus itu di samping bundle. Halaman Safety and risk menampilkan pohonnya dengan setiap status seperti yang ditulis mesin, setiap aturan tertaut ke buktinya. Di ruang kerja, kasus dibaca terhadap run yang Anda push: kesegaran tidak dibandingkan di sana, karena tidak ada berkas proyek sebagai pembanding, dan tautan rekaman hanya dibaca oleh oloproof assurance check. Rekaman keputusan menyebut kasus yang dicatat run-nya; record verify melaporkannya sebagai pernyataan tim.

Langkah selanjutnya

• Daftar bahaya membahas bahaya yang dapat menjadi dasar sebuah tujuan.
• Graf bukti menggambar setiap klaim beserta bukti yang mendasarinya.