2023 LeSN

3rd day of SNU Isabelle 2023, We practiced Verifying Functional Programs, Imperative Programming(Circus), Hoare Logic, Loop Invariants

This text covers tautologies, identities, Isar proofs, the Isabelle Simplifier, and proof by elimination examples.

This text explores formal methods in software development, focusing on functional programming, proofs, and the Isabelle/HOL prover.

연구 결과 요약 및 요일 별 진행 내용 2023 6 , Fuzz testing 년 월 저는 분야에 대한 연구를 시작했습니다 먼저 , OSSFuzzBugs 프로젝트를 접하고 관련 , 논문을 리뷰함으로써 전반적인 개념과 기술을 이해하였습니다.

Mutation-Based Fuzzing은 소프트웨어의 버그를 찾는 데 사용되는 자동화된 테스트 방법입니다. 이 방법은 소프트웨어의 코드를 무작위로 변경하여 버그를 유발할 수 있는 조건을 찾습니다.

논문리뷰: ModelDiff: Testing-Based DNN Similarity Comparison for Model Reuse Detection

심층신경망 경량화 기술 및 활용 사례 소개1) 어떤 문제를 해결하고 싶어하는 것인지 2) 왜 이 문제가 중요한지 3) 어떻게 해결하고 싶어하는 것인지 4) 해당 문제에 대한 느낌 등에 대하여 준비

로지코믹스 책 소개글입니다. 단순히 러셀의 삶과 그의 철학적 탐구를 서술하는 것 뿐만 아니라, 그 과정에서 철학 그 자체의 본질에 대해서도 탐구합니다.

이 비디오는 딥 뉴럴 네트워크의 형식적 검증에 대해 깊게 다룹니다. 강건성, 불완전 검증부터 AAAI AutoLay 라이브러리 소개와 AlphaCert 도구 사용법까지 포괄적으로 설명합니다.

TensorFlow 환경 내에서 딥러닝 모델의 양자화 방법과 계층별 분석 전략을 탐구합니다. 성능 향상을 목표로 한 최적화 방안과 함께, 모델의 세부 구조를 효과적으로 이해하기 위한 분석법을 제시합니다.

quantization in neural networks, specifically focusing on quantization for inference. The paper discusses various aspects of quantization.

요약Loss function add, remove or replace the loss function에 집중하여

Verifying concurrent programs poses challenges due to their complexity and potential for non-deterministic behavior.

TensorFlow와 PyTorch의 차이를 그래프 구조, API와 사용성, 배포, 지원 및 커뮤니티, 확장성에 대해 설명을 담은 글입니다.

PyTorch로 구현된 연구를 TensorFlow로 변환하려는 경우, 여러 고려사항과 주의해야 할 점이 있습니다. 그에 대한 설명을 담은 글입니다.

paper with code: https://paperswithcode.com/paper/quantization-and-training-of-neural-networksCVPR 2018Quantization, GeneralClassificationDataset

- 외부 라이브러리는 최소한만 이용하고 파이썬을 사용해 딥러닝 프로그램을 처음부터 구현합니다. _ 파이썬이 처음인 사람도 이해할 수 있도록 파이썬 사용법도 간략히 설명합니다. _ 실제 동작하는 파이썬 코드와 독자가 직접 실험할 수 있는 학습 환경을 제공합니다.

Tours through the BookIntroduction to Software TestingFuzzing: Breaking Things with Random InputsCode CoverageMutation-Based FuzzingGreybox FuzzingSea

DeepArc, a method to modularize neural networks, reducing the cost of model maintenance tasks by decomposing the network into consecutive modules.

Code Coverage Summary:IntroductionCode coverage measures which parts of a program are executed during a test run.This measurement is crucial for test

Decomposing a deep neural network (DNN) into modules to bring the benefits of modularity to deep learning.

.

Layer 별로 tensor값 출력하기

The paper introduces SegNet, a deep convolutional neural network architecture for semantic pixel-wise segmentation, which consists of an encoder netwo

텐서플로우에서 C++ 코드를 작성하여 연산을 구현할 때, 주로 포함되는 주요 컴포넌트와 각각의 역할에 대해서 설명하는 글입니다. 연산 등록, 형태 추론, 커널 구현, 커널 등록으로 구성되어있습니다.

Greybox Fuzzing 에 대한 설명입니다. Greybox Fuzzing with AFL, AFL 개요, Greybox Fuzzing에 필요한 요소들, 성능 평가 등으로 구성되어 있습니다.

The paper introduces testing techniques for neural networks using coverage-guided fuzzing (CGF) methods, which involve random mutations of inputs guid

DeepArc 환경설정, 디렉토리 구성, RQn 폴더, 파일 구성에 대한 설명을 담은 글입니다.

NNrepair is a technique for repairing neural network classifiers by identifying faulty network parameters and applying small modifications to fix them

The paper proposes a new method called Weight Fixing Networks (WFN) to minimize the information content of neural networks by reducing the number of u

kill -9 641 로 해결

배경지식 Centering Matrix Gram matrix CKA연산 유사성 행렬 연산 시각화

표준 상관 분석(CCA)을 사용하여 신경망 표현을 비교하는 방법을 살펴보고, 서로 다른 초기화에서 학습된 네트워크의 표현 간의 대응을 안정적으로 식별할 수 있는 중심 커널 정렬(CKA)이라는 유사성 지수를 소개합니다.

블랙박스 테스팅(Black Box Testing)과 화이트박스 테스팅(White Box Testing)은 소프트웨어 테스팅의 두 가지 기본적인 접근법이며, 각각의 테스팅 방식은 다음과 같은 차이점을 가지고 있습니다.

화이트박스 테스팅은 소프트웨어의 내부 구조와 작동 원리를 분석하여 테스팅을 수행하는 방법입니다. 여기에는 여러 가지 테스팅 기법이 포함되며, 각 기법은 특정한 목적과 접근 방식을 가지고 있습니다. 글에서 몇 가지 주요 화이트박스 테스팅 기법에 대해 설명합니다.

NNrepair는 결함 위치 파악을 사용하여 잠재적으로 결함이 있는 네트워크 매개 변수를 식별하고 결함을 해결하기 위해 작은 수정을 가하는 제약 조건 기반 기법입니다. Directory와 코드에 대한 설명을 담은 글입니다.

ModelDiff는 두 모델의 유사도를 비교하는 데에 사용됩니다. ModelDiff github Directory와 파일 및 코드 구성을 소개하는 글입니다.

다중 비트 양자화는 비트 분할 및 스티칭 프레임워크를 사용하여 구현할 수 있습니다.이 프레임워크는 두 가지 주요 단계로 구성됩니다: 비트 분할과 비트 최적화다음은 다중 비트 양자화를 위한 단계별 프로세스입니다:비트 분할: 이 단계에서는 가중치 양자화의 M비트 제약 조건

error message build error가 여러 폴더에서 발생한 것을 확인할 수 있었습니다. 중복되는 클래스가 각 폴더마다 존재해서 삭제했습니다. 경로는 다음과 같습니다.

ReluDiff는 원하는 속성이 검증될 때까지 근사치를 반복적으로 개선하는 빨리 감기 간격 분석 패스와 역방향 패스로 구성되며, 기존 검증 도구에 비해 상당한 속도 향상을 달성하고 더 많은 속성을 증명할 수 있습니다.

이 논문은 안전이 중요한 시스템에서 매우 중요한 구조적으로 유사한 신경망의 차등 검증 문제를 다룹니다.저자들은 피드포워드 ReLU 네트워크에서 미분 검증의 정확도와 계산 효율성을 크게 향상시키는 기호적이고 세분화된 근사화 기법인 NeuroDiff를 제안합니다.이 논문은

this paper presents an SMT-based encoding of the problem, exploring its utility and limitations.

The paper explores the use of differential testing to uncover failures in Automatic Speech Recognition (ASR) systems.

이 글에서는 RNN과 CNN의 차이점과 각각의 응용 분야에 대해 설명합니다.

Quantization을 이해하기 위해, 크레파스 색상을 예로 들어 볼게요. 크레파스 세트에는 많은 색상이 있지만, 때때로 우리는 모든 색상을 사용하지 않고 몇 가지 기본 색상만 사용해서 그림을 그립니다. 이렇게 하면 크레파스 세트를 더 작고 가볍게 만들 수 있어요.컴

ModelDiff는 마치 두 사람이 같은 그림을 보고 어떻게 반응하는지 비교하는 것처럼, 두 딥러닝 모델이 얼마나 비슷한지를 측정하는 도구예요.

컴퓨터 과학이나 딥 러닝과 같은 분야에서 공학적인 문제와 과학적인 문제를 구분하는 방식을 설명합니다. CNN모델 연구를 통해, 실제 연구를 할 때 마주할 수 있는 예시를 담았습니다.

BERT 모델과 ResNet 모델은 근본적으로 다른 목적과 구조를 가진 두 가지 중요한 인공지능 모델입니다. 이들의 차이점을 여러 측면에서 살펴보겠습니다.

SMT(Satisfiability Modulo Theories) 솔버와 다른 종류의 솔버(예를 들어 SAT(Satisfiability) 솔버, 전통적인 수학적 솔버 등) 간의 차이를 이해하기 위해, 주요 특징과 기능을 표 형식으로 비교해보겠습니다.

많이 사용되는 SMT 솔버인 Z3를 이용한 다양한 문제 해결 예시입니다. Z3는 복잡한 논리적 조건과 수학적 이론을 포함하는 문제를 해결하는 데 매우 유용합니다. 다음은 몇 가지 다양한 유형의 문제를 해결하는 Z3 코드 예시입니다.

현재의 AI 시스템의 취약성, 해석 가능성 부족과 같은 문제점으로 인해더 신뢰할 수 있고 해석 가능한 AI 시스템의 필요성딥 뉴럴 네트워크의 공격과 방어의 최신 동향을 이해하고 습득적대적 공격, 방어, 실험적 견고성 및 수학적 인증과 같은 주제를 논의합니다.

Intro, Index