Formal Methods Techniques in AI Verification

Formal methods are mathematical techniques used to rigorously verify the correctness, safety, and robustness of AI systems, particularly in high-stakes applications such as autonomous vehicles, medical diagnostics, and aerospace. 

When I did my master's degree 10 years ago, I discussed, evaluated, and qualitatively reviewed some of these techniques within the formal methods. You may search my thesis title "A source code perspective C overflow vulnerabilities exploit taxonomy based on well-defined criteria"

Below is a brief explanation of key techniques within formal methods, along with relevant examples and mathematical formulations simplified to ease the understanding.

---

1. Abstract Interpretation

Definition:
Abstract interpretation is a static program analysis technique that approximates program behavior by mapping infinite concrete domains (e.g., real numbers) to a finite abstract domain (e.g., intervals). This technique is used to detect errors such as buffer overflows, division by zero, and numeric instability.

Example:
Consider an AI algorithm using floating-point arithmetic. Instead of testing all possible floating-point values, abstract interpretation groups them into intervals. If a neural network's activation function outputs values in $[-1,1]$, the abstract interpretation would ensure no computations exceed this range.

Mathematical Representation:
For a program function $f(x)$, abstract interpretation defines an abstraction function $\alpha$ and a concretization function $\gamma$:

$$\forall x \in \text{ConcreteDomain}, \quad \alpha(f(x)) \approx f(\alpha(x))$$

where $\alpha(x)$ is the abstract representation, and $\gamma(\alpha(x))$ maps it back to the concrete domain.

---

2. Semantic Static Analysis

Definition:
Semantic static analysis inspects a program's source code without executing it to determine properties such as termination, correctness, and possible runtime errors.

Example:
A neural network classifier trained for medical diagnosis should not output probabilities exceeding $1$. Static analysis verifies whether the probability function adheres to:

$$\sum P(y|x) = 1, \quad \forall x \in \text{InputDomain}$$

where $P(y|x)$ represents the probability of class $y$ given input $x$.

---

3. Model Checking

Definition:
Model checking systematically explores a system's state space to ensure it satisfies a given set of formal specifications, typically expressed in temporal logic.

Example:
In an autonomous driving system, a model checker can verify whether a car always stops at a red light by checking the Linear Temporal Logic (LTL) formula:

$$\Box (\text{RedLight} \rightarrow \Diamond \text{Stop})$$

which states that if a red light appears, the car must eventually stop.

---

4. Proof Assistants

Definition:
Proof assistants are software tools that help construct formal proofs of system correctness by allowing users to define mathematical models and verify logical statements interactively.

Example:
A self-driving car’s braking system should ensure that stopping distance does not exceed a threshold $d_{\text{safe}}$:

$$d_{\text{stop}}=\frac{v^2}{2a}\le d_{\text{safe}}$$

where $v$ is the vehicle speed and $a$ is the braking deceleration. A proof assistant like Coq or Isabelle verifies this inequality.

---

5. Deductive Verification

Definition:
Deductive verification formally proves that a system satisfies its specification using logical reasoning. This involves deriving proof obligations that demonstrate correctness.

Example:
In an AI-based medical diagnosis system, a deductive verification approach ensures that if input $x$ is classified as disease-positive, then the treatment $T(x)$ should always be prescribed:

$$\forall x, \quad \text{Diagnosis}(x) = \text{Positive} \Rightarrow T(x) \neq \emptyset$$

---

6. Model-Based Testing

Definition:
Model-based testing (MBT) derives test cases from formal models of a system’s expected behavior, ensuring comprehensive test coverage.

Example:
For an AI-powered ATM system, a state machine model might specify:

1. Insert Card → PIN Entry → Transaction → Dispense Cash
2. Insert Card → PIN Entry → Incorrect PIN → Card Ejection

Each path is converted into test cases, ensuring all scenarios are tested.

---

7. Design by Refinement

Definition:
Design by refinement incrementally develops a system by starting with an abstract specification and progressively introducing more details while maintaining correctness.

Example:
For a neural network-based control system, an initial specification may state:

$$\text{Output}\in [0,1]$$

As the design is refined, more constraints are added to ensure robustness against adversarial attacks.

---

Conclusion

These formal methods provide robust frameworks for ensuring AI systems behave as expected in critical applications. While abstract interpretation and static analysis focus on pre-runtime validation, model checking, and proof assistants help verify properties at runtime. Deductive verification ensures correctness by logical reasoning, while model-based testing and refinement guide structured system development.

Read More

Ensuring Robustness in AI Systems: A Multi-Phase Validation Approach

Abstract

Artificial Intelligence (AI) systems are increasingly integral across various sectors, necessitating rigorous validation to ensure they function as intended with minimal errors. This article delineates a comprehensive, multi-phase validation framework designed to enhance the reliability and accuracy of AI systems. Organizations can mitigate risks associated with AI deployment by implementing structured validation processes, thereby fostering trust and efficacy in AI applications.

Introduction

The proliferation of AI technologies has transformed industries by automating complex tasks and providing data-driven insights. However, the deployment of AI systems without thorough validation can lead to significant errors, undermining their intended purposes and potentially causing adverse outcomes. Therefore, establishing a robust validation framework is imperative to ensure AI systems operate with high accuracy and reliability.

Phases of AI System Validation

1. Data Validation
2. Model Training and Validation
3. Pre-Deployment Validation
4. Post-Deployment Monitoring and Validation

Reducing Error Rates in AI Systems

Achieving low error rates in AI systems is paramount, especially in critical applications. Studies indicate that acceptable error rates for AI should be significantly lower than those for human performance to foster trust and reliability. For instance, in medical diagnostics, a survey revealed that the acceptable error rate for AI was 6.8%, compared to 11.3% for human practitioners.

To minimize errors, organizations should implement high-quality data collection, robust validation processes, and advanced algorithms tailored to specific use cases.

Conclusion

Implementing a multi-phase validation framework is essential to ensure AI systems serve their intended purposes with minimal errors. By meticulously validating data, rigorously training and testing models, and continuously monitoring performance post-deployment, organizations can enhance the reliability and effectiveness of AI applications. Such structured validation not only mitigates risks but also builds stakeholder confidence in AI technologies.

References

1. The 5 Stages of Machine Learning Validation (https://towardsdatascience.com/the-5-stages-of-machine-learning-validation-162193f8e5db)
2. Goodbye Noise, Hello Signal: Data Validation Methods That Work (https://www.pecan.ai/blog/data-validation-methods-that-work/?utm_source=chatgpt.com)
3. Training, validation, and test phases in AI — explained in a way you'll never forget (https://towardsdatascience.com/training-validation-and-test-phases-in-ai-explained-in-a-way-youll-never-forget-744be50154e8)
4. Verification and Validation of Systems in Which AI is a Key Element (https://sebokwiki.org/wiki/Verification_and_Validation_of_Systems_in_Which_AI_is_a_Key_Element?utm_source=chatgpt.com)
5. Should artificial intelligence have lower acceptable error rates than humans? (https://pmc.ncbi.nlm.nih.gov/articles/PMC10301708/?utm_source=chatgpt.com)
6. Understanding Error Rate: A Crucial Guide for Professionals (https://helio.app/ux-research/design-metrics/understanding-error-rate-a-crucial-guide-for-professionals/?utm_source=chatgpt.com)

Read More

AI Audit and the Importance of Having Competent Auditor

"However, efforts to meet AI audit service demands, and by extension, any use of audits by public regulators, face three important challenges. First, it remains unclear what the audit object(s) will be – the exact thing that gets audited. Second, despite efforts to build training and credentialing for AI auditors, a sufficient supply of capable AI auditors is lagging. And third, unless markets have clear regulations around auditing, AI audits could suffer from a race to the bottom in audit quality." -

https://www.techpolicy.press/ai-audit-objects-credentialing-and-the-racetothebottom-three-ai-auditing-challenges-and-a-path-forward/?utm_source=chatgpt.com

---

As AI systems become increasingly prevalent, the need for rigorous auditing to ensure their safety and efficacy has never been greater. An article on TechPolicy Press highlights the critical role of AI auditing in ensuring the safety and effectiveness of AI systems. While I agree that increasing the number of AI auditors is essential, I want to emphasize the equally critical need to ensure their competence and experience.

We can't afford to take a lax approach where anyone who passes a certification exam is deemed qualified to audit AI systems. In-depth knowledge and practical experience are paramount. This concern is particularly relevant when considering the practices of some companies that prioritize hiring "bright young talent" with strong communication skills but lack real-world understanding of AI systems to manage their operational cost. These auditors often provide vague or irrelevant recommendations, or misunderstand the situation entirely, leading to wasted time and potentially jeopardizing safety.

Just like any complex system, AI requires careful auditing by qualified professionals. Competent and experienced auditors can identify and mitigate risks, ultimately safeguarding AI systems and the people they interact with.

---

The Importance of Auditor Expertise

AI systems are complex and can have unintended consequences. Auditors need a deep understanding of how these systems work, including their algorithms, data sources, and potential biases. They also need to be able to assess the risks associated with these systems and recommend appropriate mitigation strategies.

Unfortunately, the current landscape of AI auditing is not without its challenges. There is a lack of standardized training and certification programs, which can lead to inconsistencies in the quality of audits. Additionally, there is a risk of a "race to the bottom" in audit quality, as companies may prioritize cost over quality when selecting auditors.

---

A Path Forward

To address these challenges, we need to take several steps. First, we need to develop robust training and certification programs for AI auditors. These programs should be rigorous and cover a wide range of topics, including AI fundamentals, risk assessment, and audit methodologies.

Second, we need to establish clear standards for AI audits. These standards should be developed by experts in the field and should be regularly updated to reflect the latest developments in AI.

Third, we need to create a culture of quality in AI auditing. This means holding companies accountable for the quality of their audits and rewarding auditors for their expertise and experience.

---

Conclusion

AI auditing is critical to ensuring the safe and responsible development of AI systems. By investing in the training and development of competent AI auditors, we can help ensure that these systems are used for good and that their potential benefits are realized.

Let's foster a culture of rigorous AI auditing with a strong emphasis on auditor expertise. Share your thoughts in the comments!

#AI #auditing #artificialintelligence #safety #technology #riskmanagement

Read More

Senario Untuk Menerangkan Mengenai AI Kepada Orang Kampung

Ketika ini terdapat jurang pengetahuan terutamanya dalam bidang AI antara mereka yang di bandar dan mereka yang berada di kampung-kampung yang jauh dari bandar dan pekan. Jadi, bagaimana kita boleh memberi penerangan kepada mereka ini mengenai teknologi terkini seperti AI.

Dengan bantuan AI, maka, terhasil dialog yang berkenaan yang mungkin kita boleh jadikan sebagai bahan media dalam memberikan penerangan, bukan sahaja kepada mereka yang berada di kampung, malah pada mereka yang kurang pemahaman berkaitan AI ini.

Senario 1: Perbualan di Kedai Kopi

(Watak: Pak Abu, Pak Mat, dan Mat Din)

Pak Abu: Eh, korang dengar tak pasal benda AI yang budak-budak bandar selalu sembang tu? Aku dengar macam robot pintar pulak.

Pak Mat: Hah! AI tu macam otak manusia la, Abu. Tapi dia duduk dalam mesin. Kau tahu tak, kalau kau cakap "Hai Google" kat telefon kau, dia boleh jawab balik? Itu pun AI.

Mat Din: Kalau aku cakap, “Google, buatkan aku kopi,” dia buat tak?

Pak Mat: Kopi tak boleh, Din. Kau ingat AI tu pembantu rumah ke? Tapi kalau kau nak resepi buat kopi tarik power, dia boleh carikan kau langkah-langkah. Canggih, kan?

Mat Din: Hmmm, itu AI ke? Macam aku minta bini aku bancuh kopi, dia tanya, "Nak manis ke, kurang gula?" Itu kira AI jugak ke?

Pak Abu: Eh, taklah Din. Itu isteri AI - "Awek Intelligent"! (semua ketawa)

Pak Mat: Hahaha, tapi serius, AI ni boleh jadi macam manusia. Contohnya, kalau kita ni pekebun sawit, AI boleh tengok mana pokok yang tak sihat guna dron. Tak payah kita penat pusing kebun. Dia terus bagi tahu pokok mana kena tebang.

Mat Din: Oh, kalau macam tu, aku kena start guna AI jugak lah. Letih aku pusing kebun hari-hari! Tapi kalau AI tak betul bagitahu, aku halau dia masuk parit!

---

Senario 2: Perbualan di Tepi Sawah

(Watak: Pak Long, Pak Ngah, dan Amir)

Pak Long: Aku dengar sekarang ni petani kat Jepun pakai AI untuk tanam padi. Betul ke, Pak Ngah?

Pak Ngah: Betul, Long. AI ni pandai. Dia boleh tengok cuaca, tanah, dan air, lepas tu dia bagi tahu bila masa sesuai tanam dan tuai. Kita ni pakai naluri je, sebab tu kadang-kadang hasil tak menjadi.

Amir: Wah, canggihnya! Jadi AI tu macam bomoh sawah lah, ye?

Pak Ngah: Bomoh moden lah, Amir. Dia tak pakai tangkal, tapi pakai sensor dan komputer.

Pak Long: Kalau AI ni pandai sangat, nanti kerja petani tak ada gunanya lah?

Pak Ngah: Eh, taklah Long. AI ni tolong buat kerja berat je. Macam kita dulu guna kerbau, sekarang pakai traktor. AI ni traktor versi pintar. Tapi kena ada orang bijak jugak jaga dia, kalau tak dia "lumpuh."

Amir: Kalau macam tu, lepas ni aku nak pasang AI kat bendang aku. Kalau AI tu pandai sangat, suruh dia halau burung pipit sekali. Asyik makan padi aku je!

---

Senario 3: Perbualan di Perkampungan Nelayan

(Watak: Pak Ali, Pak Jali, dan Din Tekong)

Pak Ali: Korang tahu tak, sekarang ada bot yang boleh gerak sendiri, pakai AI. Dia boleh cari ikan kat laut tanpa nelayan ikut pun.

Pak Jali: Lah, habislah kita kalau macam tu. Kalau AI pandai sangat, siapa nak makan nasi hasil titik peluh kita ni?

Din Tekong: Relaxlah, Jali. AI ni cuma tolong kita. Contohnya, kalau kau pasang sonar AI, dia boleh tunjuk kat mana ikan berkumpul. Tak payah kita main tebak je baling pukat.

Pak Ali: Tapi Din, kalau AI salah tengok, bawak kita pergi cari ikan duyung macam mana?

Din Tekong: Itu kau kena guna AI yang betul, Ali. Jangan main beli dari internet murah-murah. Nanti ikan tak dapat, bot kau pulak yang tenggelam!

Pak Jali: Hahaha, tapi aku takutlah kalau AI pandai sangat. Nanti dia buat keputusan sendiri. Silap-silap, dia bawak bot pergi Filipina terus!

Din Tekong: Hahaha, itu AI lari rumah namanya. Jangan risau. AI tu tetap kena ada otak manusia kawal. Dia takkan berfungsi kalau kita tak suruh.

---

Senario 4: Perbualan di Dusun Buah

(Watak: Wak Seman, Pak Teh, dan Amin)

Wak Seman: Tahu tak, sekarang ada AI yang boleh petik buah sendiri? Robot dia siap tahu mana buah durian yang matang, mana yang muda. Tak payah kita tunggu bawah pokok kena hempap.

Pak Teh: Seriuslah, Wak? Kalau ada benda tu, aku nak beli satu. Tak payah dah aku sakit pinggang panjat pokok manggis.

Amin: Eh, Wak. Kalau macam tu, robot tu tahu ke beza durian kampung dengan durian Musang King?

Wak Seman: Tahu, Amin. Dia siap boleh scan bau durian kau tu. Kalau Musang King, dia ambil. Kalau durian kampung, dia letak balik. Canggih kan?

Pak Teh: Tapi Wak, kalau AI pandai sangat, nanti dia tak nak kerja dengan kita, dia buat kebun sendiri macam mana?

Wak Seman: Hahaha, jangan takutlah Teh. AI ni tak boleh makan durian, tak ada tekak. Kau tak payah risau dia buka gerai jual durian.

Amin: Tapi Wak, kalau AI dah pandai, nanti kita malas. Semua benda serah kat robot. Jangan-jangan nanti AI tu robot jadi tuan kita!

Wak Seman: Itulah pasal kena kawal. AI ni ibarat parang tajam. Kalau kau pandai guna, kerja senang. Kalau tak, kau sendiri kena potong. Jadi, gunalah dengan bijak.

Nota: Gambar di jana oleh Microsoft Designer manakala dialog di jana oleh ChatGPT.

_______________________________________________________________________________

Kesimpulan

Dari perbualan di kedai kopi, sawah, perkampungan nelayan, dan kebun buah, kita dapat melihat bahawa AI (Kecerdasan Buatan) sebenarnya adalah alat yang dicipta untuk memudahkan kehidupan kita. Sama seperti penggunaan teknologi lain seperti traktor, sonar, dan mesin automasi, AI bertujuan untuk membantu manusia bekerja dengan lebih cekap, cepat, dan berkesan. Namun, ia tidak bermakna AI boleh menggantikan manusia sepenuhnya. Sebaliknya, AI masih memerlukan pemantauan, kawalan, dan keputusan manusia untuk berfungsi dengan baik.

Walau bagaimanapun, semua kelebihan ini datang dengan cabaran. AI bukan sahaja pandai melakukan tugas teknikal, tetapi ia juga semakin mampu membuat keputusan, memberi cadangan, malah mempengaruhi hasil sesuatu situasi. Justeru, ini membawa kita kepada persoalan besar: bagaimana kita memastikan AI selamat, beretika, dan tidak mendatangkan bahaya kepada manusia?

Read More